Documentation

SampCert.Samplers.Laplace.Properties

DiscreteLaplaceSample Properties #

This file proves evaluation and normalization properties of DiscreteLaplaceSample.

source
@[simp]
theorem SLang.DiscreteLaplaceSampleLoopIn1Aux_normalizes (t : ℕ+) :
∑' (x : ℕ × Bool), SLang.DiscreteLaplaceSampleLoopIn1Aux t x = 1
source
theorem SLang.DiscreteLaplaceSampleLoopIn1Aux_apply_true (t : ℕ+) (n : ℕ) :
SLang.DiscreteLaplaceSampleLoopIn1Aux t (n, true) = if n < ↑t then ENNReal.ofReal (Real.exp (-(↑n / ↑↑t))) / ↑↑t else 0
source
theorem SLang.DiscreteLaplaceSampleLoopIn1Aux_apply_false (t : ℕ+) (n : ℕ) :
SLang.DiscreteLaplaceSampleLoopIn1Aux t (n, false) = if n < ↑t then (1 - ENNReal.ofReal (Real.exp (-(↑n / ↑↑t)))) / ↑↑t else 0
source
theorem SLang.DiscreteLaplaceSampleLoopIn1_apply_pre (t : ℕ+) (n : ℕ) :
SLang.DiscreteLaplaceSampleLoopIn1 t n = SLang.DiscreteLaplaceSampleLoopIn1Aux t (n, true) * (∑' (a : ℕ), SLang.DiscreteLaplaceSampleLoopIn1Aux t (a, true))⁻¹
source
theorem SLang.DiscreteLaplaceSampleLoopIn1_apply (t : ℕ+) (n : ℕ) (support : n < ↑t) :
SLang.DiscreteLaplaceSampleLoopIn1 t n = ENNReal.ofReal (Real.exp (-(↑n / ↑↑t).toReal) * ((1 - Real.exp (-1 / ↑↑t)) / (1 - Real.exp (-1))))
source
@[simp]
theorem SLang.DiscreteLaplaceSampleLoopIn2_eq (num : ℕ) (den : ℕ+) :
SLang.DiscreteLaplaceSampleLoopIn2 num den = (SLang.BernoulliExpNegSample num den).probGeometric
source
@[simp]
theorem SLang.DiscreteLaplaceSampleLoop_apply (num : ℕ+) (den : ℕ+) (n : ℕ) (b : Bool) :
SLang.DiscreteLaplaceSampleLoop num den (b, n) = ENNReal.ofReal (Real.exp (-(↑↑den / ↑↑num))) ^ n * (1 - ENNReal.ofReal (Real.exp (-(↑↑den / ↑↑num)))) * (↑↑2)⁻¹
source
@[simp]
theorem SLang.ite_simpl_1 (x : ℕ) (y : ℕ) (a : ENNReal) :
(if x = y then 0 else if y = x then a else 0) = 0
source
@[simp]
theorem SLang.ite_simpl_2 (x : ℕ) (y : ℕ) (a : ENNReal) :
(if x = 0 then 0 else if ↑y = -↑x then a else 0) = 0
source
@[simp]
theorem SLang.ite_simpl_3 (x : ℕ) (y : ℕ) (a : ENNReal) :
(if x = y + 1 then 0 else if x = 0 then 0 else if y = x - 1 then a else 0) = 0
source
@[simp]
theorem SLang.ite_simpl_4 (x : ℕ) (y : ℕ) (a : ENNReal) :
(if ↑x = -↑y then if y = 0 then 0 else a else 0) = 0
source
@[simp]
theorem SLang.ite_simpl_5 (n : ℕ) (c : ℕ) (a : ENNReal) (h : n ≠ 0) :
(if -↑n = ↑c then a else 0) = 0
source
@[simp]
theorem SLang.DiscreteLaplaceSampleLoop_normalizes (num : ℕ+) (den : ℕ+) :
∑' (x : Bool × ℕ), SLang.DiscreteLaplaceSampleLoop num den x = 1
source
theorem SLang.avoid_double_counting (num : ℕ+) (den : ℕ+) :
(∑' (x : Bool × ℕ), if x.1 = true → ¬x.2 = 0 then SLang.DiscreteLaplaceSampleLoop num den x else 0) = (↑↑2)⁻¹ * (1 + ENNReal.ofReal (Real.exp (-(↑↑den / ↑↑num))))
source
theorem SLang.laplace_normalizer_swap (num : ℕ+) (den : ℕ+) :
(1 - Real.exp (-(↑↑den / ↑↑num))) * (1 + Real.exp (-(↑↑den / ↑↑num)))⁻¹ = (Real.exp (↑↑den / ↑↑num) - 1) * (Real.exp (↑↑den / ↑↑num) + 1)⁻¹
source
@[simp]
theorem SLang.DiscreteLaplaceSample_apply (num : ℕ+) (den : ℕ+) (x : ℤ) :
SLang.DiscreteLaplaceSample num den x = ENNReal.ofReal ((Real.exp (1 / (↑↑↑num / ↑↑↑den)) - 1) / (Real.exp (1 / (↑↑↑num / ↑↑↑den)) + 1) * Real.exp (-(↑|x| / (↑↑↑num / ↑↑↑den))))

Closed form for the evaluation of the SLang Laplace sampler.

source
@[simp]
theorem SLang.DiscreteLaplaceSample_normalizes (num : ℕ+) (den : ℕ+) :
∑' (x : ℤ), SLang.DiscreteLaplaceSample num den x = 1

SLang Laplace sampler is a proper distribution.