Stat.Privacy.Binary
Binary-input locally private experiments, their sharp scalar Fisher-information bound, and the randomized-response equality case.
Density 12 core · 13 supporting Two rows of an arbitrary measurable-output Boolean-input Markov kernel are dominated by their sum. ★ information_le_sharp
Binary private experiments and their Radon–Nikodym densities
Two rows of an arbitrary measurable-output Boolean-input Markov kernel are dominated by their sum. The real densities define the output law, score, Fisher information, balanced density, and normalized contrast. Setwise local privacy controls the contrast almost everywhere.
def SetwisePrivate reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel at privacy level has setwise local privacy when either output row gives every measurable event at most exp ε times the other row's mass.
Definition (Lean source)
parameters
def
SetwisePrivate Q ε :
Prop
def reference reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel determines its common row-sum reference measure, given by the sum of its positive and negative output rows. Here true denotes the positive sign.
def rowDensity reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel, an input sign, and an output point determine the real Radon–Nikodym density of that output row relative to the row sum, given by its Radon–Nikodym derivative.
def contraction reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A privacy level determines its binary local-privacy contraction parameter, given by the ratio (exp ε - 1)/(exp ε + 1).
def balancedDensity reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel and an output point determine the balanced density, given by half the sum of the two row densities.
def contrast reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel and an output point determine the normalized density contrast, given by the positive-row density minus the negative-row density, divided by their sum, and read as zero where that sum vanishes.
def mixtureDensity reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel, a sign-family parameter, and an output point determine the Bernoulli-mixture output density, given by weights (1 + τ)/2 and (1 - τ)/2.
def outputLaw reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel and a sign-family parameter determine the Bernoulli-mixture output law, given by the mixture of its positive and negative rows with weights (1 + τ)/2 and (1 - τ)/2, each truncated at zero. It is a convex mixture exactly when the parameter lies between −1 and 1.
def derivativeDensity reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel and an output point determine the parameter derivative of the Bernoulli-mixture density, given by half the difference of the two row densities.
def score reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel, a sign-family parameter, and an output point determine the guarded likelihood score, given by the derivative divided by positive mixture density and zero otherwise.
Definition (Lean source)
parameters
def
score Q τ z :
ℝ
given by
def information reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel and a sign-family parameter determine the scalar output Fisher information, given by the row-sum-reference integral of mixture density times squared guarded score.
Definition (Lean source)
parameters
def
information Q τ :
ℝ
given by
∫ z, mixtureDensity Q τ z * (score Q τ z) ^ 2 ∂reference Q
theorem information_le_sharp reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel, a positive privacy level, an interior sign-family parameter, and setwise local privacy give a scalar output Fisher-information bound equal to the randomized-response value: writing c = (exp ε - 1)/(exp ε + 1) for the contraction parameter, the Fisher information of the output about the sign-family parameter is at most c² / (1 - c² τ²). This statement is the upper bound only; attainment by randomized response is a separate result.
Formal statement
hypotheses
Z :
Type u_1
Q :
ε τ :
ℝ
hε :
0 < ε
hτ :
|τ| < 1
hpriv :
SetwisePrivate Q ε
conclusion
information Q τ ≤ contraction ε ^ 2 / (1 - contraction ε ^ 2 * τ ^ 2)
Proof (Lean source)
theorem information_le_sharp (Q : Kernel Bool Z) [IsMarkovKernel Q]
(ε τ : ℝ) (hε : 0 < ε) (hτ : |τ| < 1)
(hpriv : SetwisePrivate Q ε) :
information Q τ ≤
contraction ε ^ 2 / (1 - contraction ε ^ 2 * τ ^ 2) := by
haveI : IsFiniteMeasure (reference Q) := reference_finite Q
have hk0 := (contraction_mem ε hε).1
have hk1 := (contraction_mem ε hε).2
have hδ := ae_abs_contrast_le Q ε hε hpriv
have ht : Integrable (rowDensity Q true) (reference Q) :=
Measure.integrable_toReal_rnDeriv
have hf : Integrable (rowDensity Q false) (reference Q) :=
Measure.integrable_toReal_rnDeriv
have hbal : Integrable (balancedDensity Q) (reference Q) := by
unfold balancedDensity
exact (ht.add hf).div_const 2
have hbc : Integrable (fun z => balancedDensity Q z * contrast Q z)
(reference Q) := by
apply Integrable.mono' (hbal.mul_const (contraction ε))
· exact ((measurable_rowDensity Q true).add
(measurable_rowDensity Q false)).div_const 2 |>.mul
(((measurable_rowDensity Q true).sub
(measurable_rowDensity Q false)).div
((measurable_rowDensity Q true).add
(measurable_rowDensity Q false))) |>.aestronglyMeasurable
· filter_upwards [hδ] with z hz
have hb : 0 ≤ balancedDensity Q z := by
unfold balancedDensity
exact div_nonneg (add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg)
(by norm_num)
rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg hb]
exact mul_le_mul_of_nonneg_left hz hb
let C := contraction ε ^ 2 / (1 - contraction ε ^ 2 * τ ^ 2)
have hright : Integrable (fun z => C *
(balancedDensity Q z - τ * (balancedDensity Q z * contrast Q z)))
(reference Q) := by
exact (hbal.sub (hbc.const_mul τ)).const_mul C
rw [information_eq_contrast_integral Q τ hτ]
have hmain :
(∫ z, balancedDensity Q z * contrast Q z ^ 2 /
(1 + τ * contrast Q z) ∂reference Q) ≤
∫ z, C * (balancedDensity Q z -
τ * (balancedDensity Q z * contrast Q z)) ∂reference Q := by
apply integral_mono_of_nonneg
· filter_upwards [hδ] with z hz
have hb : 0 ≤ balancedDensity Q z := by
unfold balancedDensity
exact div_nonneg (add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg)
(by norm_num)
have htd : |τ * contrast Q z| < 1 := by
rw [abs_mul]
nlinarith [mul_nonneg (sub_nonneg.mpr (le_of_lt hτ))
(abs_nonneg (contrast Q z))]
have hden : 0 < 1 + τ * contrast Q z := by
have := (abs_lt.mp htd).1
linarith
exact div_nonneg (mul_nonneg hb (sq_nonneg _)) (le_of_lt hden)
· exact hright
· filter_upwards [hδ] with z hz
have hb : 0 ≤ balancedDensity Q z := by
unfold balancedDensity
exact div_nonneg (add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg)
(by norm_num)
have hc := contrast_chord
(contraction ε) τ (contrast Q z) hk0 hk1 hτ hz
have := mul_le_mul_of_nonneg_left hc hb
dsimp [C]
convert this using 1 <;> ring
calc
(∫ z, balancedDensity Q z * contrast Q z ^ 2 /
(1 + τ * contrast Q z) ∂reference Q) ≤
∫ z, C * (balancedDensity Q z -
τ * (balancedDensity Q z * contrast Q z)) ∂reference Q := hmain
_ = C := by
rw [integral_const_mul, integral_sub hbal (hbc.const_mul τ),
integral_const_mul, integral_balancedDensity Q,
integral_balanced_contrast Q]
ring
_ = _ := rfl
13 supporting declarations (lemmas, instances)
-
reference_finitetheorem — A Boolean-input Markov kernel has a finite row-sum reference measure.Proof (Lean source)
theorem reference_finite (Q : Kernel Bool Z) [IsMarkovKernel Q] : IsFiniteMeasure (reference Q) := by unfold reference infer_instance -
measurable_rowDensitytheorem — A Boolean-input Markov kernel and an input sign give a measurable real row density on the output σ-algebra.Proof (Lean source)
theorem measurable_rowDensity (Q : Kernel Bool Z) (b : Bool) : Measurable (rowDensity Q b) := by exact ((Q b).measurable_rnDeriv (reference Q)).ennreal_toReal -
row_actheorem — A Boolean-input Markov kernel and an input sign give an output row absolutely continuous with respect to the row-sum measure. -
row_eq_withDensitytheorem — A Boolean-input Markov kernel and an input sign make its Radon–Nikodym density reconstruct the corresponding output row exactly, including on zero-reference-mass sets.hypothesesconclusionQ b = (reference Q).withDensity (fun z => ofReal (rowDensity Q b z))Proof (Lean source)
theorem row_eq_withDensity (Q : Kernel Bool Z) [IsMarkovKernel Q] (b : Bool) : Q b = (reference Q).withDensity (fun z => ofReal (rowDensity Q b z)) := by haveI : IsFiniteMeasure (reference Q) := reference_finite Q haveI : IsFiniteMeasure (Q b) := inferInstance have h : ∀ᵐ z ∂reference Q, (Q b).rnDeriv (reference Q) z ≠ ⊤ := (Q b).rnDeriv_ne_top (reference Q) have heq : (fun z => ofReal (rowDensity Q b z)) =ᵐ[reference Q] (Q b).rnDeriv (reference Q) := by filter_upwards [h] with z hz simp only [rowDensity, ENNReal.ofReal_toReal hz] rw [← Measure.withDensity_rnDeriv_eq (Q b) (reference Q) (row_ac Q b)] exact withDensity_congr_ae heq.symm -
outputLaw_eq_withDensitytheorem — A Boolean-input Markov kernel and an interior sign-family parameter make the Bernoulli-mixture output law equal to the measure with its stated mixture density relative to the row-sum reference.hypothesesconclusionProof (Lean source)
theorem outputLaw_eq_withDensity (Q : Kernel Bool Z) [IsMarkovKernel Q] (τ : ℝ) (hτ : |τ| < 1) : outputLaw Q τ = (reference Q).withDensity (fun z => ofReal (mixtureDensity Q τ z)) := by have hp : 0 ≤ (1 + τ) / 2 := by have := (abs_lt.mp hτ).1; linarith have hm : 0 ≤ (1 - τ) / 2 := by have := (abs_lt.mp hτ).2; linarith have hpoint : (fun z => ofReal (mixtureDensity Q τ z)) = (fun z => ofReal ((1 + τ) / 2) • ofReal (rowDensity Q true z) + ofReal ((1 - τ) / 2) • ofReal (rowDensity Q false z)) := by funext z have ht : 0 ≤ rowDensity Q true z := ENNReal.toReal_nonneg have hf : 0 ≤ rowDensity Q false z := ENNReal.toReal_nonneg dsimp [mixtureDensity] rw [ENNReal.ofReal_add (mul_nonneg hp ht) (mul_nonneg hm hf), ENNReal.ofReal_mul hp, ENNReal.ofReal_mul hm] rw [outputLaw, row_eq_withDensity Q true, row_eq_withDensity Q false, hpoint] rw [← withDensity_smul _ (measurable_rowDensity Q true).ennreal_ofReal, ← withDensity_smul _ (measurable_rowDensity Q false).ennreal_ofReal] exact (withDensity_add_left ((measurable_rowDensity Q true).ennreal_ofReal.const_smul _) (fun z => ofReal ((1 - τ) / 2) • ofReal (rowDensity Q false z))).symm -
hasDerivAt_mixtureDensitytheorem — A Boolean-input Markov kernel, a sign-family parameter, and an output point make the Bernoulli-mixture density differentiable with the stated row-difference derivative.hypothesesconclusionProof (Lean source)
theorem hasDerivAt_mixtureDensity (Q : Kernel Bool Z) (τ : ℝ) (z : Z) : HasDerivAt (fun t => mixtureDensity Q t z) (derivativeDensity Q z) τ := by have h := ((hasDerivAt_id τ).add_const 1 |>.div_const 2 |>.mul_const (rowDensity Q true z)).add (((hasDerivAt_const τ 1).sub (hasDerivAt_id τ) |>.div_const 2).mul_const (rowDensity Q false z)) have hfun : (fun t => mixtureDensity Q t z) = (fun t => (t + 1) / 2 * rowDensity Q true z) + (fun t => (1 - t) / 2 * rowDensity Q false z) := by funext t dsimp [mixtureDensity] ring have hder : derivativeDensity Q z = 1 / 2 * rowDensity Q true z + (0 - 1) / 2 * rowDensity Q false z := by dsimp [derivativeDensity] ring rw [hfun, hder] exact h -
ae_density_privatetheorem — A Boolean-input Markov kernel, a privacy level, and setwise local privacy make the two Radon–Nikodym row densities satisfy the corresponding privacy inequalities almost everywhere under their common reference measure.hypothesesProof (Lean source)
theorem ae_density_private (Q : Kernel Bool Z) [IsMarkovKernel Q] (ε : ℝ) (hpriv : SetwisePrivate Q ε) : ∀ᵐ z ∂reference Q, rowDensity Q true z ≤ exp ε * rowDensity Q false z ∧ rowDensity Q false z ≤ exp ε * rowDensity Q true z := by haveI : IsFiniteMeasure (reference Q) := reference_finite Q have hpair (b c : Bool) : ∀ᵐ z ∂reference Q, rowDensity Q b z ≤ exp ε * rowDensity Q c z := by have hle : (Q b).rnDeriv (reference Q) ≤ᵐ[reference Q] fun z => ofReal (exp ε) * (Q c).rnDeriv (reference Q) z := by apply ae_le_of_forall_setLIntegral_le_of_sigmaFinite ((Q b).measurable_rnDeriv (reference Q)) intro s hs _ rw [lintegral_const_mul _ ((Q c).measurable_rnDeriv (reference Q))] have hb := Measure.withDensity_rnDeriv_eq (Q b) (reference Q) (row_ac Q b) have hc := Measure.withDensity_rnDeriv_eq (Q c) (reference Q) (row_ac Q c) rw [← withDensity_apply ((Q b).rnDeriv (reference Q)) hs, hb, ← withDensity_apply ((Q c).rnDeriv (reference Q)) hs, hc] exact hpriv b c s hs filter_upwards [hle, (Q c).rnDeriv_ne_top (reference Q)] with z hz hzc rw [← ENNReal.ofReal_toReal hzc, ← ENNReal.ofReal_mul (le_of_lt (Real.exp_pos ε))] at hz exact ENNReal.toReal_le_of_le_ofReal (mul_nonneg (le_of_lt (Real.exp_pos ε)) ENNReal.toReal_nonneg) hz filter_upwards [hpair true false, hpair false true] with z h₁ h₂ exact ⟨h₁, h₂⟩ -
integral_balancedDensitytheorem — A Boolean-input Markov kernel has balanced density with unit integral under its row-sum reference measure.Proof (Lean source)
theorem integral_balancedDensity (Q : Kernel Bool Z) [IsMarkovKernel Q] : ∫ z, balancedDensity Q z ∂reference Q = 1 := by haveI : IsFiniteMeasure (reference Q) := reference_finite Q have ht : Integrable (rowDensity Q true) (reference Q) := Measure.integrable_toReal_rnDeriv have hf : Integrable (rowDensity Q false) (reference Q) := Measure.integrable_toReal_rnDeriv have hrow (b : Bool) : ∫ z, rowDensity Q b z ∂reference Q = 1 := by change (∫ z, ((Q b).rnDeriv (reference Q) z).toReal ∂reference Q) = 1 rw [Measure.integral_toReal_rnDeriv (row_ac Q b)] simp [measureReal_def] simp only [balancedDensity, integral_div, integral_add ht hf, hrow] norm_num -
integral_balanced_contrasttheorem — A Boolean-input Markov kernel has balanced density times normalized contrast with mean zero under its row-sum reference measure.hypothesesZ :sharedType u_1Q :conclusion∫ z, balancedDensity Q z * contrast Q z ∂reference Q = 0Proof (Lean source)
theorem integral_balanced_contrast (Q : Kernel Bool Z) [IsMarkovKernel Q] : ∫ z, balancedDensity Q z * contrast Q z ∂reference Q = 0 := by haveI : IsFiniteMeasure (reference Q) := reference_finite Q have ht : Integrable (rowDensity Q true) (reference Q) := Measure.integrable_toReal_rnDeriv have hf : Integrable (rowDensity Q false) (reference Q) := Measure.integrable_toReal_rnDeriv have hpoint (z : Z) : balancedDensity Q z * contrast Q z = derivativeDensity Q z := by let a := rowDensity Q true z let b := rowDensity Q false z have ha : 0 ≤ a := ENNReal.toReal_nonneg have hb : 0 ≤ b := ENNReal.toReal_nonneg by_cases hs : a + b = 0 · have hza : a = 0 := by linarith have hzb : b = 0 := by linarith simp [balancedDensity, contrast, derivativeDensity, a, b, hza, hzb] · dsimp [balancedDensity, contrast, derivativeDensity] change (a + b) / 2 * ((a - b) / (a + b)) = (a - b) / 2 field_simp rw [show (fun z => balancedDensity Q z * contrast Q z) = derivativeDensity Q from funext hpoint] have hrow (b : Bool) : ∫ z, rowDensity Q b z ∂reference Q = 1 := by change (∫ z, ((Q b).rnDeriv (reference Q) z).toReal ∂reference Q) = 1 rw [Measure.integral_toReal_rnDeriv (row_ac Q b)] simp [measureReal_def] change (∫ z, (rowDensity Q true z - rowDensity Q false z) / 2 ∂reference Q) = 0 simp only [integral_div, integral_sub ht hf, hrow] norm_num -
contraction_memtheorem — A positive privacy level at the supplied privacy parameter has a contraction parameter in the half-open unit interval.Proof (Lean source)
theorem contraction_mem (ε : ℝ) (hε : 0 < ε) : 0 ≤ contraction ε ∧ contraction ε < 1 := by have he : 1 < exp ε := (Real.one_lt_exp_iff).2 hε unfold contraction constructor · exact div_nonneg (by linarith) (by linarith) · exact (div_lt_one (by linarith)).2 (by linarith) -
ae_abs_contrast_letheorem — A Boolean-input Markov kernel, a positive privacy level, and setwise local privacy make the absolute normalized row contrast almost everywhere bounded by the sharp contraction parameter.hypothesesconclusion∀ᵐ z ∂reference Q, |contrast Q z| ≤ contraction εProof (Lean source)
theorem ae_abs_contrast_le (Q : Kernel Bool Z) [IsMarkovKernel Q] (ε : ℝ) (hε : 0 < ε) (hpriv : SetwisePrivate Q ε) : ∀ᵐ z ∂reference Q, |contrast Q z| ≤ contraction ε := by have hk := (contraction_mem ε hε).1 have he : 1 < exp ε := (Real.one_lt_exp_iff).2 hε filter_upwards [ae_density_private Q ε hpriv] with z hz let a := rowDensity Q true z let b := rowDensity Q false z have ha : 0 ≤ a := ENNReal.toReal_nonneg have hb : 0 ≤ b := ENNReal.toReal_nonneg by_cases hs : a + b = 0 · have hza : a = 0 := by linarith have hzb : b = 0 := by linarith simpa [contrast, a, b, hza, hzb] using hk · have hspos : 0 < a + b := lt_of_le_of_ne (add_nonneg ha hb) (Ne.symm hs) have hnum : |a - b| * (exp ε + 1) ≤ (exp ε - 1) * (a + b) := by calc |a - b| * (exp ε + 1) = |(a - b) * (exp ε + 1)| := by rw [abs_mul, abs_of_pos (show 0 < exp ε + 1 by linarith)] _ ≤ (exp ε - 1) * (a + b) := (abs_le).2 ⟨by nlinarith [hz.2], by nlinarith [hz.1]⟩ change |(a - b) / (a + b)| ≤ (exp ε - 1) / (exp ε + 1) rw [abs_div, abs_of_pos hspos] exact (div_le_div_iff₀ hspos (by linarith)).2 hnum -
information_eq_causalean_fishertheorem — A Boolean-input Markov kernel at a sign-family parameter has the same Fisher information as the guarded likelihood-score API when that API is supplied the Bernoulli-mixture density and its derivative.hypothesesconclusioninformation Q τProof (Lean source)
theorem information_eq_causalean_fisher (Q : Kernel Bool Z) (τ : ℝ) : information Q τ = fisherInformation (reference Q) (mixtureDensity Q) (fun _ z => derivativeDensity Q z) τ := by rfl -
information_eq_contrast_integraltheorem — A Boolean-input Markov kernel at an interior sign-family parameter has Fisher information equal to the balanced-density contrast integral, including zero-density outputs.hypothesesconclusioninformation Q τ= ∫ z, balancedDensity Q z * contrast Q z ^ 2 / (1 + τ * contrast Q z) ∂reference QProof (Lean source)
theorem information_eq_contrast_integral (Q : Kernel Bool Z) [IsMarkovKernel Q] (τ : ℝ) (hτ : |τ| < 1) : information Q τ = ∫ z, balancedDensity Q z * contrast Q z ^ 2 / (1 + τ * contrast Q z) ∂reference Q := by change (∫ z, mixtureDensity Q τ z * score Q τ z ^ 2 ∂reference Q) = _ congr 1 funext z let a := rowDensity Q true z let b := rowDensity Q false z have ha : 0 ≤ a := ENNReal.toReal_nonneg have hb : 0 ≤ b := ENNReal.toReal_nonneg by_cases hs : a + b = 0 · have hza : a = 0 := by linarith have hzb : b = 0 := by linarith simp [mixtureDensity, score, derivativeDensity, balancedDensity, contrast, a, b, hza, hzb] · have hspos : 0 < a + b := lt_of_le_of_ne (add_nonneg ha hb) (Ne.symm hs) have hd : |(a - b) / (a + b)| ≤ 1 := by rw [abs_div, abs_of_pos hspos] apply (div_le_iff₀ hspos).2 have habs : |a - b| ≤ a + b := (abs_le).2 ⟨by linarith, by linarith⟩ simpa using habs have htd : |τ * ((a - b) / (a + b))| < 1 := by rw [abs_mul] nlinarith [mul_nonneg (sub_nonneg.mpr (le_of_lt hτ)) (abs_nonneg ((a - b) / (a + b)))] have hfactor : 0 < 1 + τ * ((a - b) / (a + b)) := by have := (abs_lt.mp htd).1 linarith have hmix : mixtureDensity Q τ z = (a + b) / 2 * (1 + τ * ((a - b) / (a + b))) := by change (1 + τ) / 2 * a + (1 - τ) / 2 * b = _ field_simp [hs] ring have hmixpos : 0 < mixtureDensity Q τ z := by rw [hmix] exact mul_pos (by linarith) hfactor simp only [score, if_pos hmixpos, balancedDensity, contrast, derivativeDensity] change mixtureDensity Q τ z * (((a - b) / 2) / mixtureDensity Q τ z) ^ 2 = (a + b) / 2 * ((a - b) / (a + b)) ^ 2 / (1 + τ * ((a - b) / (a + b))) rw [hmix] field_simp
RandomizedResponse 5 core · 3 supporting The Boolean randomized-response kernel realizes both extremal private contrasts and attains the sharp Fisher bound. ★ randomizedResponse_information_eq★ discreteInformation_le_sharp
Binary randomized response and countable outputs
The Boolean randomized-response kernel realizes both extremal private contrasts and attains the sharp Fisher bound. For countable measurable outputs, the Radon–Nikodym integral becomes the usual sum over atoms.
def responseProbability reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A privacy level and Boolean input sign determine the probability of a positive randomized-response report, equal to exp ε/(exp ε + 1) for positive input and 1/(exp ε + 1) for negative input.
def randomizedResponse reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A privacy level determines the Boolean-output randomized-response kernel, which reports a positive sign with probability exp ε/(exp ε + 1) when the input is positive and 1/(exp ε + 1) when it is negative, and a negative sign otherwise.
Definition (Lean source)
def discreteInformation reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel, intended for a countable measurable output alphabet, and a sign-family parameter determine the atomic scalar Fisher information, given by the sum over output points of the squared difference of the two row masses divided by four times the mixture mass ((1 + τ)·positive + (1 - τ)·negative)/2, with atoms whose denominator vanishes contributing zero. Equivalently each atom contributes its squared half-difference of row masses divided by its mixture mass.
theorem randomizedResponse_information_eq reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A positive privacy level and an interior sign-family parameter make binary randomized response attain the sharp scalar Fisher-information bound: its output Fisher information equals c² / (1 - c² τ²) exactly, where c = (exp ε - 1)/(exp ε + 1) is the contraction parameter.
Formal statement
Proof (Lean source)
theorem randomizedResponse_information_eq (ε τ : ℝ)
(hε : 0 < ε) (hτ : |τ| < 1) :
letI : IsMarkovKernel (randomizedResponse ε) := randomizedResponse_markov ε
information (randomizedResponse ε) τ =
contraction ε ^ 2 / (1 - contraction ε ^ 2 * τ ^ 2) := by
letI : IsMarkovKernel (randomizedResponse ε) := randomizedResponse_markov ε
let e := exp ε
let p := e / (e + 1)
let q := 1 / (e + 1)
have he : 0 < e := Real.exp_pos ε
have he1 : 0 < e + 1 := by linarith
have hp : 0 < p := div_pos he he1
have hq : 0 < q := div_pos (by norm_num) he1
have hcq : 1 - q = p := by
dsimp [p, q]
field_simp
<;> ring
have hcp : 1 - p = q := by
dsimp [p, q]
field_simp
<;> ring
have hqi : (exp ε + 1)⁻¹ = q := by
dsimp [q, e]
rw [one_div]
have hmass (b z : Bool) :
((randomizedResponse ε b) {z}).toReal =
if b = z then p else q := by
change ((bernoulliBool
(responseProbability ε b)) {z}).toReal = if b = z then p else q
cases b <;> cases z <;>
simp [responseProbability, bernoulliBool,
Measure.add_apply, Measure.smul_apply]
all_goals try rw [hqi]
all_goals first
| (change (ofReal (1 - q)).toReal = p
rw [hcq, ENNReal.toReal_ofReal hp.le])
| (change (ofReal q).toReal = q
rw [ENNReal.toReal_ofReal hq.le])
| (change (ofReal (1 - p)).toReal = q
rw [hcp, ENNReal.toReal_ofReal hq.le])
| (change (ofReal p).toReal = p
rw [ENNReal.toReal_ofReal hp.le])
rw [information_eq_discrete (randomizedResponse ε) τ hτ]
simp only [discreteInformation, tsum_fintype]
simp [hmass]
have hsum : p + q = 1 := by
dsimp [p, q]
field_simp
<;> ring
have hk : contraction ε = p - q := by
dsimp [contraction, p, q, e]
field_simp
<;> ring
let d₁ := (1 + τ) * p + (1 - τ) * q
let d₂ := (1 + τ) * q + (1 - τ) * p
have hct : 0 < 1 + τ := by have := (abs_lt.mp hτ).1; linarith
have hcf : 0 < 1 - τ := by have := (abs_lt.mp hτ).2; linarith
have hd₁ : 0 < d₁ := add_pos (mul_pos hct hp) (mul_pos hcf hq)
have hd₂ : 0 < d₂ := add_pos (mul_pos hct hq) (mul_pos hcf hp)
have hden : d₁ * d₂ = 1 - (p - q) ^ 2 * τ ^ 2 := by
calc
d₁ * d₂ = (p + q) ^ 2 - (p - q) ^ 2 * τ ^ 2 := by dsimp [d₁, d₂]; ring
_ = _ := by rw [hsum]; ring
rw [hk]
change (p - q) ^ 2 / (2 * d₁) + (q - p) ^ 2 / (2 * d₂) =
(p - q) ^ 2 / (1 - (p - q) ^ 2 * τ ^ 2)
rw [← hden]
field_simp [hd₁.ne', hd₂.ne']
nlinarith [hsum]
theorem discreteInformation_le_sharp reviewed
⚑ flagged
Causalean.Stat.Privacy.Binary
A Boolean-input Markov kernel on a countable measurable output alphabet, a positive privacy level, an interior sign-family parameter, and setwise local privacy give the sharp atomic Fisher-information bound: the atomic Fisher information is at most c² / (1 - c² τ²), where c = (exp ε - 1)/(exp ε + 1) is the contraction parameter. This statement is the upper bound only.
Formal statement
hypotheses
Z :
Type u_1
Q :
ε τ :
ℝ
hε :
0 < ε
hτ :
|τ| < 1
hpriv :
SetwisePrivate Q ε
conclusion
Proof (Lean source)
theorem discreteInformation_le_sharp (Q : Kernel Bool Z) [IsMarkovKernel Q]
(ε τ : ℝ) (hε : 0 < ε) (hτ : |τ| < 1)
(hpriv : SetwisePrivate Q ε) :
discreteInformation Q τ ≤
contraction ε ^ 2 / (1 - contraction ε ^ 2 * τ ^ 2) := by
rw [← information_eq_discrete Q τ hτ]
exact information_le_sharp Q ε τ hε hτ hpriv
3 supporting declarations (lemmas, instances)
-
randomizedResponse_markovtheorem — At any privacy level, binary randomized response is a Markov kernel.Proof (Lean source)
theorem randomizedResponse_markov (ε : ℝ) : IsMarkovKernel (randomizedResponse ε) := by have he : 0 < exp ε := Real.exp_pos ε refine ⟨fun b => ?_⟩ cases b · change IsProbabilityMeasure (bernoulliBool (1 / (exp ε + 1))) apply bernoulliBool_isProbabilityMeasure · positivity · apply (div_le_iff₀ (by linarith : 0 < exp ε + 1)).2 linarith · change IsProbabilityMeasure (bernoulliBool (exp ε / (exp ε + 1))) apply bernoulliBool_isProbabilityMeasure · positivity · apply (div_le_iff₀ (by linarith : 0 < exp ε + 1)).2 linarith -
randomizedResponse_privatetheorem — A positive privacy level at the supplied parameter makes binary randomized response satisfy pairwise setwise local privacy.Proof (Lean source)
theorem randomizedResponse_private (ε : ℝ) (hε : 0 < ε) : SetwisePrivate (randomizedResponse ε) ε := by intro b c s hs have he : 0 < exp ε := Real.exp_pos ε have he1 : 0 < exp ε + 1 := by linarith have hege : 1 ≤ exp ε := (Real.one_lt_exp_iff.mpr hε).le have hcomp₁ : 1 - (exp ε + 1)⁻¹ = exp ε / (exp ε + 1) := by rw [inv_eq_one_div] field_simp <;> ring have hcomp₂ : 1 - exp ε / (exp ε + 1) = (exp ε + 1)⁻¹ := by rw [inv_eq_one_div] field_simp <;> ring have hself (x : ENNReal) : x ≤ ofReal (exp ε) * x := by calc x = 1 * x := by simp _ ≤ ofReal (exp ε) * x := by gcongr simpa using ENNReal.ofReal_le_ofReal hege have hqp : ofReal ((exp ε + 1)⁻¹) ≤ ofReal (exp ε) * ofReal (exp ε / (exp ε + 1)) := by rw [← ENNReal.ofReal_mul he.le] apply ENNReal.ofReal_le_ofReal rw [inv_eq_one_div] apply (div_le_iff₀ he1).2 rw [mul_assoc, div_mul_cancel₀ _ he1.ne'] nlinarith [sq_nonneg (exp ε - 1)] have hpq : ofReal (exp ε / (exp ε + 1)) ≤ ofReal (exp ε) * ofReal ((exp ε + 1)⁻¹) := by rw [← ENNReal.ofReal_mul he.le] apply ENNReal.ofReal_le_ofReal exact (div_eq_mul_inv (exp ε) (exp ε + 1)).le change (bernoulliBool (responseProbability ε b)) s ≤ ofReal (exp ε) * (bernoulliBool (responseProbability ε c)) s cases b <;> cases c <;> by_cases ht : true ∈ s <;> by_cases hf : false ∈ s <;> simp [responseProbability, bernoulliBool, Measure.add_apply, Measure.smul_apply, Measure.dirac_apply, ht, hf, hcomp₁, hcomp₂] all_goals first | exact hself _ | exact hqp | exact hpq | rw [mul_add]; exact add_le_add (hself _) (hself _) | rw [mul_add]; exact add_le_add hqp hpq | rw [mul_add]; exact add_le_add hpq hqp -
information_eq_discretetheorem — A Boolean-input Markov kernel on a countable measurable output alphabet at an interior sign-family parameter has Radon–Nikodym Fisher information equal to its atomic Fisher sum.hypothesesconclusioninformation Q τ = discreteInformation Q τProof (Lean source)
theorem information_eq_discrete (Q : Kernel Bool Z) [IsMarkovKernel Q] (τ : ℝ) (hτ : |τ| < 1) : information Q τ = discreteInformation Q τ := by rw [information_eq_contrast_integral Q τ hτ, integral_countable' (integrable_contrast_fisher Q τ hτ)] unfold discreteInformation congr 1 funext z let r := (reference Q).real {z} let a := rowDensity Q true z let b := rowDensity Q false z have hma : r * a = (Q true {z}).toReal := rowDensity_mul_atom Q true z have hmb : r * b = (Q false {z}).toReal := rowDensity_mul_atom Q false z have ha : 0 ≤ a := ENNReal.toReal_nonneg have hb : 0 ≤ b := ENNReal.toReal_nonneg have hr : 0 ≤ r := ENNReal.toReal_nonneg change r * (balancedDensity Q z * contrast Q z ^ 2 / (1 + τ * contrast Q z)) = _ rw [← hma, ← hmb] by_cases hr0 : r = 0 · simp [hr0] by_cases hs : a + b = 0 · have hza : a = 0 := by linarith have hzb : b = 0 := by linarith simp [balancedDensity, contrast, a, b, hza, hzb] have hrpos : 0 < r := lt_of_le_of_ne hr (Ne.symm hr0) have hspos : 0 < a + b := lt_of_le_of_ne (add_nonneg ha hb) (Ne.symm hs) have hct : 0 < 1 + τ := by have := (abs_lt.mp hτ).1; linarith have hcf : 0 < 1 - τ := by have := (abs_lt.mp hτ).2; linarith have hD : 0 < (1 + τ) * a + (1 - τ) * b := by by_cases hza : a = 0 · have hbpos : 0 < b := by linarith simpa [hza] using mul_pos hcf hbpos · have hapos : 0 < a := lt_of_le_of_ne ha (Ne.symm hza) exact add_pos_of_pos_of_nonneg (mul_pos hct hapos) (mul_nonneg hcf.le hb) have hden : 0 < 1 + τ * ((a - b) / (a + b)) := by have heq : 1 + τ * ((a - b) / (a + b)) = ((1 + τ) * a + (1 - τ) * b) / (a + b) := by field_simp <;> ring rw [heq] exact div_pos hD hspos change r * (((a + b) / 2) * ((a - b) / (a + b)) ^ 2 / (1 + τ * ((a - b) / (a + b)))) = (r * a - r * b) ^ 2 / (2 * ((1 + τ) * (r * a) + (1 - τ) * (r * b))) field_simp [hr0, hs, hden.ne', hD.ne'] <;> ring