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.

Binary 17 core · 16 supporting · 2 submodules Binary-input locally private experiments, their sharp scalar Fisher-information bound, and the randomized-response equality case. Staircase 32 core · 25 supporting · 8 submodules Measurable fourteen-ray staircase refinements for four-input locally private Markov kernels.

LaplaceMechanism 7 core · 11 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★ 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:33

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:37

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:155

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:196 · 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:254

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:382 · uses laplaceMechPi

theorem approx_dp_postprocess reviewed

Causalean.Stat.Privacy

A fixed-pair approximate measure bound survives deterministic vector-to-scalar post-processing. Given an event-measure bound with allowance δ between the vector-valued measures M d and M d', pushing both measures forward by a measurable scalar map f preserves the same bound and allowance. This raw lemma does not assert probability normalization or quantify over an adjacency relation.

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 approx_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.approx_dp_postprocess · Causalean/Stat/Privacy/LaplaceMechanism.lean:476

11 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:47
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:111
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:130
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:187
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:262
pure_dp_implies_approx_dp theorem — A pure measure bound implies the corresponding approximate measure bound. Given an event-measure bound between M d and M d', adding any nonnegative allowance $\delta$ preserves the inequality with that allowance. This raw fixed-pair lemma does not assert that M consists of probability measures.

hypotheses

D :

Sort u_2
shared

α :

Type*
MeasurableSpace α

M :

D → Measure α

d d' :

D

ε δ :

ℝ

hpure :

∀ s
if
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:446
pure_dp_postprocess theorem — A fixed-pair pure measure bound survives deterministic vector-to-scalar post-processing. Given an event-measure bound between the vector-valued measures M d and M d', pushing both measures forward by a measurable scalar map f preserves the same bound. This raw lemma does not assert probability normalization or quantify over an adjacency relation.

hypotheses

D ι :

Type*

M :

D → Measure (ι → ℝ)

d d' :

D

ε :

ℝ

hM :

∀ s
if
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:459
laplaceMeasure_integrable_abs theorem — The absolute value of a centered Laplace draw has a finite expectation at every positive scale.

hypotheses

b :

ℝ

hb :

0 |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:534
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 : ℝ) * Gamma (2 : ℝ) := Real.integral_rpow_mul_exp_neg_mul_Ioi (by norm_num) (one_div_pos.mpr hb) _ = b ^ 2 := by rw [show 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:544
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 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:585
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 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:622

LaplaceKernel 2 core · 2 supporting The existing finite-coordinate mechanism is packaged as a Markov kernel for any measurable query and positive scale. ★ measurable_laplaceMechPi

Measurable finite-product Laplace mechanism

The existing finite-coordinate mechanism is packaged as a Markov kernel for any measurable query and positive scale. Its value at each input is exactly the primary library's mechanism, so measure-kernel composition applies directly.

theorem measurable_laplaceMechPi reviewed

Causalean.Stat.Privacy

At a real scale with a positive-scale certificate, a query and its measurability certificate, the finite-product Laplace release depends measurably on its input.

Formal statement

hypotheses

D :

Type u_1

shared

ι :

Type u_2

shared

b :

ℝ

hb :

0 < b

q :

D → ι → ℝ

hq :

Measurable q

conclusion

Measurable (laplaceMechPi b q)

Proof (Lean source)

@[fun_prop] theorem measurable_laplaceMechPi (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (hq : Measurable q) : Measurable (laplaceMechPi b q) := by let : IsProbabilityMeasure (laplaceMeasure b) := laplaceMeasure_isProbabilityMeasure b hb let noise : Kernel D (ι → ℝ) := Kernel.const D (Measure.pi fun _ : ι => laplaceMeasure b) let add : (ι → ℝ) × (ι → ℝ) → (ι → ℝ) := fun p => p.2 + p.1 have hadd : Measurable add := measurable_snd.add measurable_fst let release := ((Kernel.deterministic q hq).prod noise).map add have hrelease (d : D) : release d = laplaceMechPi b q d := by rw [Kernel.map_apply _ hadd, Kernel.prod_apply, Kernel.deterministic_apply, Kernel.const_apply, Measure.dirac_prod, Measure.map_map hadd measurable_prodMk_left] rfl have heq : (fun d => release d) = laplaceMechPi b q := funext hrelease rw [← heq] exact release.measurable

Causalean.Stat.Privacy.measurable_laplaceMechPi · Causalean/Stat/Privacy/LaplaceKernel.lean:22 · uses laplaceMechPi

def laplaceMechPiKernel reviewed

Causalean.Stat.Privacy

At a real scale with a positive-scale certificate, a query and its measurability certificate, the finite-coordinate release defines a kernel with the existing mechanism's inputwise measures.

Definition (Lean source)

parameters

D :

Type u_1

shared

ι :

Type u_2

shared

b :

ℝ

hb :

0 < b

q :

D → ι → ℝ

hq :

Measurable q

def

laplaceMechPiKernel b hb q hq :

Kernel D (ι → ℝ)

given by

clause 1

toFun := laplaceMechPi b q

clause 2

measurable' := measurable_laplaceMechPi b hb q hq

Causalean.Stat.Privacy.laplaceMechPiKernel · Causalean/Stat/Privacy/LaplaceKernel.lean:49

2 supporting declarations (lemmas, instances)

laplaceMechPiKernel_apply theorem — At a real scale with a positive-scale certificate, a query, its measurability certificate, and an input, the kernel equals the existing Laplace mechanism at that input.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 < b

q :

D → ι → ℝ

hq :

Measurable q

d :

D

conclusion

laplaceMechPiKernel b hb q hq d = laplaceMechPi b q d

Proof (Lean source)

@[simp] theorem laplaceMechPiKernel_apply (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (hq : Measurable q) (d : D) : laplaceMechPiKernel b hb q hq d = laplaceMechPi b q d := rfl

Causalean.Stat.Privacy.laplaceMechPiKernel_apply · Causalean/Stat/Privacy/LaplaceKernel.lean:57
laplaceMechPiKernel_isMarkovKernel instance — At a real scale with a positive-scale certificate, a query and its measurability certificate, the resulting kernel is a Markov kernel.

parameters

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 laplaceMechPi_isProbabilityMeasure b hb q d⟩

Causalean.Stat.Privacy.laplaceMechPiKernel_isMarkovKernel · Causalean/Stat/Privacy/LaplaceKernel.lean:65

LaplaceCoordinateMoments 1 core · 8 supporting Every centered coordinate of the existing finite-product mechanism has the scalar Laplace law, zero mean, and exact squared error. ★ laplaceMechPi_integral_coord_sub_sq

Finite-coordinate Laplace release moments

Every centered coordinate of the existing finite-product mechanism has the scalar Laplace law, zero mean, and exact squared error. An arbitrary real center yields query displacement squared plus twice the squared noise scale. The index type is any finite type, including Fin 2.

theorem laplaceMechPi_integral_coord_sub_sq reviewed

Causalean.Stat.Privacy

At a real scale with a positive-scale certificate, a query, an input, a coordinate, and a real center, the released coordinate's squared displacement has expectation equal to the query's squared displacement plus twice the squared scale.

Formal statement

hypotheses

D :

Type u_1

shared

ι :

Type u_2

shared

b :

ℝ

hb :

0 < b

q :

D → ι → ℝ

d :

i :

c :

ℝ

conclusion

∫ y, (y i - c) ^ 2 ∂laplaceMechPi b q d = (q d i - c) ^ 2 + 2 * b ^ 2

Proof (Lean source)

theorem laplaceMechPi_integral_coord_sub_sq (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (d : D) (i : ι) (c : ℝ) : ∫ y, (y i - c) ^ 2 ∂laplaceMechPi b q d = (q d i - c) ^ 2 + 2 * b ^ 2 := by let := laplaceMechPi_isProbabilityMeasure b hb q d have hsq := laplaceMechPi_integrable_centered_coord_sq b hb q d i have hlin := (laplaceMechPi_integrable_centered_coord b hb q d i).const_mul (2 * (q d i - c)) have hconst : Integrable (fun _ : ι → ℝ => (q d i - c) ^ 2) (laplaceMechPi b q d) := integrable_const _ have hexpand : (fun y : ι → ℝ => (y i - c) ^ 2) = fun y => ((y i - q d i) ^ 2 + 2 * (q d i - c) * (y i - q d i)) + (q d i - c) ^ 2 := by funext y ring have hsum : Integrable (fun y : ι → ℝ => (y i - q d i) ^ 2 + 2 * (q d i - c) * (y i - q d i)) (laplaceMechPi b q d) := hsq.add hlin rw [hexpand, integral_add hsum hconst, integral_add hsq hlin, integral_const_mul, laplaceMechPi_integral_centered_coord_sq b hb q d i, laplaceMechPi_integral_centered_coord b hb q d i, integral_const] simp ring

Causalean.Stat.Privacy.laplaceMechPi_integral_coord_sub_sq · Causalean/Stat/Privacy/LaplaceCoordinateMoments.lean:155 · uses laplaceMechPi

8 supporting declarations (lemmas, instances)

laplaceMechPi_map_centered_coord theorem — At a real scale with a positive-scale certificate, a query, an input, and a coordinate, subtracting the query from the released coordinate gives exactly the centered scalar Laplace law.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 y i - q d i) = laplaceMeasure b

Proof (Lean source)

theorem laplaceMechPi_map_centered_coord (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (d : D) (i : ι) : (laplaceMechPi b q d).map (fun y => y i - q d i) = laplaceMeasure b := by let : IsProbabilityMeasure (laplaceMeasure b) := laplaceMeasure_isProbabilityMeasure b hb rw [laplaceMechPi, Measure.map_map (by fun_prop) (by fun_prop)] have hcancel : (fun y : ι → ℝ => y i - q d i) ∘ (fun z => z + q d) = Function.eval i := by funext z simp [Pi.add_apply] rw [hcancel] exact (measurePreserving_eval (fun _ : ι => laplaceMeasure b) i).map_eq

Causalean.Stat.Privacy.laplaceMechPi_map_centered_coord · Causalean/Stat/Privacy/LaplaceCoordinateMoments.lean:23
laplaceMechPi_integrable_centered_coord theorem — At a real scale with a positive-scale certificate, a query, an input, and a coordinate, the released-coordinate error is integrable.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 y i - q d i) (laplaceMechPi b q d)

Proof (Lean source)

theorem laplaceMechPi_integrable_centered_coord (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (d : D) (i : ι) : Integrable (fun y => y i - q d i) (laplaceMechPi b q d) := by have h : Integrable (fun x : ℝ => x) ((laplaceMechPi b q d).map (fun y => y i - q d i)) := by rw [laplaceMechPi_map_centered_coord b hb q d i] exact laplaceMeasure_integrable_id b hb exact (integrable_map_measure h.aestronglyMeasurable ((measurable_pi_apply i).sub measurable_const).aemeasurable).mp h

Causalean.Stat.Privacy.laplaceMechPi_integrable_centered_coord · Causalean/Stat/Privacy/LaplaceCoordinateMoments.lean:50
laplaceMechPi_integral_centered_coord theorem — At a real scale with a positive-scale certificate, a query, an input, and a coordinate, the released-coordinate error has mean zero.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 < b

q :

D → ι → ℝ

d :

D

i :

ι

conclusion

∫ y, y i - q d i ∂laplaceMechPi b q d = 0

Proof (Lean source)

theorem laplaceMechPi_integral_centered_coord (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (d : D) (i : ι) : ∫ y, y i - q d i ∂laplaceMechPi b q d = 0 := by have hmap := integral_map (μ := laplaceMechPi b q d) (φ := fun y => y i - q d i) (f := fun x : ℝ => x) ((measurable_pi_apply i).sub measurable_const).aemeasurable (by fun_prop) rw [laplaceMechPi_map_centered_coord b hb q d i, laplaceMeasure_integral_id b hb] at hmap exact hmap.symm

Causalean.Stat.Privacy.laplaceMechPi_integral_centered_coord · Causalean/Stat/Privacy/LaplaceCoordinateMoments.lean:68
laplaceMechPi_integrable_centered_coord_sq theorem — At a real scale with a positive-scale certificate, a query, an input, and a coordinate, the squared released-coordinate error is integrable.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 (y i - q d i) ^ 2) (laplaceMechPi b q d)

Proof (Lean source)

theorem laplaceMechPi_integrable_centered_coord_sq (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (d : D) (i : ι) : Integrable (fun y => (y i - q d i) ^ 2) (laplaceMechPi b q d) := by have h : Integrable (fun x : ℝ => x ^ 2) ((laplaceMechPi b q d).map (fun y => y i - q d i)) := by rw [laplaceMechPi_map_centered_coord b hb q d i] exact laplaceMeasure_integrable_sq b hb exact (integrable_map_measure h.aestronglyMeasurable ((measurable_pi_apply i).sub measurable_const).aemeasurable).mp h

Causalean.Stat.Privacy.laplaceMechPi_integrable_centered_coord_sq · Causalean/Stat/Privacy/LaplaceCoordinateMoments.lean:85
laplaceMechPi_integral_centered_coord_sq theorem — At a real scale with a positive-scale certificate, a query, an input, and a coordinate, the squared released-coordinate error has expectation exactly twice the squared scale.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 < b

q :

D → ι → ℝ

d :

D

i :

ι

conclusion

∫ y, (y i - q d i) ^ 2 ∂laplaceMechPi b q d = 2 * b ^ 2

Proof (Lean source)

theorem laplaceMechPi_integral_centered_coord_sq (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (d : D) (i : ι) : ∫ y, (y i - q d i) ^ 2 ∂laplaceMechPi b q d = 2 * b ^ 2 := by have hmap := integral_map (μ := laplaceMechPi b q d) (φ := fun y => y i - q d i) (f := fun x : ℝ => x ^ 2) ((measurable_pi_apply i).sub measurable_const).aemeasurable (by fun_prop) rw [laplaceMechPi_map_centered_coord b hb q d i, laplaceMeasure_integral_sq b hb] at hmap exact hmap.symm

Causalean.Stat.Privacy.laplaceMechPi_integral_centered_coord_sq · Causalean/Stat/Privacy/LaplaceCoordinateMoments.lean:102
laplaceMechPi_lintegral_centered_coord_sq theorem — At a real scale with a positive-scale certificate, a query, an input, and a coordinate, the squared released-coordinate error has nonnegative extended expectation exactly twice the squared scale.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 < b

q :

D → ι → ℝ

d :

D

i :

ι

conclusion

∫⁻ y, ofReal ((y i - q d i) ^ 2) ∂laplaceMechPi b q d = ofReal (2 * b ^ 2)

Proof (Lean source)

theorem laplaceMechPi_lintegral_centered_coord_sq (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (d : D) (i : ι) : ∫⁻ y, ofReal ((y i - q d i) ^ 2) ∂laplaceMechPi b q d = ofReal (2 * b ^ 2) := by rw [← ofReal_integral_eq_lintegral_ofReal (laplaceMechPi_integrable_centered_coord_sq b hb q d i) (ae_of_all _ fun y => sq_nonneg (y i - q d i)), laplaceMechPi_integral_centered_coord_sq b hb q d i]

Causalean.Stat.Privacy.laplaceMechPi_lintegral_centered_coord_sq · Causalean/Stat/Privacy/LaplaceCoordinateMoments.lean:119
laplaceMechPi_integrable_coord_sub_sq theorem — At a real scale with a positive-scale certificate, a query, an input, a coordinate, and a real center, the released coordinate's squared displacement from that center is integrable.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 (y i - c) ^ 2) (laplaceMechPi b q d)

Proof (Lean source)

theorem laplaceMechPi_integrable_coord_sub_sq (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (d : D) (i : ι) (c : ℝ) : Integrable (fun y => (y i - c) ^ 2) (laplaceMechPi b q d) := by let := laplaceMechPi_isProbabilityMeasure b hb q d have hsq := laplaceMechPi_integrable_centered_coord_sq b hb q d i have hlin := (laplaceMechPi_integrable_centered_coord b hb q d i).const_mul (2 * (q d i - c)) have hconst : Integrable (fun _ : ι → ℝ => (q d i - c) ^ 2) (laplaceMechPi b q d) := integrable_const _ refine ((hsq.add hlin).add hconst).congr (ae_of_all _ fun y => ?_) dsimp ring

Causalean.Stat.Privacy.laplaceMechPi_integrable_coord_sub_sq · Causalean/Stat/Privacy/LaplaceCoordinateMoments.lean:131
laplaceMechPi_lintegral_coord_sub_sq theorem — At a real scale with a positive-scale certificate, a query, an input, a coordinate, and a real center, the released coordinate's squared displacement has the corresponding exact nonnegative extended moment.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 < b

q :

D → ι → ℝ

d :

D

i :

ι

c :

ℝ

conclusion

∫⁻ y, ofReal ((y i - c) ^ 2) ∂laplaceMechPi b q d
= ofReal ((q d i - c) ^ 2 + 2 * b ^ 2)

Proof (Lean source)

theorem laplaceMechPi_lintegral_coord_sub_sq (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (d : D) (i : ι) (c : ℝ) : ∫⁻ y, ofReal ((y i - c) ^ 2) ∂laplaceMechPi b q d = ofReal ((q d i - c) ^ 2 + 2 * b ^ 2) := by rw [← ofReal_integral_eq_lintegral_ofReal (laplaceMechPi_integrable_coord_sub_sq b hb q d i c) (ae_of_all _ fun y => sq_nonneg (y i - c)), laplaceMechPi_integral_coord_sub_sq b hb q d i c]

Causalean.Stat.Privacy.laplaceMechPi_lintegral_coord_sub_sq · Causalean/Stat/Privacy/LaplaceCoordinateMoments.lean:190

LaplaceKernelMoments 1 core · 4 supporting A probability input law and a measurable query with a square-integrable selected coordinate give an integrable released-coordinate square and the exact decomposition into input squared displacement plus 2 * b^2. ★ laplaceMechPiKernel_integral_coord_sub_sq

Exact moments under randomized inputs

A probability input law and a measurable query with a square-integrable selected coordinate give an integrable released-coordinate square and the exact decomposition into input squared displacement plus 2 * b^2. Both measure-kernel composition and joint input-release cross terms are covered. The nonnegative extended identity also holds without any moment assumption.

theorem laplaceMechPiKernel_integral_coord_sub_sq reviewed

Causalean.Stat.Privacy

At a real scale with a positive-scale certificate, a query, its measurability certificate, a probability input law, a coordinate, a square-integrability certificate for that coordinate, and a real center, the release's squared-displacement expectation equals the input squared displacement plus exactly twice the squared noise scale.

Formal statement

hypotheses

D :

Type u_1

shared

ι :

Type u_2

shared

b :

ℝ

hb :

0 < b

q :

D → ι → ℝ

hq :

Measurable q

μ :

Measure D

IsProbabilityMeasure μ

i :

hqsq :

Integrable (fun d => (q d i) ^ 2) μ

c :

ℝ

conclusion

∫ y, (y i - c) ^ 2 ∂(laplaceMechPiKernel b hb q hq ∘ₘ μ)

= (∫ d, (q d i - c) ^ 2 ∂μ) + 2 * b ^ 2

Proof (Lean source)

theorem laplaceMechPiKernel_integral_coord_sub_sq (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (hq : Measurable q) (μ : Measure D) [IsProbabilityMeasure μ] (i : ι) (hqsq : Integrable (fun d => (q d i) ^ 2) μ) (c : ℝ) : ∫ y, (y i - c) ^ 2 ∂(laplaceMechPiKernel b hb q hq ∘ₘ μ) = (∫ d, (q d i - c) ^ 2 ∂μ) + 2 * b ^ 2 := by have hL2 : MemLp (fun d => q d i) 2 μ := (memLp_two_iff_integrable_sq ((measurable_pi_apply i).comp hq).aestronglyMeasurable).mpr hqsq have hin : Integrable (fun d => (q d i - c) ^ 2) μ := (hL2.sub (memLp_const c)).integrable_sq have hout := laplaceMechPiKernel_integrable_coord_sub_sq b hb q hq μ i hqsq c have hid := laplaceMechPiKernel_lintegral_coord_sub_sq b hb q hq μ i c rw [← ofReal_integral_eq_lintegral_ofReal hout (ae_of_all _ fun y => sq_nonneg (y i - c)), ← ofReal_integral_eq_lintegral_ofReal hin (ae_of_all _ fun d => sq_nonneg (q d i - c)), ← ENNReal.ofReal_add (integral_nonneg fun d => sq_nonneg (q d i - c)) (mul_nonneg (show (0 : ℝ) ≤ 2 by norm_num) (sq_nonneg b))] at hid exact (ENNReal.ofReal_eq_ofReal_iff (integral_nonneg (μ := laplaceMechPiKernel b hb q hq ∘ₘ μ) fun y : ι → ℝ => sq_nonneg (y i - c)) (add_nonneg (integral_nonneg fun d => sq_nonneg (q d i - c)) (mul_nonneg (show (0 : ℝ) ≤ 2 by norm_num) (sq_nonneg b)))).mp hid

Causalean.Stat.Privacy.laplaceMechPiKernel_integral_coord_sub_sq · Causalean/Stat/Privacy/LaplaceKernelMoments.lean:100 · uses laplaceMechPiKernel

4 supporting declarations (lemmas, instances)

laplaceMechPiKernel_lintegral_coord_sub_sq theorem — At a real scale with a positive-scale certificate, a query, its measurability certificate, a probability input law, a coordinate, and a real center, mixing the release gives the exact nonnegative extended squared-displacement identity, even for infinite input moments.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 < b

q :

D → ι → ℝ

hq :

Measurable q

μ :

Measure D
IsProbabilityMeasure μ

i :

ι

c :

ℝ

conclusion

∫⁻ y, ofReal ((y i - c) ^ 2) ∂(laplaceMechPiKernel b hb q hq ∘ₘ μ)
= (∫⁻ d, ofReal ((q d i - c) ^ 2) ∂μ) + ofReal (2 * b ^ 2)

Proof (Lean source)

theorem laplaceMechPiKernel_lintegral_coord_sub_sq (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (hq : Measurable q) (μ : Measure D) [IsProbabilityMeasure μ] (i : ι) (c : ℝ) : ∫⁻ y, ofReal ((y i - c) ^ 2) ∂(laplaceMechPiKernel b hb q hq ∘ₘ μ) = (∫⁻ d, ofReal ((q d i - c) ^ 2) ∂μ) + ofReal (2 * b ^ 2) := by have hy : Measurable (fun y : ι → ℝ => ofReal ((y i - c) ^ 2)) := (((measurable_pi_apply i).sub measurable_const).pow_const 2).ennreal_ofReal have hd : Measurable (fun d => ofReal ((q d i - c) ^ 2)) := ((((measurable_pi_apply i).comp hq).sub measurable_const).pow_const 2).ennreal_ofReal change ∫⁻ y, ofReal ((y i - c) ^ 2) ∂μ.bind (laplaceMechPiKernel b hb q hq) = _ rw [Measure.lintegral_bind (laplaceMechPiKernel b hb q hq).measurable.aemeasurable hy.aemeasurable] simp_rw [laplaceMechPiKernel_apply, laplaceMechPi_lintegral_coord_sub_sq b hb q, ENNReal.ofReal_add (sq_nonneg (q _ i - c)) (mul_nonneg (show (0 : ℝ) ≤ 2 by norm_num) (sq_nonneg b))] rw [lintegral_add_left hd] simp

Causalean.Stat.Privacy.laplaceMechPiKernel_lintegral_coord_sub_sq · Causalean/Stat/Privacy/LaplaceKernelMoments.lean:25
laplaceMechPiKernel_integrable_coord_sub_sq theorem — At a real scale with a positive-scale certificate, a query, its measurability certificate, a probability input law, a coordinate, a square-integrability certificate for that coordinate, and a real center, the mixed release has an integrable squared displacement.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 (q d i) ^ 2) μ

c :

ℝ

conclusion

Integrable (fun y => (y i - c) ^ 2) (laplaceMechPiKernel b hb q hq ∘ₘ μ)

Proof (Lean source)

theorem laplaceMechPiKernel_integrable_coord_sub_sq (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (hq : Measurable q) (μ : Measure D) [IsProbabilityMeasure μ] (i : ι) (hqsq : Integrable (fun d => (q d i) ^ 2) μ) (c : ℝ) : Integrable (fun y => (y i - c) ^ 2) (laplaceMechPiKernel b hb q hq ∘ₘ μ) := by have hL2 : MemLp (fun d => q d i) 2 μ := (memLp_two_iff_integrable_sq ((measurable_pi_apply i).comp hq).aestronglyMeasurable).mpr hqsq have hin : Integrable (fun d => (q d i - c) ^ 2) μ := (hL2.sub (memLp_const c)).integrable_sq refine ⟨(show Measurable (fun y : ι → ℝ => (y i - c) ^ 2) from ((measurable_pi_apply i).sub measurable_const).pow_const 2).aestronglyMeasurable, ?_⟩ apply (hasFiniteIntegral_iff_ofReal (ae_of_all _ fun y : ι → ℝ => sq_nonneg (y i - c))).mpr rw [laplaceMechPiKernel_lintegral_coord_sub_sq b hb q hq μ i c] exact ENNReal.add_lt_top.mpr ⟨(hasFiniteIntegral_iff_ofReal (ae_of_all _ fun d => sq_nonneg (q d i - c))).mp hin.hasFiniteIntegral, ENNReal.ofReal_lt_top⟩

Causalean.Stat.Privacy.laplaceMechPiKernel_integrable_coord_sub_sq · Causalean/Stat/Privacy/LaplaceKernelMoments.lean:60
laplaceMechPiKernel_integrable_cross theorem — At a real scale with a positive-scale certificate, a query, its measurability certificate, a probability input law, a coordinate, a square-integrability certificate for that coordinate, and a real center, the displacement-error cross term is integrable under the joint input-release law.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 (q d i) ^ 2) μ

c :

ℝ

conclusion

Integrable (fun p : D × (ι → ℝ) => (q p.1 i - c) * (p.2 i - q p.1 i)) (μ ⊗ₘ laplaceMechPiKernel b hb q hq)

Proof (Lean source)

theorem laplaceMechPiKernel_integrable_cross (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (hq : Measurable q) (μ : Measure D) [IsProbabilityMeasure μ] (i : ι) (hqsq : Integrable (fun d => (q d i) ^ 2) μ) (c : ℝ) : Integrable (fun p : D × (ι → ℝ) => (q p.1 i - c) * (p.2 i - q p.1 i)) (μ ⊗ₘ laplaceMechPiKernel b hb q hq) := by have hL2 : MemLp (fun d => q d i) 2 μ := (memLp_two_iff_integrable_sq ((measurable_pi_apply i).comp hq).aestronglyMeasurable).mpr hqsq have hin : Integrable (fun d => q d i - c) μ := (hL2.sub (memLp_const c)).integrable (by norm_num) have hf : Measurable (fun p : D × (ι → ℝ) => (q p.1 i - c) * (p.2 i - q p.1 i)) := (((measurable_pi_apply i).comp (hq.comp measurable_fst)).sub measurable_const).mul (((measurable_pi_apply i).comp measurable_snd).sub ((measurable_pi_apply i).comp (hq.comp measurable_fst))) apply (Measure.integrable_compProd_iff hf.aestronglyMeasurable).mpr constructor · exact ae_of_all _ fun d => (laplaceMechPi_integrable_centered_coord b hb q d i).const_mul (q d i - c) · have habs (d : D) : ∫ y, |y i - q d i| ∂laplaceMechPi b q d = b := by have hmap := integral_map (μ := laplaceMechPi b q d) (φ := fun y => y i - q d i) (f := fun x : ℝ => |x|) ((measurable_pi_apply i).sub measurable_const).aemeasurable (by fun_prop) rw [laplaceMechPi_map_centered_coord b hb q d i, laplaceMeasure_integral_abs b hb] at hmap exact hmap.symm simpa only [laplaceMechPiKernel_apply, norm_mul, Real.norm_eq_abs, integral_const_mul, habs] using hin.norm.mul_const b

Causalean.Stat.Privacy.laplaceMechPiKernel_integrable_cross · Causalean/Stat/Privacy/LaplaceKernelMoments.lean:140
laplaceMechPiKernel_integral_cross theorem — At a real scale with a positive-scale certificate, a query, its measurability certificate, a probability input law, a coordinate, a square-integrability certificate for that coordinate, and a real center, the displacement-error cross term has integral zero.

hypotheses

D :

Type u_1
shared

ι :

Type u_2
shared

b :

ℝ

hb :

0 (q d i) ^ 2) μ

c :

ℝ

conclusion

∫ p : D × (ι → ℝ), (q p.1 i - c) * (p.2 i - q p.1 i) ∂(μ ⊗ₘ laplaceMechPiKernel b hb q hq)
= 0

Proof (Lean source)

theorem laplaceMechPiKernel_integral_cross (b : ℝ) (hb : 0 < b) (q : D → ι → ℝ) (hq : Measurable q) (μ : Measure D) [IsProbabilityMeasure μ] (i : ι) (hqsq : Integrable (fun d => (q d i) ^ 2) μ) (c : ℝ) : ∫ p : D × (ι → ℝ), (q p.1 i - c) * (p.2 i - q p.1 i) ∂(μ ⊗ₘ laplaceMechPiKernel b hb q hq) = 0 := by rw [Measure.integral_compProd (laplaceMechPiKernel_integrable_cross b hb q hq μ i hqsq c)] simp only [laplaceMechPiKernel_apply, integral_const_mul, laplaceMechPi_integral_centered_coord b hb q, mul_zero, integral_zero]

Causalean.Stat.Privacy.laplaceMechPiKernel_integral_cross · Causalean/Stat/Privacy/LaplaceKernelMoments.lean:192

LaplaceMean 1 core · 2 supporting Reflection invariance and the exact zero mean of the existing density-defined Laplace measure. ★ laplaceMeasure_integral_id

Centered Laplace mean

Reflection invariance and the exact zero mean of the existing density-defined Laplace measure. Absolute integrability is reused from the primary library. This file is independent of the second-moment proof chain.

theorem laplaceMeasure_integral_id reviewed

Causalean.Stat.Privacy

At a real scale with a positive-scale certificate, a centered Laplace draw has mean zero.

Formal statement

hypotheses

b :

ℝ

hb :

0 < b

conclusion

∫ x : ℝ, x ∂laplaceMeasure b = 0

Proof (Lean source)

theorem laplaceMeasure_integral_id (b : ℝ) (hb : 0 < b) : ∫ x : ℝ, x ∂laplaceMeasure b = 0 := by have hmeas : AEStronglyMeasurable (fun x : ℝ => x) ((laplaceMeasure b).map (fun x : ℝ => -x)) := by rw [laplaceMeasure_map_neg b] exact (laplaceMeasure_integrable_id b hb).aestronglyMeasurable have hreflection := integral_map (μ := laplaceMeasure b) (φ := fun x : ℝ => -x) (by fun_prop) hmeas rw [laplaceMeasure_map_neg b, integral_neg] at hreflection linarith

Causalean.Stat.Privacy.laplaceMeasure_integral_id · Causalean/Stat/Privacy/LaplaceMean.lean:46 · uses laplaceMeasure

2 supporting declarations (lemmas, instances)

laplaceMeasure_integrable_id theorem — At a real scale with a positive-scale certificate, a centered Laplace draw has an integrable signed value.

hypotheses

b :

ℝ

hb :

0 x) (laplaceMeasure b)

Proof (Lean source)

theorem laplaceMeasure_integrable_id (b : ℝ) (hb : 0 < b) : Integrable (fun x : ℝ => x) (laplaceMeasure b) := by exact (laplaceMeasure_integrable_abs b hb).mono' (by fun_prop) (ae_of_all _ fun x => by simp)

Causalean.Stat.Privacy.laplaceMeasure_integrable_id · Causalean/Stat/Privacy/LaplaceMean.lean:18
laplaceMeasure_map_neg theorem — At a real scale, reflecting the centered Laplace measure about zero preserves that measure.

hypotheses

b :

ℝ

conclusion

(laplaceMeasure b).map (fun x : ℝ => -x) = laplaceMeasure b

Proof (Lean source)

theorem laplaceMeasure_map_neg (b : ℝ) : (laplaceMeasure b).map (fun x : ℝ => -x) = laplaceMeasure b := by ext s hs rw [Measure.map_apply (by fun_prop) hs, laplaceMeasure, withDensity_apply _ (hs.preimage (by fun_prop)), withDensity_apply _ hs] calc (∫⁻ x in (fun x : ℝ => -x) ⁻¹' s, ofReal (laplacePDF b x)) = ∫⁻ x in (fun x : ℝ => -x) ⁻¹' s, ofReal (laplacePDF b (-x)) := by simp only [laplacePDF, abs_neg] _ = ∫⁻ x in s, ofReal (laplacePDF b x) ∂(volume.map (fun x : ℝ => -x)) := (setLIntegral_map hs (measurable_laplacePDF b).ennreal_ofReal (by fun_prop)).symm _ = _ := by rw [Measure.map_neg_eq_self]

Causalean.Stat.Privacy.laplaceMeasure_map_neg · Causalean/Stat/Privacy/LaplaceMean.lean:25

LaplaceSecondMoment 1 core · 4 supporting The density-weighted square is integrable, and its integral is exactly twice the squared scale. ★ laplaceMeasure_integral_sq

Exact Laplace second moments

The density-weighted square is integrable, and its integral is exactly twice the squared scale. Bochner and nonnegative extended-integral interfaces are provided for the existing laplaceMeasure; no new distribution is defined.

theorem laplaceMeasure_integral_sq reviewed

Causalean.Stat.Privacy

At a real scale with a positive-scale certificate, a centered Laplace draw has second moment exactly twice the squared scale.

Formal statement

hypotheses

b :

ℝ

hb :

0 < b

conclusion

∫ x : ℝ, x ^ 2 ∂laplaceMeasure b = 2 * b ^ 2

Proof (Lean source)

theorem laplaceMeasure_integral_sq (b : ℝ) (hb : 0 < b) : ∫ x : ℝ, x ^ 2 ∂laplaceMeasure b = 2 * b ^ 2 := by have hnonneg (x : ℝ) : 0 ≤ laplacePDF b x := by unfold laplacePDF positivity 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 (hnonneg _), smul_eq_mul] let f : ℝ → ℝ := fun x => (2 * b)⁻¹ * (x ^ 2 * exp (-x / b)) rw [show (fun x : ℝ => laplacePDF b x * x ^ 2) = fun x => f |x| by funext x simp only [f, laplacePDF, sq_abs] ring, integral_comp_abs] have hright : (∫ x in Ioi (0 : ℝ), f x) = (2 * b)⁻¹ * (2 * b ^ 3) := by rw [show f = fun x => (2 * b)⁻¹ * (x ^ 2 * exp (-x / b)) by rfl, integral_const_mul, integral_sq_mul_exp_neg_div_Ioi b hb] rw [hright] field_simp [hb.ne']

Causalean.Stat.Privacy.laplaceMeasure_integral_sq · Causalean/Stat/Privacy/LaplaceSecondMoment.lean:105 · uses laplaceMeasure

4 supporting declarations (lemmas, instances)

integrable_sq_mul_laplacePDF theorem — At a real scale with a positive-scale certificate, the square times the centered Laplace density is integrable with respect to Lebesgue measure.

hypotheses

b :

ℝ

hb :

0 x ^ 2 * laplacePDF b x)

Proof (Lean source)

theorem integrable_sq_mul_laplacePDF (b : ℝ) (hb : 0 < b) : Integrable (fun x : ℝ => x ^ 2 * laplacePDF b x) := by let f : ℝ → ℝ := fun x => (2 * b)⁻¹ * (x ^ 2 * exp (-x / b)) have hright : IntegrableOn f (Ioi 0) := by have hbase := Real.GammaIntegral_convergent (s := (3 : ℝ)) (by norm_num) have hscaled : IntegrableOn (fun x : ℝ => exp (-(1 / b * x)) * (1 / b * x) ^ ((3 : ℝ) - 1)) (Ioi 0) := (integrableOn_Ioi_comp_mul_left_iff (fun x : ℝ => exp (-x) * x ^ ((3 : ℝ) - 1)) 0 (one_div_pos.mpr hb)).mpr (by simpa using hbase) have hs : IntegrableOn (fun x : ℝ => (2 * b)⁻¹ * (b ^ 2 * (exp (-(1 / b * x)) * (1 / b * x) ^ ((3 : ℝ) - 1)))) (Ioi 0) := (hscaled.const_mul (b ^ 2)).const_mul (2 * b)⁻¹ refine hs.congr_fun ?_ measurableSet_Ioi intro x hx simp only [f, show (3 : ℝ) - 1 = 2 by norm_num, Real.rpow_two] rw [show -(1 / b * x) = -x / b by ring] field_simp [hb.ne'] have hright_abs : IntegrableOn (fun x => f |x|) (Ioi 0) := by refine hright.congr_fun ?_ measurableSet_Ioi intro x hx change f x = f |x| rw [abs_of_pos (by simpa only [mem_Ioi] using hx)] have hall : Integrable (fun x => f |x|) := by have hleft : IntegrableOn (fun x => f |x|) (Iic 0) := by rw [← Measure.map_neg_eq_self (volume : Measure ℝ)] let m : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).measurableEmbedding rw [m.integrableOn_map_iff] simp_rw [Function.comp_def, abs_neg, neg_preimage, neg_Iic, neg_zero] exact mpr integrableOn_Ici_iff_integrableOn_Ioi hright_abs rw [← integrableOn_univ] simpa only [Iic_union_Ioi] using hleft.union hright_abs refine hall.congr (ae_of_all _ fun x => ?_) simp only [f, laplacePDF, sq_abs] ring

Causalean.Stat.Privacy.integrable_sq_mul_laplacePDF · Causalean/Stat/Privacy/LaplaceSecondMoment.lean:19
integral_sq_mul_exp_neg_div_Ioi theorem — At a real scale with a positive-scale certificate, the positive-half-line quadratic exponential integral equals twice the cubed scale.

hypotheses

b :

ℝ

hb :

0 < b

conclusion

(∫ x : ℝ in Ioi 0, x ^ 2 * exp (-x / b)) = 2 * b ^ 3

Proof (Lean source)

theorem integral_sq_mul_exp_neg_div_Ioi (b : ℝ) (hb : 0 < b) : (∫ x : ℝ in Ioi 0, x ^ 2 * exp (-x / b)) = 2 * b ^ 3 := by calc _ = ∫ x : ℝ in Ioi 0, x ^ ((3 : ℝ) - 1) * exp (-((1 / b) * x)) := by apply setIntegral_congr_fun measurableSet_Ioi intro x hx simp only [show (3 : ℝ) - 1 = 2 by norm_num, Real.rpow_two] rw [show -x / b = -(1 / b * x) by ring] _ = (1 / (1 / b)) ^ (3 : ℝ) * Gamma (3 : ℝ) := Real.integral_rpow_mul_exp_neg_mul_Ioi (by norm_num) (one_div_pos.mpr hb) _ = 2 * b ^ 3 := by rw [show Gamma (3 : ℝ) = 2 by norm_num] rw [one_div_one_div, show b ^ (3 : ℝ) = b ^ (3 : ℕ) from Real.rpow_natCast b 3] ring

Causalean.Stat.Privacy.integral_sq_mul_exp_neg_div_Ioi · Causalean/Stat/Privacy/LaplaceSecondMoment.lean:65
laplaceMeasure_integrable_sq theorem — At a real scale with a positive-scale certificate, a centered Laplace draw has an integrable square.

hypotheses

b :

ℝ

hb :

0 x ^ 2) (laplaceMeasure b)

Proof (Lean source)

theorem laplaceMeasure_integrable_sq (b : ℝ) (hb : 0 < b) : Integrable (fun x : ℝ => x ^ 2) (laplaceMeasure b) := by have hnonneg (x : ℝ) : 0 ≤ laplacePDF b x := by unfold laplacePDF positivity 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 (hnonneg _), smul_eq_mul, mul_comm] using integrable_sq_mul_laplacePDF b hb

Causalean.Stat.Privacy.laplaceMeasure_integrable_sq · Causalean/Stat/Privacy/LaplaceSecondMoment.lean:87
laplaceMeasure_lintegral_sq theorem — At a real scale with a positive-scale certificate, a centered Laplace draw has nonnegative extended second moment exactly twice the squared scale.

hypotheses

b :

ℝ

hb :

0 < b

conclusion

∫⁻ x : ℝ, ofReal (x ^ 2) ∂laplaceMeasure b = ofReal (2 * b ^ 2)

Proof (Lean source)

theorem laplaceMeasure_lintegral_sq (b : ℝ) (hb : 0 < b) : ∫⁻ x : ℝ, ofReal (x ^ 2) ∂laplaceMeasure b = ofReal (2 * b ^ 2) := by rw [← ofReal_integral_eq_lintegral_ofReal (laplaceMeasure_integrable_sq b hb) (ae_of_all _ fun x => sq_nonneg x), laplaceMeasure_integral_sq b hb]

Causalean.Stat.Privacy.laplaceMeasure_lintegral_sq · Causalean/Stat/Privacy/LaplaceSecondMoment.lean:132