Stat.Privacy

Differential privacy via the Laplace mechanism: the centered Laplace distribution and its density-ratio bound, scalar and finite-dimensional additive-noise release, pure and approximate ε-differential-privacy guarantees, post-processing closure, and Laplace-noise moment bounds.

LaplaceMechanism 9 core · 9 supporting This file supplies the classical centred Laplace distribution, its density-ratio bound, scalar and finite-dimensional Laplace mechanisms, and post-processing lemmas. ★ laplaceMech_pure_dp★ laplaceMechPi_pure_dp★ pure_dp_implies_approx_dp★ pure_dp_postprocess★ approx_dp_postprocess

The Laplace mechanism and pure differential privacy

This file supplies the classical centred Laplace distribution, its density-ratio bound, scalar and finite-dimensional Laplace mechanisms, and post-processing lemmas. Dataset types and adjacency relations remain completely abstract.

def laplacePDF reviewed

Causalean.Stat.Privacy

For a real scale parameter and a real evaluation point, the centered Laplace density is $(2b)^{-1}\exp(-|x|/b)$ .

Definition (Lean source)

parameters

b x :

ℝ

def

laplacePDF b x :

ℝ

given by

(2 * b)⁻¹ * exp (-|x| / b)

Causalean.Stat.Privacy.laplacePDF · Causalean/Stat/Privacy/LaplaceMechanism.lean:29

def laplaceMeasure reviewed

Causalean.Stat.Privacy

For a real scale parameter, the centered Laplace measure is Lebesgue measure weighted by the nonnegative part of the centered Laplace density at that scale.

Definition (Lean source)

parameters

b :

ℝ

def

laplaceMeasure b :

Measure ℝ

given by

volume.withDensity (fun x => ofReal (laplacePDF b x))

Causalean.Stat.Privacy.laplaceMeasure · Causalean/Stat/Privacy/LaplaceMechanism.lean:33

def laplaceMech reviewed

Causalean.Stat.Privacy

For a dataset domain, a real noise scale, and a real-valued query on that domain, the scalar Laplace mechanism assigns to each dataset the distribution of the query evaluated at that dataset plus an independent centered Laplace draw with that scale.

Definition (Lean source)

parameters

D :

Type*

b :

ℝ

q :

D → ℝ

def

laplaceMech b q :

D → Measure ℝ

given by

fun d => (laplaceMeasure b).map (fun z => z + q d)

Causalean.Stat.Privacy.laplaceMech · Causalean/Stat/Privacy/LaplaceMechanism.lean:151

theorem laplaceMech_pure_dp reviewed

Causalean.Stat.Privacy

Scalar Laplace mechanism is purely differentially private. Given a positive sensitivity bound $\Delta$ and a positive privacy level $\varepsilon$ such that the query q changes by at most $\Delta$ between any pair of adjacent datasets, releasing q after adding independent Laplace noise of scale $\Delta/\varepsilon$ satisfies pure $\varepsilon$ -differential privacy: for every adjacent pair, the probability of any measurable event under one release is at most $e^\varepsilon$ times its probability under the other.

Formal statement

hypotheses

D :

Type*

Adj :

D → D → Prop

q :

D → ℝ

Δ ε :

ℝ

hΔ :

0 < Δ

hε :

0 < ε

hsens :

∀ d d'

Adj d d'

then

|q d - q d'| ≤ Δ

d d' :

Adj d d'

s :

MeasurableSet s

conclusion

(laplaceMech (Δ / ε) q d).real s ≤ exp ε * (laplaceMech (Δ / ε) q d').real s

Proof (Lean source)

theorem laplaceMech_pure_dp {D : Type*} (Adj : D → D → Prop) (q : D → ℝ) {Δ ε : ℝ} (hΔ : 0 < Δ) (hε : 0 < ε) (hsens : ∀ d d', Adj d d' → |q d - q d'| ≤ Δ) : ∀ d d', Adj d d' → ∀ s, MeasurableSet s → (laplaceMech (Δ / ε) q d).real s ≤ exp ε * (laplaceMech (Δ / ε) q d').real s := by intro d d' hadd s hs have hb : 0 < Δ / ε := div_pos hΔ hε have hscale : |q d - q d'| / (Δ / ε) ≤ ε := by apply (div_le_iff₀ hb).2 calc |q d - q d'| ≤ Δ := hsens d d' hadd _ = ε * (Δ / ε) := by field_simp have hpdf (x : ℝ) : laplacePDF (Δ / ε) (x - q d) ≤ exp ε * laplacePDF (Δ / ε) (x - q d') := by calc laplacePDF (Δ / ε) (x - q d) ≤ exp (|q d - q d'| / (Δ / ε)) * laplacePDF (Δ / ε) (x - q d') := laplacePDF_shift_le (Δ / ε) (q d) (q d') x hb _ ≤ exp ε * laplacePDF (Δ / ε) (x - q d') := by exact mul_le_mul_of_nonneg_right (Real.exp_le_exp.mpr hscale) (laplacePDF_nonneg hb _) have hmeasure : laplaceMech (Δ / ε) q d ≤ (ofReal (exp ε)) • laplaceMech (Δ / ε) q d' := by rw [laplaceMech_eq_withDensity, laplaceMech_eq_withDensity] let f : ℝ → ENNReal := fun x => ofReal (laplacePDF (Δ / ε) (x - q d')) have hf : Measurable f := ((measurable_laplacePDF (Δ / ε)).comp (by fun_prop)).ennreal_ofReal change volume.withDensity _ ≤ ofReal (exp ε) • volume.withDensity f rw [← withDensity_smul (μ := volume) (ofReal (exp ε)) hf] apply withDensity_mono filter_upwards with x change ofReal (laplacePDF (Δ / ε) (x - q d)) ≤ ofReal (exp ε) * ofReal (laplacePDF (Δ / ε) (x - q d')) rw [← ENNReal.ofReal_mul (Real.exp_pos ε).le] exact ENNReal.ofReal_le_ofReal (hpdf x) have hle := hmeasure s rw [Measure.smul_apply] at hle letI : IsProbabilityMeasure (laplaceMech (Δ / ε) q d) := laplaceMech_isProbabilityMeasure (Δ / ε) hb q d letI : IsProbabilityMeasure (laplaceMech (Δ / ε) q d') := laplaceMech_isProbabilityMeasure (Δ / ε) hb q d' change ((laplaceMech (Δ / ε) q d) s).toReal ≤ exp ε * ((laplaceMech (Δ / ε) q d') s).toReal rw [← ENNReal.toReal_ofReal (Real.exp_pos ε).le, ← ENNReal.toReal_mul] · exact ENNReal.toReal_mono (ENNReal.mul_ne_top ENNReal.ofReal_ne_top (measure_ne_top (laplaceMech (Δ / ε) q d') s)) hle

Causalean.Stat.Privacy.laplaceMech_pure_dp · Causalean/Stat/Privacy/LaplaceMechanism.lean:192 · uses laplaceMech

def laplaceMechPi reviewed

Causalean.Stat.Privacy

For a dataset domain, a finite coordinate index set, a real noise scale, and a coordinate-indexed real-valued query on the dataset domain, the finite-dimensional Laplace mechanism assigns to each dataset the distribution obtained by adding independent centered Laplace draws with that scale to all query coordinates.

Definition (Lean source)

parameters

D ι :

Type*

Fintype ι

b :

ℝ

q :

D → (ι → ℝ)

def

laplaceMechPi b q :

D → Measure (ι → ℝ)

given by

fun d => (Measure.pi (fun _ : ι => laplaceMeasure b)).map (fun z => z + q d)

Causalean.Stat.Privacy.laplaceMechPi · Causalean/Stat/Privacy/LaplaceMechanism.lean:250

theorem laplaceMechPi_pure_dp reviewed

Causalean.Stat.Privacy

Vector Laplace mechanism is purely differentially private. Given a positive $\ell^1$ -sensitivity bound $\Delta$ and a positive privacy level $\varepsilon$ such that the coordinatewise absolute differences of the query q sum to at most $\Delta$ between any pair of adjacent datasets, releasing q after adding independent Laplace noise of scale $\Delta/\varepsilon$ to each coordinate satisfies pure $\varepsilon$ -differential privacy: for every adjacent pair, the probability of any measurable event under one release is at most $e^\varepsilon$ times its probability under the other.

Formal statement

hypotheses

D ι :

Type*

Fintype ι

Adj :

D → D → Prop

q :

D → (ι → ℝ)

Δ ε :

ℝ

hΔ :

0 < Δ

hε :

0 < ε

hsens :

∀ d d'

Adj d d'

then

∑ i, |q d i - q d' i| ≤ Δ

d d' :

Adj d d'

s :

MeasurableSet s

conclusion

(laplaceMechPi (Δ / ε) q d).real s ≤ exp ε * (laplaceMechPi (Δ / ε) q d').real s

Proof (Lean source)

theorem laplaceMechPi_pure_dp {D ι : Type*} [Fintype ι] (Adj : D → D → Prop) (q : D → (ι → ℝ)) {Δ ε : ℝ} (hΔ : 0 < Δ) (hε : 0 < ε) (hsens : ∀ d d', Adj d d' → ∑ i, |q d i - q d' i| ≤ Δ) : ∀ d d', Adj d d' → ∀ s, MeasurableSet s → (laplaceMechPi (Δ / ε) q d).real s ≤ exp ε * (laplaceMechPi (Δ / ε) q d').real s := by intro d d' hadd s hs have hb : 0 < Δ / ε := div_pos hΔ hε let μ : ι → Measure ℝ := fun i => (laplaceMeasure (Δ / ε)).map (fun z => z + q d i) let ν : ι → Measure ℝ := fun i => (laplaceMeasure (Δ / ε)).map (fun z => z + q d' i) let c : ι → ENNReal := fun i => ofReal (exp (|q d i - q d' i| / (Δ / ε))) letI (i : ι) : IsProbabilityMeasure (μ i) := by dsimp [μ] letI := laplaceMeasure_isProbabilityMeasure (Δ / ε) hb exact Measure.isProbabilityMeasure_map (by fun_prop) letI (i : ι) : IsProbabilityMeasure (ν i) := by dsimp [ν] letI := laplaceMeasure_isProbabilityMeasure (Δ / ε) hb exact Measure.isProbabilityMeasure_map (by fun_prop) have hpi : Measure.pi μ ≤ (∏ i, c i) • Measure.pi ν := pi_le_smul_pi μ ν c (fun i => laplace_shift_measure_le _ _ _ hb) have hsum : (∑ i, |q d i - q d' i| / (Δ / ε)) ≤ ε := by rw [← Finset.sum_div] apply (div_le_iff₀ hb).2 calc (∑ i, |q d i - q d' i|) ≤ Δ := hsens d d' hadd _ = ε * (Δ / ε) := by field_simp have hc : (∏ i, c i) ≤ ofReal (exp ε) := by change (∏ i, ofReal (exp (|q d i - q d' i| / (Δ / ε)))) ≤ _ rw [← ENNReal.ofReal_prod_of_nonneg (fun i _ => (Real.exp_pos _).le), ← Real.exp_sum] exact ENNReal.ofReal_le_ofReal (Real.exp_le_exp.mpr hsum) have hmeasure : laplaceMechPi (Δ / ε) q d ≤ ofReal (exp ε) • laplaceMechPi (Δ / ε) q d' := by rw [laplaceMechPi_eq_pi_shift (hb := hb), laplaceMechPi_eq_pi_shift (hb := hb)] apply hpi.trans rw [Measure.le_iff'] intro t simp only [Measure.smul_apply, smul_eq_mul] change (∏ i, c i) * (Measure.pi ν) t ≤ ofReal (exp ε) * (Measure.pi ν) t gcongr have hle := hmeasure s rw [Measure.smul_apply] at hle letI := laplaceMechPi_isProbabilityMeasure (Δ / ε) hb q d letI := laplaceMechPi_isProbabilityMeasure (Δ / ε) hb q d' change ((laplaceMechPi (Δ / ε) q d) s).toReal ≤ exp ε * ((laplaceMechPi (Δ / ε) q d') s).toReal rw [← ENNReal.toReal_ofReal (Real.exp_pos ε).le, ← ENNReal.toReal_mul] exact ENNReal.toReal_mono (ENNReal.mul_ne_top ENNReal.ofReal_ne_top (measure_ne_top (laplaceMechPi (Δ / ε) q d') s)) hle

Causalean.Stat.Privacy.laplaceMechPi_pure_dp · Causalean/Stat/Privacy/LaplaceMechanism.lean:378 · uses laplaceMechPi

theorem pure_dp_implies_approx_dp reviewed

Causalean.Stat.Privacy

Pure DP implies approximate DP. Given a mechanism M satisfying pure $\varepsilon$ -differential privacy between releases M d and M d', i.e. the probability of every measurable event under one release is at most $e^\varepsilon$ times its probability under the other, adding any nonnegative failure allowance $\delta$ to the bound still yields a valid $(\varepsilon,\delta)$ -approximate differential-privacy guarantee between M d and M d'.

Formal statement

hypotheses

D :

Sort u_2

shared

α :

Type*

MeasurableSpace α

M :

D → Measure α

d d' :

ε δ :

ℝ

hpure :

∀ s

MeasurableSet s

then

(M d).real s ≤ exp ε * (M d').real s

hδ :

0 ≤ δ

s :

MeasurableSet s

conclusion

(M d).real s ≤ exp ε * (M d').real s + δ

Proof (Lean source)

theorem pure_dp_implies_approx_dp {α : Type*} [MeasurableSpace α] (M : D → Measure α) (d d' : D) (ε δ : ℝ) (hpure : ∀ s, MeasurableSet s → (M d).real s ≤ exp ε * (M d').real s) (hδ : 0 ≤ δ) : ∀ s, MeasurableSet s → (M d).real s ≤ exp ε * (M d').real s + δ := by intro s hs exact (hpure s hs).trans (le_add_of_nonneg_right hδ)

Causalean.Stat.Privacy.pure_dp_implies_approx_dp · Causalean/Stat/Privacy/LaplaceMechanism.lean:442

theorem pure_dp_postprocess reviewed

Causalean.Stat.Privacy

Post-processing preserves pure differential privacy. Given a vector-valued mechanism M satisfying pure $\varepsilon$ -differential privacy between the releases M d and M d', post-processing the release by any measurable scalar summary f again satisfies pure $\varepsilon$ -differential privacy, now between the f-summaries of M d and M d'.

Formal statement

hypotheses

D ι :

Type*

M :

D → Measure (ι → ℝ)

d d' :

ε :

ℝ

hM :

∀ s

MeasurableSet s

then

(M d).real s ≤ exp ε * (M d').real s

f :

(ι → ℝ) → ℝ

hf :

Measurable f

s :

MeasurableSet s

conclusion

((M d).map f).real s ≤ exp ε * ((M d').map f).real s

Proof (Lean source)

theorem pure_dp_postprocess {D ι : Type*} (M : D → Measure (ι → ℝ)) (d d' : D) (ε : ℝ) (hM : ∀ s, MeasurableSet s → (M d).real s ≤ exp ε * (M d').real s) (f : (ι → ℝ) → ℝ) (hf : Measurable f) : ∀ s, MeasurableSet s → ((M d).map f).real s ≤ exp ε * ((M d').map f).real s := by intro s hs change ((M d).map f s).toReal ≤ exp ε * ((M d').map f s).toReal rw [Measure.map_apply hf hs, Measure.map_apply hf hs] exact hM (f ⁻¹' s) (hs.preimage hf)

Causalean.Stat.Privacy.pure_dp_postprocess · Causalean/Stat/Privacy/LaplaceMechanism.lean:457

theorem approx_dp_postprocess reviewed

Causalean.Stat.Privacy

Post-processing preserves approximate differential privacy. Given a vector-valued mechanism M obeying an $(\varepsilon,\delta)$ -approximate DP bound between the releases M d and M d' for every measurable event, with a nonnegative failure allowance $\delta$ , post-processing the release by any measurable scalar summary f again satisfies the same $(\varepsilon,\delta)$ -approximate DP bound, now between the f-summaries of M d and M d'.

Formal statement

hypotheses

D ι :

Type*

M :

D → Measure (ι → ℝ)

d d' :

ε δ :

ℝ

hM :

∀ s

MeasurableSet s

then

(M d).real s ≤ exp ε * (M d').real s + δ

_hδ :

0 ≤ δ

f :

(ι → ℝ) → ℝ

hf :

Measurable f

s :

MeasurableSet s

conclusion

((M d).map f).real s ≤ exp ε * ((M d').map f).real s + δ

Proof (Lean source)

theorem approx_dp_postprocess {D ι : Type*} (M : D → Measure (ι → ℝ)) (d d' : D) (ε δ : ℝ) (hM : ∀ s, MeasurableSet s → (M d).real s ≤ exp ε * (M d').real s + δ) (_hδ : 0 ≤ δ) (f : (ι → ℝ) → ℝ) (hf : Measurable f) : ∀ s, MeasurableSet s → ((M d).map f).real s ≤ exp ε * ((M d').map f).real s + δ := by intro s hs change ((M d).map f s).toReal ≤ exp ε * ((M d').map f s).toReal + δ rw [Measure.map_apply hf hs, Measure.map_apply hf hs] exact hM (f ⁻¹' s) (hs.preimage hf)

Causalean.Stat.Privacy.approx_dp_postprocess · Causalean/Stat/Privacy/LaplaceMechanism.lean:474

9 supporting declarations (lemmas, instances)

measurable_laplacePDF lemma — The Laplace density with scale b is a measurable function on the real line.

hypotheses

b :

ℝ

conclusion

Measurable (laplacePDF b)

Proof (Lean source)

@[fun_prop] lemma measurable_laplacePDF (b : ℝ) : Measurable (laplacePDF b) := by unfold laplacePDF fun_prop

Causalean.Stat.Privacy.measurable_laplacePDF · Causalean/Stat/Privacy/LaplaceMechanism.lean:43
laplaceMeasure_isProbabilityMeasure theorem — At every positive scale, the centered Laplace measure has total mass one and therefore defines a probability distribution.

hypotheses

b :

ℝ

hb :

0 < b

conclusion

IsProbabilityMeasure (laplaceMeasure b)

Proof (Lean source)

theorem laplaceMeasure_isProbabilityMeasure (b : ℝ) (hb : 0 < b) : IsProbabilityMeasure (laplaceMeasure b) := by refine ⟨?_⟩ rw [laplaceMeasure, withDensity_apply _ MeasurableSet.univ] rw [Measure.restrict_univ] have hdens : (fun x => ofReal (laplacePDF b x)) = fun x => (toNNReal (laplacePDF b x) : ENNReal) := by funext x rw [ENNReal.ofReal_eq_coe_nnreal (laplacePDF_nonneg hb x)] congr 1 ext simp [Real.toNNReal_of_nonneg (laplacePDF_nonneg hb x)] rw [hdens, lintegral_coe_eq_integral] · convert congrArg ofReal (integral_laplacePDF hb) using 1 <;> simp [max_eq_left (laplacePDF_nonneg hb _)] · simpa [Real.toNNReal_of_nonneg, laplacePDF_nonneg hb] using integrable_laplacePDF hb

Causalean.Stat.Privacy.laplaceMeasure_isProbabilityMeasure · Causalean/Stat/Privacy/LaplaceMechanism.lean:107
laplacePDF_shift_le theorem — Moving the center of a positive-scale Laplace density changes its value at any observation by at most an exponential factor determined by the distance between the old and new centers divided by the scale.

hypotheses

b u v z :

ℝ

hb :

0 < b

conclusion

laplacePDF b (z - u) ≤ exp (|u - v| / b) * laplacePDF b (z - v)

Proof (Lean source)

theorem laplacePDF_shift_le (b u v z : ℝ) (hb : 0 < b) : laplacePDF b (z - u) ≤ exp (|u - v| / b) * laplacePDF b (z - v) := by have htri : |z - v| - |z - u| ≤ |u - v| := by calc |z - v| - |z - u| ≤ |(z - v) - (z - u)| := abs_sub_abs_le_abs_sub (z - v) (z - u) _ = |u - v| := by congr 1; simp have hexp : exp (-|z - u| / b) ≤ exp (|u - v| / b) * exp (-|z - v| / b) := by rw [← Real.exp_add, Real.exp_le_exp] rw [show |u - v| / b + -|z - v| / b = (|u - v| - |z - v|) / b by ring] exact (div_le_div_iff_of_pos_right hb).2 (by linarith) unfold laplacePDF calc (2 * b)⁻¹ * exp (-|z - u| / b) ≤ (2 * b)⁻¹ * (exp (|u - v| / b) * exp (-|z - v| / b)) := mul_le_mul_of_nonneg_left hexp (by positivity) _ = exp (|u - v| / b) * ((2 * b)⁻¹ * exp (-|z - v| / b)) := by ring

Causalean.Stat.Privacy.laplacePDF_shift_le · Causalean/Stat/Privacy/LaplaceMechanism.lean:126
laplaceMech_isProbabilityMeasure theorem — Adding positive-scale Laplace noise to a scalar query produces a probability distribution for the release under every dataset.

hypotheses

D :

Type*

b :

ℝ

hb :

0 < b

q :

D → ℝ

d :

D

conclusion

IsProbabilityMeasure (laplaceMech b q d)

Proof (Lean source)

theorem laplaceMech_isProbabilityMeasure {D : Type*} (b : ℝ) (hb : 0 < b) (q : D → ℝ) (d : D) : IsProbabilityMeasure (laplaceMech b q d) := by letI : IsProbabilityMeasure (laplaceMeasure b) := laplaceMeasure_isProbabilityMeasure b hb unfold laplaceMech exact Measure.isProbabilityMeasure_map (by fun_prop)

Causalean.Stat.Privacy.laplaceMech_isProbabilityMeasure · Causalean/Stat/Privacy/LaplaceMechanism.lean:183
laplaceMechPi_isProbabilityMeasure theorem — Adding independent positive-scale Laplace noise in finitely many coordinates produces a probability distribution for the vector release under every dataset.

hypotheses

D ι :

Type*
Fintype ι

b :

ℝ

hb :

0 < b

q :

D → (ι → ℝ)

d :

D

conclusion

IsProbabilityMeasure (laplaceMechPi b q d)

Proof (Lean source)

theorem laplaceMechPi_isProbabilityMeasure {D ι : Type*} [Fintype ι] (b : ℝ) (hb : 0 < b) (q : D → (ι → ℝ)) (d : D) : IsProbabilityMeasure (laplaceMechPi b q d) := by letI : IsProbabilityMeasure (laplaceMeasure b) := laplaceMeasure_isProbabilityMeasure b hb haveI : IsProbabilityMeasure (Measure.pi (fun _ : ι => laplaceMeasure b)) := inferInstance unfold laplaceMechPi exact Measure.isProbabilityMeasure_map (by fun_prop)

Causalean.Stat.Privacy.laplaceMechPi_isProbabilityMeasure · Causalean/Stat/Privacy/LaplaceMechanism.lean:258
laplaceMeasure_integrable_abs theorem — The absolute value of a centered Laplace draw has a finite expectation at every positive scale.

hypotheses

b :

ℝ

hb :

0 < b

conclusion

Integrable (fun x : ℝ => |x|) (laplaceMeasure b)

Proof (Lean source)

theorem laplaceMeasure_integrable_abs (b : ℝ) (hb : 0 < b) : Integrable (fun x : ℝ => |x|) (laplaceMeasure b) := by rw [laplaceMeasure, integrable_withDensity_iff_integrable_smul' (measurable_laplacePDF b).ennreal_ofReal (ae_of_all _ fun _ => ENNReal.ofReal_lt_top)] simpa only [ENNReal.toReal_ofReal (laplacePDF_nonneg hb _), smul_eq_mul, mul_comm] using integrable_abs_mul_laplacePDF b hb

Causalean.Stat.Privacy.laplaceMeasure_integrable_abs · Causalean/Stat/Privacy/LaplaceMechanism.lean:533
laplaceMeasure_integral_abs theorem — The expected absolute value of a centered Laplace draw equals its positive scale.

hypotheses

b :

ℝ

hb :

0 < b

conclusion

∫ x, |x| ∂(laplaceMeasure b) = b

Proof (Lean source)

theorem laplaceMeasure_integral_abs (b : ℝ) (hb : 0 < b) : ∫ x, |x| ∂(laplaceMeasure b) = b := by rw [laplaceMeasure, integral_withDensity_eq_integral_toReal_smul (measurable_laplacePDF b).ennreal_ofReal (ae_of_all _ fun _ => ENNReal.ofReal_lt_top)] simp_rw [ENNReal.toReal_ofReal (laplacePDF_nonneg hb _), smul_eq_mul] let f : ℝ → ℝ := fun x => (2 * b)⁻¹ * (x * exp (-x / b)) rw [show (fun x : ℝ => laplacePDF b x * |x|) = fun x => f |x| by funext x simp only [f, laplacePDF] ring, integral_comp_abs] have hplain : (∫ x in Ioi (0 : ℝ), x * exp (-x / b)) = b ^ 2 := by calc _ = ∫ x in Ioi (0 : ℝ), x ^ ((2 : ℝ) - 1) * exp (-((1 / b) * x)) := by apply setIntegral_congr_fun measurableSet_Ioi intro x hx simp only [show (2 : ℝ) - 1 = 1 by norm_num, Real.rpow_one] rw [show -x / b = -(1 / b * x) by ring] _ = (1 / (1 / b)) ^ (2 : ℝ) * Real.Gamma (2 : ℝ) := Real.integral_rpow_mul_exp_neg_mul_Ioi (by norm_num) (one_div_pos.mpr hb) _ = b ^ 2 := by rw [show Real.Gamma (2 : ℝ) = 1 by norm_num] field_simp [hb.ne'] exact Real.rpow_natCast b 2 have hright : (∫ x in Ioi (0 : ℝ), f x) = (2 * b)⁻¹ * b ^ 2 := by rw [show f = fun x => (2 * b)⁻¹ * (x * exp (-x / b)) by rfl, integral_const_mul, hplain] rw [hright] field_simp [hb.ne']

Causalean.Stat.Privacy.laplaceMeasure_integral_abs · Causalean/Stat/Privacy/LaplaceMechanism.lean:543
laplacePi_integral_euclidean_norm_le theorem — The expected Euclidean norm of a finite vector of independent centered Laplace draws is at most the number of coordinates times their common positive scale.

hypotheses

ι :

Type*
Fintype ι

b :

ℝ

hb :

0 < b

conclusion

∫ w, sqrt (∑ i : ι, (w i) ^ 2) ∂(Measure.pi fun _ : ι => laplaceMeasure b)
≤ (Fintype.card ι : ℝ) * b

Proof (Lean source)

theorem laplacePi_integral_euclidean_norm_le {ι : Type*} [Fintype ι] (b : ℝ) (hb : 0 < b) : ∫ w, sqrt (∑ i : ι, (w i) ^ 2) ∂(Measure.pi fun _ : ι => laplaceMeasure b) ≤ (Fintype.card ι : ℝ) * b := by letI : IsProbabilityMeasure (laplaceMeasure b) := laplaceMeasure_isProbabilityMeasure b hb let P : Measure (ι → ℝ) := Measure.pi fun _ : ι => laplaceMeasure b have hcoord (i : ι) : Integrable (fun w : ι → ℝ => |w i|) P := integrable_comp_eval (laplaceMeasure_integrable_abs b hb) have hsum : Integrable (fun w : ι → ℝ => ∑ i : ι, |w i|) P := integrable_finset_sum _ fun i _ => hcoord i have hnorm : Integrable (fun w : ι → ℝ => sqrt (∑ i : ι, (w i) ^ 2)) P := by have hcontinuous : Continuous (fun w : ι → ℝ => sqrt (∑ i : ι, (w i) ^ 2)) := Real.continuous_sqrt.comp (continuous_finset_sum _ fun i _ => (continuous_apply i).pow 2) refine hsum.mono' hcontinuous.aestronglyMeasurable (ae_of_all _ fun w => ?_) rw [Real.norm_of_nonneg (Real.sqrt_nonneg _)] exact sqrt_sum_sq_le_sum_abs w calc ∫ w, sqrt (∑ i : ι, (w i) ^ 2) ∂P ≤ ∫ w, ∑ i : ι, |w i| ∂P := integral_mono hnorm hsum (sqrt_sum_sq_le_sum_abs) _ = ∑ i : ι, ∫ w, |w i| ∂P := integral_finset_sum _ fun i _ => hcoord i _ = ∑ _i : ι, b := by congr 1 with i change (∫ w : ι → ℝ, |w i| ∂Measure.pi (fun _ : ι => laplaceMeasure b)) = b exact (integral_comp_eval (μ := fun _ : ι => laplaceMeasure b) (i := i) (f := fun x : ℝ => |x|) (Continuous.aestronglyMeasurable continuous_abs)).trans (laplaceMeasure_integral_abs b hb) _ = (Fintype.card ι : ℝ) * b := by simp

Causalean.Stat.Privacy.laplacePi_integral_euclidean_norm_le · Causalean/Stat/Privacy/LaplaceMechanism.lean:584
laplacePi_integrable_euclidean_norm theorem — The Euclidean norm of finitely many independent centered Laplace draws has a finite expectation whenever their common scale is positive.

hypotheses

ι :

Type*
Fintype ι

b :

ℝ

hb :

0 < b

conclusion

Integrable (fun w : ι → ℝ => sqrt (∑ i : ι, (w i) ^ 2)) (Measure.pi fun _ : ι => laplaceMeasure b)

Proof (Lean source)

theorem laplacePi_integrable_euclidean_norm {ι : Type*} [Fintype ι] (b : ℝ) (hb : 0 < b) : Integrable (fun w : ι → ℝ => sqrt (∑ i : ι, (w i) ^ 2)) (Measure.pi fun _ : ι => laplaceMeasure b) := by letI : IsProbabilityMeasure (laplaceMeasure b) := laplaceMeasure_isProbabilityMeasure b hb have hcoord (i : ι) : Integrable (fun w : ι → ℝ => |w i|) (Measure.pi fun _ : ι => laplaceMeasure b) := integrable_comp_eval (laplaceMeasure_integrable_abs b hb) have hsum : Integrable (fun w : ι → ℝ => ∑ i : ι, |w i|) (Measure.pi fun _ : ι => laplaceMeasure b) := integrable_finset_sum _ fun i _ => hcoord i have hcontinuous : Continuous (fun w : ι → ℝ => sqrt (∑ i : ι, (w i) ^ 2)) := Real.continuous_sqrt.comp (continuous_finset_sum _ fun i _ => (continuous_apply i).pow 2) refine hsum.mono' hcontinuous.aestronglyMeasurable (ae_of_all _ fun w => ?_) rw [Real.norm_of_nonneg (Real.sqrt_nonneg _)] exact sqrt_sum_sq_le_sum_abs w

Causalean.Stat.Privacy.laplacePi_integrable_euclidean_norm · Causalean/Stat/Privacy/LaplaceMechanism.lean:621