diff --git a/SampCert/DifferentialPrivacy/Abstract.lean b/SampCert/DifferentialPrivacy/Abstract.lean index cdf2720d..083a1a6f 100644 --- a/SampCert/DifferentialPrivacy/Abstract.lean +++ b/SampCert/DifferentialPrivacy/Abstract.lean @@ -10,31 +10,78 @@ import SampCert.Foundations.Basic /-! # Differential Privacy -This file defines a notion of a differential private system. +This file defines an abstract system of differentially private operators. -/ noncomputable section open Classical Nat Int Real ENNReal -def NonZeroNQ (nq : List T → SLang U) := +/-- +A mechanism is nonzero on its entire domain +-/ +def NonZeroNQ (nq : List T → PMF U) := ∀ l : List T, ∀ n : U, nq l n ≠ 0 -def NonTopSum (nq : List T → SLang U) := - ∀ l : List T, ∑' n : U, nq l n ≠ ⊤ - namespace SLang abbrev Query (T U : Type) := List T → U -abbrev Mechanism (T U : Type) := List T → SLang U + +abbrev Mechanism (T U : Type) := List T → PMF U /-- -Product of mechanisms. +General (value-dependent) composition of mechanisms +-/ +def privComposeAdaptive (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (l : List T) : SLang (U × V) := do + let A <- nq1 l + let B <- nq2 A l + return (A, B) + + +lemma compose_sum_rw_adaptive (nq1 : List T → SLang U) (nq2 : U -> List T → SLang V) (u : U) (v : V) (l : List T) : + (∑' (a : U), nq1 l a * ∑' (a_1 : V), if u = a ∧ v = a_1 then nq2 a l a_1 else 0) = nq1 l u * nq2 u l v := by + have hrw1 : ∀ (a : U), nq1 l a * (∑' (a_1 : V), if u = a ∧ v = a_1 then nq2 a l a_1 else 0) = if (u = a) then (nq1 l a * ∑' (a_1 : V), if u = a ∧ v = a_1 then nq2 a l a_1 else 0) else 0 := by + intro a + split + · simp + · aesop + have hrw2 : ∀ (a : U), (if (u = a) then (nq1 l a * ∑' (a_1 : V), if u = a ∧ v = a_1 then nq2 a l a_1 else 0) else 0) = (nq1 l u * (∑' (a_1 : V), if u = a ∧ v = a_1 then nq2 u l a_1 else 0)) := by + intro a + split + · aesop + · aesop + rw [tsum_congr hrw1] + rw [tsum_congr hrw2] + clear hrw1 hrw2 + rw [ENNReal.tsum_mul_left] + congr 1 + rw [<- ENNReal.tsum_prod] + have hrw3 : ∀ (p : U × V), (if u = p.1 ∧ v = p.2 then nq2 u l p.2 else 0) = nq2 u l v * (if p = (u, v) then 1 else 0) := by + intro p + split + · aesop + · aesop + rw [tsum_congr hrw3] + rw [ENNReal.tsum_mul_left] + rw [tsum_ite_eq] + exact MulOneClass.mul_one (nq2 u l v) + + +/-- +Chain rule relating the adaptive composition definitions + +The joint distribution decomposes into the conditional and marginal (ie, nq1 l) distributions +-/ +lemma privComposeChainRule (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (l : List T) : + ∀ (u : U), ∀ (v : V), privComposeAdaptive nq1 nq2 l (u, v) = nq1 l u * nq2 u l v := by + intros u v + rw [<- compose_sum_rw_adaptive] + simp [privComposeAdaptive] -Note that the second mechanism does not depend on the output of the first; this is in currently -in contrast to the notions of composition found in the DP literature. +/-- +Product of mechanisms. -/ -def privCompose (nq1 : Mechanism T U) (nq2 : Mechanism T V) (l : List T) : SLang (U × V) := do +def privCompose (nq1 : Mechanism T U) (nq2 : Mechanism T V) (l : List T) : PMF (U × V) := do let A ← nq1 l let B ← nq2 l return (A,B) @@ -42,78 +89,61 @@ def privCompose (nq1 : Mechanism T U) (nq2 : Mechanism T V) (l : List T) : SLang /-- Mechanism obtained by applying a post-processing function to a mechanism. -/ -def privPostProcess (nq : Mechanism T U) (pp : U → V) (l : List T) : SLang V := do +def privPostProcess (nq : Mechanism T U) (pp : U → V) (l : List T) : PMF V := do let A ← nq l return pp A - /-- Abstract definition of a differentially private systemm. -/ class DPSystem (T : Type) where /-- - Notion of differential privacy with a paramater (ε-DP, ε-zCDP, etc) + Differential privacy proposition, with one real paramater (ε-DP, ε-zCDP, etc) -/ prop : Mechanism T Z → ℝ → Prop /-- - Noise mechanism (eg. Laplace, Discrete Gaussian, etc) - Paramaterized by a query, sensitivity, and the numerator/denominator ofa (rational) security paramater. + A noise mechanism (eg. Laplace, Discrete Gaussian, etc) + Paramaterized by a query, sensitivity, and a (rational) security paramater. -/ - noise : Query T ℤ → ℕ+ → ℕ+ → ℕ+ → Mechanism T ℤ + noise : Query T ℤ → (sensitivity : ℕ+) → (num : ℕ+) → (den : ℕ+) → Mechanism T ℤ /-- - Adding noise to a query makes it differentially private. + Adding noise to a query makes it private. -/ noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, sensitivity q Δ → prop (noise q Δ εn εd) (εn / εd) /-- - Notion of privacy composes by addition. + Privacy composes by addition. -/ compose_prop : {U V : Type} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] → [Inhabited U] → [MeasurableSpace V] → [Countable V] → [DiscreteMeasurableSpace V] → [Inhabited V] → ∀ m₁ : Mechanism T U, ∀ m₂ : Mechanism T V, ∀ ε₁ ε₂ ε₃ ε₄ : ℕ+, prop m₁ (ε₁ / ε₂) → prop m₂ (ε₃ / ε₄) → prop (privCompose m₁ m₂) ((ε₁ / ε₂) + (ε₃ / ε₄)) + /- + Uniformity conditions for adaptive composition + -/ + -- adaptive_unif_prop {U : Type} : (U -> Mechanism T Z) -> Prop + /- + Notion of privacy composes by addition + -/ + -- adaptive_compose_prop : {U V : Type} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] → [Inhabited U] → [MeasurableSpace V] → [Countable V] → [DiscreteMeasurableSpace V] → [Inhabited V] → ∀ m₁ : Mechanism T U, ∀ m₂ : U -> Mechanism T V, ∀ ε₁ ε₂ ε₃ ε₄ : ℕ+, + -- prop m₁ (ε₁ / ε₂) → (∀ u, prop (m₂ u) (ε₃ / ε₄)) -> adaptive_unif_prop m₂ → prop (privComposeAdaptive m₁ m₂) ((ε₁ / ε₂) + (ε₃ / ε₄)) + /-- + Requirement for postcomposition to hold. + -/ + postprocess_prop_f : {U V : Type} -> (f : U -> V) -> Prop /-- - Notion of privacy is invariant under post-processing. + Privacy is invariant under post-processing. -/ - postprocess_prop : {U : Type} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] → [Inhabited U] → { pp : U → V } → Function.Surjective pp → ∀ m : Mechanism T U, ∀ ε₁ ε₂ : ℕ+, + postprocess_prop : {U : Type} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] → [Inhabited U] → { pp : U → V } → postprocess_prop_f pp → ∀ m : Mechanism T U, ∀ ε₁ ε₂ : ℕ+, prop m (ε₁ / ε₂) → prop (privPostProcess m pp) (ε₁ / ε₂) @[simp] -lemma bind_bind_indep (p : Mechanism T U) (q : Mechanism T V) (h : U → V → SLang A) : - (fun l => (p l).probBind (fun a : U => (q l).probBind fun b : V => h a b)) - = - fun l => (privCompose p q l).probBind (fun z => h z.1 z.2) := by +lemma bind_bind_indep (p : Mechanism T U) (q : Mechanism T V) (h : U → V → PMF A) : + (fun l => (p l) >>= (fun a : U => (q l) >>= fun b : V => h a b)) = + fun l => (privCompose p q l) >>= (fun z => h z.1 z.2) := by ext l x simp [privCompose, tsum_prod'] - apply tsum_congr - intro b - rw [← ENNReal.tsum_mul_left] - apply tsum_congr - intro c - rw [← mul_assoc] - congr 1 - rw [tsum_eq_single b] - . congr 1 - rw [tsum_eq_single c] - . simp - . intro b' h1 - simp - intro h2 - subst h2 - contradiction - . intro b' h1 - rw [tsum_eq_single c] - . simp - intro h2 - subst h2 - contradiction - . intro b'' h2 - simp - intro h3 h4 - subst h3 - subst h4 - contradiction -lemma compose_sum_rw (nq1 : List T → SLang U) (nq2 : List T → SLang V) (b : U) (c : V) (l : List T) : - (∑' (a : U), nq1 l a * ∑' (a_1 : V), if b = a ∧ c = a_1 then nq2 l a_1 else 0) = nq1 l b * nq2 l c := by - have A : ∀ a : U, ∀ b : U, (∑' (a_1 : V), if b = a ∧ c = a_1 then nq2 l a_1 else 0) = if b = a then (∑' (a_1 : V), if c = a_1 then nq2 l a_1 else 0) else 0 := by +lemma compose_sum_rw (nq1 : U -> ENNReal) (nq2 : V -> ENNReal) (b : U) (c : V) : + (∑' (a : U), nq1 a * ∑' (a_1 : V), if b = a ∧ c = a_1 then nq2 a_1 else 0) = nq1 b * nq2 c := by + have A : ∀ a : U, ∀ b : U, (∑' (a_1 : V), if b = a ∧ c = a_1 then nq2 a_1 else 0) = if b = a then (∑' (a_1 : V), if c = a_1 then nq2 a_1 else 0) else 0 := by intro x y split . rename_i h @@ -131,7 +161,7 @@ lemma compose_sum_rw (nq1 : List T → SLang U) (nq2 : List T → SLang V) (b : rw [A] rw [ENNReal.tsum_eq_add_tsum_ite b] simp - have B : ∀ x : U, (if x = b then 0 else if b = x then nq1 l x * ∑' (a_1 : V), if c = a_1 then nq2 l a_1 else 0 else 0) = 0 := by + have B : ∀ x : U, (if x = b then 0 else if b = x then nq1 x * ∑' (a_1 : V), if c = a_1 then nq2 a_1 else 0 else 0) = 0 := by intro x split . simp @@ -150,7 +180,7 @@ lemma compose_sum_rw (nq1 : List T → SLang U) (nq2 : List T → SLang V) (b : congr 1 rw [ENNReal.tsum_eq_add_tsum_ite c] simp - have C :∀ x : V, (if x = c then 0 else if c = x then nq2 l x else 0) = 0 := by + have C :∀ x : V, (if x = c then 0 else if c = x then nq2 x else 0) = 0 := by intro x split . simp @@ -167,47 +197,11 @@ lemma compose_sum_rw (nq1 : List T → SLang U) (nq2 : List T → SLang V) (b : rw [C] simp -/-- -Composed queries are normalizable. --/ -theorem privCompose_NonTopSum {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nt1 : NonTopSum nq1) (nt2 : NonTopSum nq2) : - NonTopSum (privCompose nq1 nq2) := by - simp [NonTopSum] at * - intro l - replace nt1 := nt1 l - replace nt2 := nt2 l - simp [privCompose] - rw [ENNReal.tsum_prod'] - conv => - right - left - right - intro a - right - intro b - simp - rw [compose_sum_rw] - conv => - right - left - right - intro a - rw [ENNReal.tsum_mul_left] - rw [ENNReal.tsum_mul_right] - rw [mul_eq_top] - intro H - cases H - . rename_i H - cases H - contradiction - . rename_i H - cases H - contradiction /-- All outputs of a composed query have nonzero probability. -/ -theorem privCompose_NonZeroNQ {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nn1 : NonZeroNQ nq1) (nn2 : NonZeroNQ nq2) : +theorem privCompose_NonZeroNQ {nq1 : Mechanism T U} {nq2 : Mechanism T V} (nn1 : NonZeroNQ nq1) (nn2 : NonZeroNQ nq2) : NonZeroNQ (privCompose nq1 nq2) := by simp [NonZeroNQ] at * intro l a b @@ -216,6 +210,9 @@ theorem privCompose_NonZeroNQ {nq1 : List T → SLang U} {nq2 : List T → SLang simp [privCompose] exists a +/-- +Partition series into fibers. `g` maps an element to its fiber. +-/ theorem ENNReal.HasSum_fiberwise {f : T → ENNReal} {a : ENNReal} (hf : HasSum f a) (g : T → V) : HasSum (fun c : V ↦ ∑' b : g ⁻¹' {c}, f b) a := by let A := (Equiv.sigmaFiberEquiv g) @@ -229,6 +226,9 @@ theorem ENNReal.HasSum_fiberwise {f : T → ENNReal} {a : ENNReal} (hf : HasSum . rfl . apply ENNReal.summable +/-- +Partition series into fibers. `g` maps an element to its fiber. +-/ theorem ENNReal.tsum_fiberwise (p : T → ENNReal) (f : T → V) : ∑' (x : V), ∑' (b : (f ⁻¹' {x})), p b = ∑' i : T, p i := by @@ -237,6 +237,9 @@ theorem ENNReal.tsum_fiberwise (p : T → ENNReal) (f : T → V) : apply Summable.hasSum exact ENNReal.summable +/-- +Rewrite a series into a sum over fibers. `f` maps an element into its fiber. +-/ theorem fiberwisation (p : T → ENNReal) (f : T → V) : (∑' i : T, p i) = ∑' (x : V), if {a : T | x = f a} = {} then 0 else ∑'(i : {a : T | x = f a}), p i := by @@ -271,7 +274,11 @@ lemma condition_to_subset (f : U → V) (g : U → ENNReal) (x : V) : simp rw [B] -theorem privPostProcess_NonZeroNQ {nq : List T → SLang U} {f : U → V} (nn : NonZeroNQ nq) (sur : Function.Surjective f) : + +/-- +Postprocessing by a surjection preserves `NonZeroNQ`. +-/ +theorem privPostProcess_NonZeroNQ {nq : Mechanism T U} {f : U → V} (nn : NonZeroNQ nq) (sur : Function.Surjective f) : NonZeroNQ (privPostProcess nq f) := by simp [NonZeroNQ, Function.Surjective, privPostProcess] at * intros l n @@ -283,26 +290,4 @@ theorem privPostProcess_NonZeroNQ {nq : List T → SLang U} {f : U → V} (nn : . rw [h] . apply nn -theorem privPostProcess_NonTopSum {nq : List T → SLang U} (f : U → V) (nt : NonTopSum nq) : - NonTopSum (privPostProcess nq f) := by - simp [NonTopSum, privPostProcess] at * - intros l - have nt := nt l - rw [← ENNReal.tsum_fiberwise _ f] at nt - conv => - right - left - right - intro n - rw [condition_to_subset] - have A : ∀ x : V, f ⁻¹' {x} = {y | x = f y} := by - aesop - conv => - right - left - right - intro x - rw [← A] - trivial - end SLang diff --git a/SampCert/DifferentialPrivacy/Neighbours.lean b/SampCert/DifferentialPrivacy/Neighbours.lean index fe541bba..e9bb31fc 100644 --- a/SampCert/DifferentialPrivacy/Neighbours.lean +++ b/SampCert/DifferentialPrivacy/Neighbours.lean @@ -7,16 +7,31 @@ Authors: Jean-Baptiste Tristan /-! # Neighbours -This file defines the notion of neighbouring lists, in order to define a notion of sensitivity. +This file defines neighbouring lists. -/ variable {T : Type} /-- -The notion of "difference" between lists for differential privacy. +Lists which differ by the inclusion or modification of an element. + +This is SampCert's private property. -/ inductive Neighbour (l₁ l₂ : List T) : Prop where | Addition : l₁ = a ++ b → l₂ = a ++ [n] ++ b → Neighbour l₁ l₂ | Deletion : l₁ = a ++ [n] ++ b → l₂ = a ++ b → Neighbour l₁ l₂ | Update : l₁ = a ++ [n] ++ b → l₂ = a ++ [m] ++ b -> Neighbour l₁ l₂ + + +/-- +Neighbour relation is symmetric. +-/ +def Neighbour_symm (l₁ l₂ : List T) (H : Neighbour l₁ l₂) : Neighbour l₂ l₁ := by + cases H + · rename_i _ _ _ Hl1 Hl2 + exact Neighbour.Deletion Hl2 Hl1 + · rename_i _ _ _ Hl1 Hl2 + exact Neighbour.Addition Hl2 Hl1 + · rename_i _ _ _ _ Hl1 Hl2 + exact Neighbour.Update Hl2 Hl1 diff --git a/SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean b/SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean new file mode 100644 index 00000000..0d9db6a7 --- /dev/null +++ b/SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean @@ -0,0 +1,134 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jean-Baptiste Tristan, Markus de Medeiros +-/ +import SampCert.DifferentialPrivacy.Abstract +import SampCert.DifferentialPrivacy.Pure.DP +import Mathlib.Data.Set.Defs +import Mathlib.Data.Set.Prod +import Mathlib.Logic.IsEmpty + +noncomputable section + +open Classical Set + +variable [Hu : Nonempty U] + +/-- +Mediant inequality +-/ +lemma tsum_mediant (f g : U -> ENNReal) (hg0 : ∀ u, g u ≠ 0) (hf0 : ∀ u, f u ≠ 0): + (∑' (u : U), f u) / (∑' (u : U), g u) ≤ ⨆ u, f u / g u := by + + -- We need this to discharge side conditions in this proof, but we can get away with + -- some classical reasoning instead + cases (Classical.em (∀ u , g u ≠ ⊤)) + case inr => + rename_i Hk + -- rcases Hk with ⟨ ucont, Hcont ⟩ + have hgtop : ∃ u, g u = ⊤ := by apply (Decidable.not_forall_not.mp Hk) + have sumtop : ∑' (u : U) , g u = ⊤ := by exact ENNReal.tsum_eq_top_of_eq_top hgtop + rw [sumtop] + simp + case inl => + rename_i assumption_g + -- cases (isEmpty_or_nonempty U) + -- · rename_i HU + -- rw [iSup_of_empty] + -- rw [tsum_empty] + -- rw [tsum_empty] + -- simp + -- · rename_i Hu + rcases Hu with ⟨ u0 ⟩ + apply (ENNReal.div_le_iff_le_mul _ _).mpr + · rw [← ENNReal.tsum_mul_left] + apply ENNReal.tsum_le_tsum + intro u + apply (ENNReal.div_le_iff_le_mul _ _).mp + · refine (le_iSup (fun u => HDiv.hDiv (f u) (g u)) u) + · left; apply hg0 + · right + apply ne_of_gt + apply (LT.lt.trans_le ?g1 ?g2) + case g2 => + apply le_iSup + apply u + refine (ENNReal.div_pos (hf0 u) ?g1.hb) + apply assumption_g + · left + apply ne_of_gt + apply (LT.lt.trans_le ?z1 ?z2) + case z2 => + apply ENNReal.le_tsum + apply u0 + exact pos_iff_ne_zero.mpr (hg0 u0) + · right + apply ne_of_gt + apply (LT.lt.trans_le ?z3 ?z4) + case z4 => + apply le_iSup + apply u0 + refine (ENNReal.div_pos (hf0 u0) ?z6) + apply assumption_g + +lemma bounded_quotient (f g : U -> ENNReal) (b : ENNReal) (h_bound : ∀ (u : U), f u / g u ≤ b) (hg0 : ∀ u, g u ≠ 0) (hf0 : ∀ u, f u ≠ 0) : + (∑' (u : U), f u) / (∑' (u : U), g u) ≤ b := by + apply le_trans + · refine (tsum_mediant _ _ hg0 hf0) + · simp + assumption + +namespace SLang + +-- Better proof for Pure DP adaptive composition +theorem PureDP_ComposeAdaptive' (nq1 : List T → SLang U) (nq2 : U -> List T → SLang V) (ε₁ ε₂ ε₃ ε₄ : ℕ+) (h1 : PureDP nq1 ((ε₁ : ℝ) / ε₂)) (h2 : ∀ u : U, PureDP (nq2 u) ((ε₃ : ℝ) / ε₄)) : + PureDP (privComposeAdaptive nq1 nq2) (((ε₁ : ℝ) / ε₂) + ((ε₃ : ℝ) / ε₄)) := by + simp [PureDP] at * + rcases h1 with ⟨h1a, h1nz⟩ + rw [event_eq_singleton] at * + simp [DP_singleton] at * + apply And.intro + · intros l₁ l₂ Hl₁l₂ u v + rw [privComposeChainRule] + rw [privComposeChainRule] + rw [Real.exp_add] + rw [ENNReal.ofReal_mul ?s1] + case s1 => apply Real.exp_nonneg + rw [ENNReal.div_eq_inv_mul] + rw [ENNReal.mul_inv] + · rw [<- mul_assoc] + rw [mul_right_comm] + conv => + lhs + arg 1 + rw [mul_assoc] + rw [mul_right_comm] + rw [← ENNReal.div_eq_inv_mul] + rw [← ENNReal.div_eq_inv_mul] + rcases h2 u with ⟨ h2a'_pre, _ ⟩ + rw [event_eq_singleton] at h2a'_pre + simp [DP_singleton] at h2a'_pre + exact (mul_le_mul' (h1a l₁ l₂ Hl₁l₂ u) (h2a'_pre l₁ l₂ Hl₁l₂ v)) + · left + apply h1nz + · right + rcases (h2 u) with ⟨ _ , h2nz ⟩ + apply h2nz + · simp only [NonZeroNQ] + intros l n + simp only [privComposeAdaptive , bind, pure, bind_pure, bind_apply] + apply ne_of_gt + apply (LT.lt.trans_le ?g1 ?g2) + case g2 => + apply ENNReal.le_tsum + apply n.1 + apply ENNReal.mul_pos + · apply h1nz + · simp + exists n.2 + simp + rcases (h2 n.1) with ⟨ _ , H2nz ⟩ + apply H2nz + +end SLang diff --git a/SampCert/DifferentialPrivacy/Pure/Composition.lean b/SampCert/DifferentialPrivacy/Pure/Composition.lean index 18504502..c781260a 100644 --- a/SampCert/DifferentialPrivacy/Pure/Composition.lean +++ b/SampCert/DifferentialPrivacy/Pure/Composition.lean @@ -7,14 +7,26 @@ import SampCert.DifferentialPrivacy.Abstract import SampCert.DifferentialPrivacy.Pure.DP import Mathlib.Data.Set.Defs import Mathlib.Data.Set.Prod +import Mathlib.Logic.IsEmpty + +/-! +# Pure Composition in Pure Differential Privacy + +This file proves a pure DP privacy bound on composed independent queries. +-/ noncomputable section open Classical Set +variable [Hu : Nonempty U] + namespace SLang -theorem PureDP_Compose' {nq1 : Mechanism T U} {nq2 : List T → SLang V} {ε₁ ε₂ ε₃ ε₄ : ℕ+} (h1 : PureDP nq1 ((ε₁ : ℝ) / ε₂)) (h2 : PureDP nq2 ((ε₃ : ℝ) / ε₄)) : +/-- +Pure DP privacy bound for ``privCompose``. +-/ +theorem privCompose_DP_bound {nq1 : Mechanism T U} {nq2 : Mechanism T V} {ε₁ ε₂ ε₃ ε₄ : ℕ+} (h1 : PureDP nq1 ((ε₁ : ℝ) / ε₂)) (h2 : PureDP nq2 ((ε₃ : ℝ) / ε₄)) : DP (privCompose nq1 nq2) (((ε₁ : ℝ) / ε₂) + ((ε₃ : ℝ) / ε₄)) := by simp [PureDP] at * rcases h1 with ⟨h1a, _⟩ @@ -57,7 +69,11 @@ theorem PureDP_Compose' {nq1 : Mechanism T U} {nq2 : List T → SLang V} {ε₁ . aesop . aesop -theorem PureDP_Compose (nq1 : List T → SLang U) (nq2 : List T → SLang V) (ε₁ ε₂ ε₃ ε₄ : ℕ+) (h : PureDP nq1 ((ε₁ : ℝ) / ε₂)) (h' : PureDP nq2 ((ε₃ : ℝ) / ε₄)) : + +/-- +Pure DP satisfies pure differential privacy. +-/ +theorem privCompose_DP (nq1 : Mechanism T U) (nq2 : Mechanism T V) (ε₁ ε₂ ε₃ ε₄ : ℕ+) (h : PureDP nq1 ((ε₁ : ℝ) / ε₂)) (h' : PureDP nq2 ((ε₃ : ℝ) / ε₄)) : PureDP (privCompose nq1 nq2) (((ε₁ : ℝ) / ε₂) + ((ε₃ : ℝ) / ε₄)) := by simp [PureDP] at * have hc := h @@ -65,7 +81,7 @@ theorem PureDP_Compose (nq1 : List T → SLang U) (nq2 : List T → SLang V) (ε rcases h with ⟨ _ , h2 ⟩ rcases h' with ⟨ _ , h'2 ⟩ constructor - . apply PureDP_Compose' hc h'c + . apply privCompose_DP_bound hc h'c . apply privCompose_NonZeroNQ h2 h'2 end SLang diff --git a/SampCert/DifferentialPrivacy/Pure/Mechanism/Code.lean b/SampCert/DifferentialPrivacy/Pure/Mechanism/Code.lean index b8ff5a4e..6d82adf7 100644 --- a/SampCert/DifferentialPrivacy/Pure/Mechanism/Code.lean +++ b/SampCert/DifferentialPrivacy/Pure/Mechanism/Code.lean @@ -3,13 +3,20 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SampCert.Samplers.LaplaceGen.Code +import SampCert.Samplers.LaplaceGen.Properties + +/-! +# Implementation of ``privNoisedQueryPure`` +-/ noncomputable section namespace SLang -def privNoisedQueryPure (query : List T → ℤ) (Δ : ℕ+) (ε₁ ε₂ : ℕ+) (l : List T) : SLang ℤ := do - DiscreteLaplaceGenSample (Δ * ε₂) ε₁ (query l) +/-- +Add noise to a a query from the discrete Laplace distribution in order to obtain a (ε₁/ε₂)-DP mechanism from a Δ-sensitive query. +-/ +def privNoisedQueryPure (query : List T → ℤ) (Δ : ℕ+) (ε₁ ε₂ : ℕ+) (l : List T) : PMF ℤ := do + DiscreteLaplaceGenSamplePMF (Δ * ε₂) ε₁ (query l) end SLang diff --git a/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean index ff3d3605..7d1e3214 100644 --- a/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean +++ b/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean @@ -7,15 +7,26 @@ import SampCert.DifferentialPrivacy.Pure.DP import SampCert.DifferentialPrivacy.Pure.Mechanism.Code import SampCert.Samplers.LaplaceGen.Basic +/-! +# Properties of ``privNoisedQueryPure`` + +This file proves pure differential privacy for ``privNoisedQueryPure``. +-/ + noncomputable section open Classical Nat Int Real ENNReal MeasureTheory Measure namespace SLang +/-- +Noised query has nonzero probability over entire domain. +-/ theorem NoisedQuery_NonZeroNQPureDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) : NonZeroNQ (privNoisedQueryPure query Δ ε₁ ε₂) := by simp [NonZeroNQ, privNoisedQueryPure] + simp [DiscreteLaplaceGenSamplePMF] + simp [DFunLike.coe, PMF.instFunLike] intro l n apply Real.mul_pos . rw [_root_.div_pos_iff] @@ -27,12 +38,12 @@ theorem NoisedQuery_NonZeroNQPureDP (query : List T → ℤ) (Δ ε₁ ε₂ : apply add_pos A Real.zero_lt_one . apply exp_pos -theorem natAbs_to_abs (a b : ℤ) : +lemma natAbs_to_abs (a b : ℤ) : (a - b).natAbs = |(a : ℝ) - (b : ℝ)| := by rw [Int.cast_natAbs] simp only [cast_abs, Int.cast_sub] -theorem normalizing_constant_nonzero (ε₁ ε₂ Δ : ℕ+) : +lemma normalizing_constant_nonzero (ε₁ ε₂ Δ : ℕ+) : (rexp (ε₁ / (Δ * ε₂)) - 1) / (rexp (ε₁ / (Δ * ε₂)) + 1) ≠ 0 := by field_simp intro h @@ -47,12 +58,18 @@ theorem normalizing_constant_nonzero (ε₁ ε₂ Δ : ℕ+) : rw [h] at C contradiction -theorem NoisedQuery_PureDP' (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_sensitivity : sensitivity query Δ) : + +/-- +Differential privacy bound for a ``privNoisedQueryPure`` +-/ +theorem privNoisedQueryPure_DP_bound (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_sensitivity : sensitivity query Δ) : DP (privNoisedQueryPure query Δ ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by rw [event_eq_singleton] at * simp [DP_singleton] at * intros l₁ l₂ neighbours x simp [privNoisedQueryPure] + simp [DiscreteLaplaceGenSamplePMF] + simp [DFunLike.coe, PMF.instFunLike] rw [← ENNReal.ofReal_div_of_pos] . apply ofReal_le_ofReal rw [division_def] @@ -117,11 +134,15 @@ theorem NoisedQuery_PureDP' (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bo exact (add_lt_add_iff_right 1).mpr A . apply exp_pos -theorem NoisedQuery_PureDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_sensitivity : sensitivity query Δ) : + +/-- +Laplace noising mechanism ``privNoisedQueryPure`` produces a pure ``ε₁/ε₂``-DP mechanism from a Δ-sensitive query. +-/ +theorem privNoisedQueryPure_DP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_sensitivity : sensitivity query Δ) : PureDP (privNoisedQueryPure query Δ ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by simp [PureDP] constructor - . apply NoisedQuery_PureDP' + . apply privNoisedQueryPure_DP_bound apply bounded_sensitivity . apply NoisedQuery_NonZeroNQPureDP diff --git a/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean b/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean index d8c12a4d..c71230a6 100644 --- a/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean +++ b/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean @@ -8,13 +8,19 @@ import SampCert.DifferentialPrivacy.Pure.DP import Mathlib.Data.Set.Defs import Mathlib.Data.Set.Prod +/-! +# ``privPostProcess`` pure DP + +This file establishes a pure DP bound for ``privPostProcess`` +-/ + noncomputable section open Classical Set namespace SLang -theorem PureDP_PostProcess' {nq : Mechanism T U} {ε₁ ε₂ : ℕ+} (h : PureDP nq ((ε₁ : ℝ) / ε₂)) (f : U → V) : +lemma privPostProcess_DP_bound {nq : Mechanism T U} {ε₁ ε₂ : ℕ+} (h : PureDP nq ((ε₁ : ℝ) / ε₂)) (f : U → V) : DP (privPostProcess nq f) (((ε₁ : ℝ) / ε₂)) := by simp [PureDP] at * rcases h with ⟨ha, _⟩ @@ -37,13 +43,16 @@ theorem PureDP_PostProcess' {nq : Mechanism T U} {ε₁ ε₂ : ℕ+} (h : PureD exact Real.exp_pos ((ε₁: ℝ) / ε₂) . simp -theorem PureDP_PostProcess {f : U → V} (sur : Function.Surjective f) (nq : List T → SLang U) (ε₁ ε₂ : ℕ+) (h : PureDP nq ((ε₁ : ℝ) / ε₂)) : +/-- +``privPostProcess`` satisfies pure DP, for any surjective postprocessing function. +-/ +theorem PureDP_PostProcess {f : U → V} (sur : Function.Surjective f) (nq : Mechanism T U) (ε₁ ε₂ : ℕ+) (h : PureDP nq ((ε₁ : ℝ) / ε₂)) : PureDP (privPostProcess nq f) (((ε₁ : ℝ) / ε₂)) := by simp [PureDP] at * have hc := h rcases h with ⟨ _ , h2 ⟩ constructor - . apply PureDP_PostProcess' hc + . apply privPostProcess_DP_bound hc . apply privPostProcess_NonZeroNQ h2 sur end SLang diff --git a/SampCert/DifferentialPrivacy/Pure/System.lean b/SampCert/DifferentialPrivacy/Pure/System.lean index 0106fc7e..48a32fa6 100644 --- a/SampCert/DifferentialPrivacy/Pure/System.lean +++ b/SampCert/DifferentialPrivacy/Pure/System.lean @@ -7,17 +7,32 @@ import SampCert.DifferentialPrivacy.Abstract import SampCert.DifferentialPrivacy.Pure.DP import SampCert.DifferentialPrivacy.Pure.Mechanism.Basic import SampCert.DifferentialPrivacy.Pure.Composition +import SampCert.DifferentialPrivacy.Pure.AdaptiveComposition import SampCert.DifferentialPrivacy.Pure.Postprocessing +/-! +# Pure DP system +-/ + namespace SLang variable { T : Type } +/-- +Pure ε-DP with noise drawn from the discrete Laplace distribution. +-/ noncomputable instance PureDPSystem : DPSystem T where prop := PureDP noise := privNoisedQueryPure - noise_prop := NoisedQuery_PureDP - compose_prop := PureDP_Compose +-- adaptive_unif_prop := fun _ => True +-- adaptive_compose_prop := fun {U V} +-- [MeasurableSpace U] [Countable U] [DiscreteMeasurableSpace U] [Inhabited U] +-- [MeasurableSpace V] [Countable V] [DiscreteMeasurableSpace V] [Inhabited V] +-- m₁ m₂ ε₁ ε₂ ε₃ ε₄ a a_1 _ => +-- PureDP_ComposeAdaptive' m₁ m₂ ε₁ ε₂ ε₃ ε₄ a a_1 + noise_prop := privNoisedQueryPure_DP + compose_prop := privCompose_DP + postprocess_prop_f := Function.Surjective postprocess_prop := PureDP_PostProcess end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean index 66fab2ec..2cf226d8 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Code.lean @@ -10,7 +10,7 @@ import SampCert.DifferentialPrivacy.Queries.BoundedSum.Code /-! # ``privNoisedBoundedMean`` Implementation -This file defines a differentially private noising of a bounded mean query. +This file defines a differentially private bounded mean query. -/ noncomputable section @@ -20,9 +20,9 @@ namespace SLang variable [dps : DPSystem ℕ] /-- -Compute a noised mean using a noised sum and noised count +Compute a noised mean using a noised sum and noised count. -/ -def privNoisedBoundedMean (U : ℕ+) (ε₁ ε₂ : ℕ+) (l : List ℕ) : SLang ℚ := do +def privNoisedBoundedMean (U : ℕ+) (ε₁ ε₂ : ℕ+) (l : List ℕ) : PMF ℚ := do let S ← privNoisedBoundedSum U ε₁ (2 * ε₂) l let C ← privNoisedCount ε₁ (2 * ε₂) l return S / C diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean index 43befc61..5cd28b1b 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean @@ -39,14 +39,16 @@ lemma budget_split (ε₁ ε₂ : ℕ+) : field_simp ring_nf + /-- DP bound for noised mean. -/ -theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) : +theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) + (H : dps.postprocess_prop_f (fun a : ℤ × ℤ => (a.1 : ℚ) / (a.2 : ℚ))) : dps.prop (privNoisedBoundedMean U ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by unfold privNoisedBoundedMean - simp - apply dps.postprocess_prop div_surjective + rw [bind_bind_indep] + apply dps.postprocess_prop H rw [budget_split] apply dps.compose_prop . apply privNoisedBoundedSum_DP diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean index 96c10995..12a37d7a 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Code.lean @@ -11,7 +11,7 @@ import Init.Data.Int.Order /-! # ``privNoisedBoundedSum`` Implementation -This file defines a differentially private noising of a bounded sum query. +This file defines a differentially private bounded sum query. -/ noncomputable section @@ -29,7 +29,7 @@ def exactBoundedSum (U : ℕ+) (l : List ℕ) : ℤ := /-- Noised bounded sum query obtained by applying the DP noise mechanism to the bounded sum. -/ -def privNoisedBoundedSum (U : ℕ+) (ε₁ ε₂ : ℕ+) (l : List ℕ) : SLang ℤ := do +def privNoisedBoundedSum (U : ℕ+) (ε₁ ε₂ : ℕ+) (l : List ℕ) : PMF ℤ := do dps.noise (exactBoundedSum U) U ε₁ ε₂ l end SLang diff --git a/SampCert/DifferentialPrivacy/Queries/Count/Code.lean b/SampCert/DifferentialPrivacy/Queries/Count/Code.lean index 7e841c6e..a94db31e 100644 --- a/SampCert/DifferentialPrivacy/Queries/Count/Code.lean +++ b/SampCert/DifferentialPrivacy/Queries/Count/Code.lean @@ -19,14 +19,14 @@ variable {T : Type} variable [dps : DPSystem T] /-- -Query to count the size of the input +Query to count the size of the input list. -/ def exactCount (l : List T) : ℤ := List.length l /-- -Noised counting mechanism from the DP system +A noised counting mechanism. -/ -def privNoisedCount (ε₁ ε₂ : ℕ+) (l : List T) : SLang ℤ := do +def privNoisedCount (ε₁ ε₂ : ℕ+) (l : List T) : PMF ℤ := do dps.noise exactCount 1 ε₁ ε₂ l end SLang diff --git a/SampCert/DifferentialPrivacy/RenyiDivergence.lean b/SampCert/DifferentialPrivacy/RenyiDivergence.lean index be404036..d3b45a4f 100644 --- a/SampCert/DifferentialPrivacy/RenyiDivergence.lean +++ b/SampCert/DifferentialPrivacy/RenyiDivergence.lean @@ -6,49 +6,1148 @@ Authors: Jean-Baptiste Tristan import Mathlib.Topology.Algebra.InfiniteSum.Ring import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable import Mathlib.Analysis.SpecialFunctions.Pow.NNReal +import SampCert.Util.Log +import Mathlib.Probability.ProbabilityMassFunction.Basic +import Mathlib.Probability.ProbabilityMassFunction.Integrals +import Mathlib.Analysis.Convex.Integral /-! Renyi Divergence -This file defines the Renyi divergence and equations for evaluating its expectation. +This file defines the Renyi divergence, and equations for evaluating it. -/ -open Real ENNReal +open Real ENNReal PMF Nat Int MeasureTheory Measure PMF +open Classical + + +/-- +Simplified consequence of absolute continuity between PMF's. +-/ +def AbsCts (p q : T -> ENNReal) : Prop := ∀ x : T, q x = 0 -> p x = 0 + + +/-- +All PMF's are absolutely continuous with respect to themselves. +-/ +lemma AbsCts_refl (q : PMF T) : AbsCts q q := by + rw [AbsCts] + simp + +/-- +Obtain simplified absolute continuity from the measure-theoretic version of absolute continuity in a discrete space. +-/ +lemma PMF_AbsCts [MeasurableSpace T] [MeasurableSingletonClass T] (p q : PMF T) (H : AbsolutelyContinuous (PMF.toMeasure p) (PMF.toMeasure q)) : AbsCts p q := by + rw [AbsolutelyContinuous] at H + rw [AbsCts] + intro x Hx + have Hxm : q.toMeasure { x } = 0 := by + rw [toMeasure] + simp + apply (toOuterMeasure_apply_eq_zero_iff q {x}).mpr + exact Set.disjoint_singleton_right.mpr fun a => a Hx + have H := H Hxm + rw [toMeasure] at H + simp at * + have Hp : Disjoint p.support {x} := (toOuterMeasure_apply_eq_zero_iff p {x}).mp H + simp at Hp + assumption + +lemma PMF_mul_mul_inv_eq_mul_cancel (p q : PMF T) (HA : AbsCts p q) (a : T) : (p a / q a) * q a = p a := by + apply mul_mul_inv_eq_mul_cancel + · rw [AbsCts] at HA + intro + simp_all + · simp + have HK : (q a ≠ ⊤) := apply_ne_top q a + simp_all only [ne_eq, not_false_eq_true] + simp variable {T : Type} /-- -The Renyi divergence. +Definition of the Renyi divergence as an EReal. -/ -noncomputable def RenyiDivergence (p q : T → ENNReal) (α : ℝ) : ℝ := - (α - 1)⁻¹ * Real.log (∑' x : T, (p x)^α * (q x)^(1 - α)).toReal +noncomputable def RenyiDivergence_def (p q : PMF T) (α : ℝ) : EReal := + (α - 1)⁻¹ * (elog (∑' x : T, (p x)^α * (q x)^(1 - α))) /-- -Closed form of the series in the definition of hte Renyi divergence. +Rearrange the definition of ``RenyiDivergence_def`` to obtain an equation for the inner series. -/ -theorem RenyiDivergenceExpectation (p q : T → ENNReal) {α : ℝ} (h : 1 < α) (h1 : ∀ x : T, q x ≠ 0) (h2 : ∀ x : T, q x ≠ ⊤) : - (∑' x : T, (p x)^α * (q x)^(1 - α)) = ∑' x : T, (p x / q x)^α * (q x) := by - congr 4 - ext x - rw [ENNReal.rpow_sub] - . rw [← ENNReal.mul_comm_div] - rw [← ENNReal.div_rpow_of_nonneg] - . rw [ENNReal.rpow_one] - . apply le_of_lt (lt_trans Real.zero_lt_one h ) - . apply h1 x - . apply h2 x +lemma RenyiDivergence_def_exp (p q : PMF T) {α : ℝ} (h : 1 < α) : + eexp (((α - 1)) * RenyiDivergence_def p q α) = (∑' x : T, (p x)^α * (q x)^(1 - α)) := by + rw [RenyiDivergence_def] + rw [<- mul_assoc] + have H1 : (α.toEReal - OfNat.ofNat 1) = (α - OfNat.ofNat 1).toEReal := by + rw [EReal.coe_sub] + congr + have H2 : ((α.toEReal - OfNat.ofNat 1) * (α - OfNat.ofNat 1)⁻¹.toEReal = 1) := by + rw [H1] + rw [← EReal.coe_mul] + rw [mul_inv_cancel] + · simp + · linarith + simp [H2] + +/- +The Renyi divergence is monotonic in the value of its sum. +-/ +--lemma RenyiDivergence_mono_sum (x y : ℝ) (α : ℝ) (h : 1 < α) : (Real.exp ((α - 1) * x)) ≤ (Real.exp ((α - 1) * y)) -> (x ≤ y) := by +-- intro H +-- apply le_of_mul_le_mul_left +-- · exact exp_le_exp.mp H +-- · linarith /-- -Closed form for the Renti Divergence. +Renyi Divergence series written as a conditional expectation. -/ -theorem RenyiDivergenceExpectation' (p q : T → ENNReal) {α : ℝ} (h : 1 < α) (h1 : ∀ x : T, q x ≠ 0) (h2 : ∀ x : T, q x ≠ ⊤) : - (α - 1)⁻¹ * Real.log ((∑' x : T, (p x)^α * (q x)^(1 - α))).toReal = (α - 1)⁻¹ * Real.log (∑' x : T, (p x / q x)^α * (q x)).toReal := by +theorem RenyiDivergenceExpectation (p q : T → ENNReal) {α : ℝ} (h : 1 < α) (H : AbsCts p q) : + (∑' x : T, (p x)^α * (q x)^(1 - α)) = ∑' x: T, (p x / q x)^α * (q x) := by congr 4 ext x - rw [ENNReal.rpow_sub] - . rw [← ENNReal.mul_comm_div] - rw [← ENNReal.div_rpow_of_nonneg] - . rw [ENNReal.rpow_one] - . apply le_of_lt (lt_trans Real.zero_lt_one h ) - . apply h1 x - . apply h2 x + rw [AbsCts] at H + generalize Hvq : q x = vq + cases vq <;> simp + · -- q x = ⊤ + rw [ENNReal.zero_rpow_of_pos ?H] + case H => linarith + simp + right + apply h + · rename_i vq' + cases (Classical.em (vq' = 0)) + · -- q x = 0 + -- by abs. cty. p x = 0 + rename_i Hvq' + have Hp : p x = 0 := by + apply H + simp [Hvq, Hvq'] + simp [Hp, Hvq', Hvq] + left + linarith + · -- q x ∈ ℝ+ + rename_i Hvq' + generalize Hvp : p x = vp + cases vp <;> simp + · -- q x ∈ ℝ+, p x = ⊤ + rw [ENNReal.top_rpow_of_pos ?H] + case H => linarith + rw [top_mul'] + split + · exfalso + rename_i Hcont + apply Hvq' + have Hcont' : (vq' : ENNReal) = 0 ∧ 0 < (1-α) ∨ (vq' : ENNReal) = ⊤ ∧ (1-α)< 0 := by + exact rpow_eq_zero_iff.mp Hcont + cases Hcont' + · simp_all only [some_eq_coe, none_eq_top, zero_ne_top] + · simp_all only [some_eq_coe, none_eq_top, top_rpow_of_neg, coe_ne_top, sub_neg, and_true] + · rw [top_mul'] + split + · simp_all only [some_eq_coe, none_eq_top, zero_ne_top] + · rfl + · rename_i vp + cases (Classical.em (vq' = 0)) + · -- q x ∈ ℝ+, p x = 0 + rename_i Hvp' + simp_all + · -- q x ∈ ℝ+, p x ∈ ℝ+ + rename_i Hvp' + rw [ENNReal.rpow_sub] + . rw [← ENNReal.mul_comm_div] + rw [← ENNReal.div_rpow_of_nonneg] + . rw [ENNReal.rpow_one] + . apply le_of_lt (lt_trans Real.zero_lt_one h ) + · simp_all only [some_eq_coe, not_false_eq_true, ne_eq, coe_eq_zero] + · simp_all only [some_eq_coe, not_false_eq_true, ne_eq, coe_ne_top] + + +/-! +## Jensen's inequalitya +-/ +section Jensen + +variable {T : Type} +variable [t1 : MeasurableSpace T] +variable [t2 : MeasurableSingletonClass T] +variable [tcount : Countable T] -- New + +variable {U V : Type} +variable [m2 : MeasurableSpace U] +variable [count : Countable U] +variable [disc : DiscreteMeasurableSpace U] +variable [Inhabited U] + +lemma Integrable_rpow (f : T → ℝ) (nn : ∀ x : T, 0 ≤ f x) (μ : Measure T) (α : ENNReal) (mem : Memℒp f α μ) (h1 : α ≠ 0) (h2 : α ≠ ⊤) : + MeasureTheory.Integrable (fun x : T => (f x) ^ α.toReal) μ := by + have X := @MeasureTheory.Memℒp.integrable_norm_rpow T ℝ t1 μ _ f α mem h1 h2 + revert X + conv => + left + left + intro x + rw [← norm_rpow_of_nonneg (nn x)] + intro X + simp [Integrable] at * + constructor + . cases X + rename_i left right + rw [@aestronglyMeasurable_iff_aemeasurable] + apply AEMeasurable.pow_const + simp [Memℒp] at mem + cases mem + rename_i left' right' + rw [aestronglyMeasurable_iff_aemeasurable] at left' + simp [left'] + . rw [← hasFiniteIntegral_norm_iff] + simp [X] + +-- MARKUSDE: This lemma is derivable from ``Renyi_Jensen_strict_real``, however it requires a reduction +-- to first eliminate all elements (t : T) where q t = 0 from the series. +/-- +Jensen's inequality for the exponential applied to the real-valued function ``(⬝)^α``. +-/ +theorem Renyi_Jensen_real (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 < α) (h2 : ∀ x : T, 0 ≤ f x) (mem : Memℒp f (ENNReal.ofReal α) (PMF.toMeasure q)) : + ((∑' x : T, (f x) * (q x).toReal)) ^ α ≤ (∑' x : T, (f x) ^ α * (q x).toReal) := by + conv => + enter [1, 1, 1, x] + rw [mul_comm] + rw [← smul_eq_mul] + conv => + enter [2, 1, x] + rw [mul_comm] + rw [← smul_eq_mul] + rw [← PMF.integral_eq_tsum] + rw [← PMF.integral_eq_tsum] + + have A := @convexOn_rpow α (le_of_lt h) + have B : ContinuousOn (fun (x : ℝ) => x ^ α) (Set.Ici 0) := by + apply ContinuousOn.rpow + . exact continuousOn_id' (Set.Ici 0) + . exact continuousOn_const + . intro x h' + simp at h' + have OR : x = 0 ∨ 0 < x := by exact LE.le.eq_or_gt h' + cases OR + . rename_i h'' + subst h'' + right + apply lt_trans zero_lt_one h + . rename_i h'' + left + by_contra + rename_i h3 + subst h3 + simp at h'' + have C : @IsClosed ℝ UniformSpace.toTopologicalSpace (Set.Ici 0) := by + exact isClosed_Ici + have D := @ConvexOn.map_integral_le T ℝ t1 _ _ _ (PMF.toMeasure q) (Set.Ici 0) f (fun (x : ℝ) => x ^ α) (PMF.toMeasure.isProbabilityMeasure q) A B C + simp at D + apply D + . exact MeasureTheory.ae_of_all (PMF.toMeasure q) h2 + . apply MeasureTheory.Memℒp.integrable _ mem + rw [one_le_ofReal] + apply le_of_lt h + . rw [Function.comp_def] + have X : ENNReal.ofReal α ≠ 0 := by + simp + apply lt_trans zero_lt_one h + have Y : ENNReal.ofReal α ≠ ⊤ := by + simp + have Z := @Integrable_rpow T t1 f h2 (PMF.toMeasure q) (ENNReal.ofReal α) mem X Y + rw [toReal_ofReal] at Z + . exact Z + . apply le_of_lt + apply lt_trans zero_lt_one h + . have X : ENNReal.ofReal α ≠ 0 := by + simp + apply lt_trans zero_lt_one h + have Y : ENNReal.ofReal α ≠ ⊤ := by + simp + have Z := @Integrable_rpow T t1 f h2 (PMF.toMeasure q) (ENNReal.ofReal α) mem X Y + rw [toReal_ofReal] at Z + . exact Z + . apply le_of_lt + apply lt_trans zero_lt_one h + . apply MeasureTheory.Memℒp.integrable _ mem + rw [one_le_ofReal] + apply le_of_lt h + + +/-- +Strict version of Jensen't inequality applied to the function ``(⬝)^α``. +-/ +theorem Renyi_Jensen_strict_real (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 < α) (h2 : ∀ x : T, 0 ≤ f x) (mem : Memℒp f (ENNReal.ofReal α) (PMF.toMeasure q)) (HT_nz : ∀ t : T, q t ≠ 0): + ((∑' x : T, (f x) * (q x).toReal)) ^ α < (∑' x : T, (f x) ^ α * (q x).toReal) ∨ (∀ x : T, f x = ∑' (x : T), (q x).toReal * f x) := by + conv => + enter [1, 1, 1, 1, x] + rw [mul_comm] + rw [← smul_eq_mul] + conv => + enter [1, 2, 1, x] + rw [mul_comm] + rw [← smul_eq_mul] + rw [← PMF.integral_eq_tsum] + rw [← PMF.integral_eq_tsum] + + have A := strictConvexOn_rpow h + + have B : ContinuousOn (fun (x : ℝ) => x ^ α) (Set.Ici 0) := by + apply ContinuousOn.rpow + . exact continuousOn_id' (Set.Ici 0) + . exact continuousOn_const + . intro x h' + simp at h' + have OR : x = 0 ∨ 0 < x := by exact LE.le.eq_or_gt h' + cases OR + . rename_i h'' + subst h'' + right + apply lt_trans zero_lt_one h + . rename_i h'' + left + by_contra + rename_i h3 + subst h3 + simp at h'' + have C : @IsClosed ℝ UniformSpace.toTopologicalSpace (Set.Ici 0) := by + exact isClosed_Ici + have D := @StrictConvexOn.ae_eq_const_or_map_average_lt T ℝ t1 _ _ _ (PMF.toMeasure q) (Set.Ici 0) f (fun (x : ℝ) => x ^ α) ((PMF.toMeasure.isProbabilityMeasure q).toIsFiniteMeasure) A B C ?G1 ?G2 ?G3 + case G1 => + exact MeasureTheory.ae_of_all (PMF.toMeasure q) h2 + case G2 => + apply MeasureTheory.Memℒp.integrable _ mem + rw [one_le_ofReal] + apply le_of_lt h + case G3 => + rw [Function.comp_def] + have X : ENNReal.ofReal α ≠ 0 := by + simp + apply lt_trans zero_lt_one h + have Y : ENNReal.ofReal α ≠ ⊤ := by + simp + have Z := @Integrable_rpow T t1 f h2 (PMF.toMeasure q) (ENNReal.ofReal α) mem X Y + rw [toReal_ofReal] at Z + . exact Z + . apply le_of_lt + apply lt_trans zero_lt_one h + simp at D + · cases D + · rename_i HR + right + simp at HR + -- Because T is discrete, almost-everywhere equality should become equality + have HR' := @Filter.EventuallyEq.eventually _ _ (q.toMeasure.ae) f (Function.const T (⨍ (x : T), f x ∂q.toMeasure)) HR + simp [Filter.Eventually] at HR' + -- The measure of the compliment of the set in HR' is zero + simp [MeasureTheory.Measure.ae] at HR' + rw [PMF.toMeasure_apply _ _ ?Hmeas] at HR' + case Hmeas => + apply (@measurableSet_discrete _ _ ?DM) + apply MeasurableSingletonClass.toDiscreteMeasurableSpace + -- Sum is zero iff all elements are zero + apply ENNReal.tsum_eq_zero.mp at HR' + -- Indicator is zero when proposition is not true + intro x + have HR' := HR' x + simp at HR' + cases (Classical.em (f x = ⨍ (x : T), f x ∂q.toMeasure)) + · rename_i Heqx + -- Rewrite the average + rw [MeasureTheory.average] at Heqx + rw [MeasureTheory.integral_countable'] at Heqx + · simp at Heqx + conv at Heqx => + rhs + arg 1 + intro x + rw [PMF.toMeasure_apply_singleton] + · skip + · apply measurableSet_singleton + -- Interesting.... is this sum not just 1? + simp at * + apply Heqx + · simp + apply MeasureTheory.Memℒp.integrable _ mem + have X : (1 : ENNReal) = ENNReal.ofReal (1 : ℝ) := by simp + rw [X] + apply ofReal_le_ofReal_iff'.mpr + left + linarith + · -- At type T, q x is never zero + rename_i Hnex + exfalso + apply (HT_nz x) + apply HR' + apply Hnex + · rename_i HR + left + rw [<- MeasureTheory.integral_average] + rw [<- MeasureTheory.integral_average] + simp + rw [<- MeasureTheory.integral_average] + rw [<- MeasureTheory.integral_average] + simp + apply HR + . have X : ENNReal.ofReal α ≠ 0 := by + simp + apply lt_trans zero_lt_one h + have Y : ENNReal.ofReal α ≠ ⊤ := by + simp + have Z := @Integrable_rpow T t1 f h2 (PMF.toMeasure q) (ENNReal.ofReal α) mem X Y + rw [toReal_ofReal] at Z + . exact Z + . apply le_of_lt + apply lt_trans zero_lt_one h + . apply MeasureTheory.Memℒp.integrable _ mem + rw [one_le_ofReal] + apply le_of_lt h + +end Jensen + + +/-- +Quotient from the Real-valued Jenen's inequality applied to the series in the Renyi divergence. +-/ +noncomputable def Renyi_Jensen_f (p q : PMF T) : T -> ℝ := (fun z => (p z / q z).toReal) + +/-- +Summand from the Renyi divergence equals a real-valued summand, except in a special case. +-/ +lemma Renyi_Jensen_rw (p q : PMF T) {α : ℝ} (h : 1 < α) (H : AbsCts p q) (Hspecial : ∀ x : T, ¬(p x = ⊤ ∧ q x ≠ 0 ∧ q x ≠ ⊤)) (x : T) : + (p x / q x)^α * (q x) = ENNReal.ofReal (((Renyi_Jensen_f p q) x)^α * (q x).toReal) := by + simp [Renyi_Jensen_f] + rw [ENNReal.toReal_rpow] + rw [<- ENNReal.toReal_mul] + rw [ENNReal.ofReal_toReal] + apply mul_ne_top + · apply rpow_ne_top_of_nonneg + · linarith + · intro HK + apply ENNReal.div_eq_top.mp at HK + simp at HK + rw [AbsCts] at H + cases HK + · rename_i HK + rcases HK with ⟨ HK1, HK2 ⟩ + simp_all + · rename_i HK + rcases HK with ⟨ HK1, HK2 ⟩ + simp_all + apply HK2 + apply (Hspecial) + · apply HK1 + · intro Hcont1 + simp_all + · exact apply_ne_top q x + + +-- MARKUSDE: I think it might be possible to use `Renyi_Jensen_strict_real` in this proof instead, +-- this would eliminate the need for `Renyi_Jensen_real`. +/-- +Jensen's inquality applied to ENNReals, in the case that q is nonzero. +-/ +lemma Renyi_Jensen_ENNReal_reduct [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T] + (p q : PMF T) {α : ℝ} (h : 1 < α) (H : AbsCts p q) (Hq : ∀ t, q t ≠ 0) : + (∑' x : T, (p x / q x) * q x) ^ α ≤ (∑' x : T, (p x / q x) ^ α * q x) := by + have Hdiscr : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace + cases (Classical.em (∑' (a : T), (p a / q a) ^ α * q a ≠ ⊤)) + · rename_i Hnts + cases (Classical.em (∀ x : T, ¬(p x = ⊤ ∧ q x ≠ 0 ∧ q x ≠ ⊤))) + · -- Typical case + rename_i Hspecial + conv => + rhs + arg 1 + intro x + rw [Renyi_Jensen_rw p q h H Hspecial] + rw [<- ENNReal.ofReal_tsum_of_nonneg ?Hnonneg ?Hsummable] + case Hnonneg => + intro t + apply mul_nonneg + · refine rpow_nonneg ?ha.hx α + simp [Renyi_Jensen_f] + · exact toReal_nonneg + case Hsummable => + conv => + congr + intro x + rw [Renyi_Jensen_f] + conv => + arg 1 + intro x + lhs + rw [ENNReal.toReal_rpow] + conv => + arg 1 + intro x + rw [<- ENNReal.toReal_mul] + apply ENNReal.summable_toReal + assumption + have HRJf_nonneg (a : T) : 0 <= Renyi_Jensen_f p q a := by apply toReal_nonneg + have HRJf_nt (a : T) : p a / q a ≠ ⊤ := by + intro HK + have HK' : (p a ≠ 0 ∧ q a = 0 ∨ p a = ⊤ ∧ q a ≠ ⊤) := by exact div_eq_top.mp HK + cases HK' + · rename_i HK' + rcases HK' with ⟨ HK1 , HK2 ⟩ + rw [AbsCts] at H + simp_all only [ne_eq, not_and, Decidable.not_not, ENNReal.zero_div, zero_ne_top] + · rename_i HK' + rcases HK' with ⟨ HK1 , _ ⟩ + apply (Hspecial a) + simp_all + have Hsum_indicator (a : T) : ∑' (i : T), q i * Set.indicator {a} (fun x => 1) i = q a := by + have Hfun : (fun (i : T) => q i * Set.indicator {a} (fun x => 1) i) = (fun (i : T) => if i = a then q a else 0) := by + funext i + rw [Set.indicator] + split <;> simp <;> split <;> simp_all + rw [Hfun] + exact tsum_ite_eq a (q a) + apply (le_trans ?G1 ?G2) + case G2 => + apply (ofReal_le_ofReal ?Hle) + case Hle => + apply Renyi_Jensen_real + · apply h + · simp [Renyi_Jensen_f] + · simp [Memℒp] + constructor + . apply MeasureTheory.StronglyMeasurable.aestronglyMeasurable + apply Measurable.stronglyMeasurable + apply Measurable.ennreal_toReal + conv => + right + intro x + rw [division_def] + apply Measurable.mul + . apply measurable_discrete + . apply Measurable.inv + apply measurable_discrete + · simp [snorm] + split + · simp + · rename_i Hα + simp [snorm'] + rw [MeasureTheory.lintegral_countable'] + rw [toReal_ofReal (le_of_lt (lt_trans zero_lt_one h))] + apply rpow_lt_top_of_nonneg + · simp + apply le_of_not_ge Hα + · conv => + enter [1, 1, a, 1, 1] + rw [<- Real.toNNReal_eq_nnnorm_of_nonneg (HRJf_nonneg a)] + rw [Renyi_Jensen_f] + rw [<- ENNReal.ofReal.eq_1] + rw [ENNReal.ofReal_toReal (HRJf_nt a)] + rfl + conv => + enter [1, 1, a, 2] + simp [toMeasure] + simp [PMF.toOuterMeasure] + rw [Hsum_indicator] + apply Hnts + case G1 => + -- We need the latter fn to be summable or else it becomes zero and the inequality does not hold + rw [<- ENNReal.ofReal_rpow_of_nonneg ?Harg ?Hα] + case Harg => + apply tsum_nonneg + intro i + apply mul_nonneg + · apply HRJf_nonneg + · exact toReal_nonneg + case Hα => linarith + apply (ENNReal.rpow_le_rpow _ ?Hα') + case Hα' => linarith + conv => + rhs + arg 1 + arg 1 + intro a + rw [Renyi_Jensen_f] + rw [<- ENNReal.toReal_mul] + rw [<- ENNReal.tsum_toReal_eq] + · rw [ENNReal.ofReal_toReal] + conv => + enter [1, 1, a] + rw [PMF_mul_mul_inv_eq_mul_cancel p q H] + exact tsum_coe_ne_top p + · intro a + conv => + arg 1 + rw [PMF_mul_mul_inv_eq_mul_cancel p q H] + exact apply_ne_top p a + · -- Special case: There exists some element x0 with p x0 = ⊤ but q x0 ∈ ℝ+ + rename_i Hspecial + simp at * + rcases Hspecial with ⟨ x0, ⟨ H1, _, H3 ⟩⟩ + have HT1 : (∑' (x : T), p x / q x * q x) ^ α = ⊤ := by + apply rpow_eq_top_iff.mpr + right + apply And.intro + · apply ENNReal.tsum_eq_top_of_eq_top + exists x0 + apply mul_eq_top.mpr + right + apply And.intro + · apply div_eq_top.mpr + simp_all + · simp_all + · linarith + have HT2 : ∑' (x : T), (p x / q x) ^ α * q x = ⊤ := by + apply ENNReal.tsum_eq_top_of_eq_top + exists x0 + apply mul_eq_top.mpr + right + apply And.intro + · apply rpow_eq_top_iff.mpr + right + apply And.intro + · simp_all + exact top_div_of_ne_top H3 + · simp_all + linarith + · simp_all + rw [HT1, HT2] + · rename_i HStop + simp at * + rw [HStop] + exact OrderTop.le_top ((∑' (x : T), p x / q x * q x) ^ α) + + +/-- +On types where q is nonzero, Jensen's inequality for the Renyi divergence sum is tight only for equal distributions. +-/ +lemma Renyi_Jensen_ENNReal_converse_reduct [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T] + (p q : PMF T) {α : ℝ} (h : 1 < α) (H : AbsCts p q) (Hq : ∀ t, q t ≠ 0) + (Hsumeq : (∑' x : T, (p x / q x) * q x) ^ α = (∑' x : T, (p x / q x) ^ α * q x)) : + (p = q) := by + have Hdiscr : DiscreteMeasurableSpace T := MeasurableSingletonClass.toDiscreteMeasurableSpace + cases (Classical.em (∑' (a : T), (p a / q a) ^ α * q a ≠ ⊤)) + · -- Preliminary stuff, basically the same as the forward case + rename_i Hnts + cases (Classical.em (∀ x : T, ¬(p x = ⊤ ∧ q x ≠ 0 ∧ q x ≠ ⊤))) + · rename_i Hspecial + conv at Hsumeq => + rhs + arg 1 + intro x + rw [Renyi_Jensen_rw p q h H Hspecial] + rw [<- ENNReal.ofReal_tsum_of_nonneg ?Hnonneg ?Hsummable] at Hsumeq + case Hnonneg => + intro t + apply mul_nonneg + · refine rpow_nonneg ?ha.hx α + simp [Renyi_Jensen_f] + · exact toReal_nonneg + case Hsummable => + conv => + congr + intro x + rw [Renyi_Jensen_f] + conv => + enter [1, x, 1] + rw [ENNReal.toReal_rpow] + conv => + enter [1, x] + rw [<- ENNReal.toReal_mul] + apply ENNReal.summable_toReal + assumption + have HRJf_nonneg (a : T) : 0 <= Renyi_Jensen_f p q a := by apply toReal_nonneg + have HRJf_nt (a : T) : p a / q a ≠ ⊤ := by + intro HK + have HK' : (p a ≠ 0 ∧ q a = 0 ∨ p a = ⊤ ∧ q a ≠ ⊤) := by exact div_eq_top.mp HK + cases HK' + · rename_i HK' + rcases HK' with ⟨ HK1 , HK2 ⟩ + rw [AbsCts] at H + simp_all only [ne_eq, not_and, Decidable.not_not, ENNReal.zero_div, zero_ne_top] + · rename_i HK' + rcases HK' with ⟨ HK1 , _ ⟩ + apply (Hspecial a) + simp_all + have Hsum_indicator (a : T) : ∑' (i : T), q i * Set.indicator {a} (fun x => 1) i = q a := by + have Hfun : (fun (i : T) => q i * Set.indicator {a} (fun x => 1) i) = (fun (i : T) => if i = a then q a else 0) := by + funext i + rw [Set.indicator] + split <;> simp <;> split <;> simp_all + rw [Hfun] + exact tsum_ite_eq a (q a) + + -- Apply the converse lemma + have Hieq := Renyi_Jensen_strict_real (Renyi_Jensen_f p q) q α h HRJf_nonneg ?GLp Hq + case GLp => + -- ℒp bound (same as forward proof) + simp [Memℒp] + constructor + . apply MeasureTheory.StronglyMeasurable.aestronglyMeasurable + apply Measurable.stronglyMeasurable + apply Measurable.ennreal_toReal + conv => + right + intro x + rw [division_def] + apply Measurable.mul + . apply measurable_discrete + . apply Measurable.inv + apply measurable_discrete + · simp [snorm] + split + · simp + · rename_i Hα + simp [snorm'] + rw [MeasureTheory.lintegral_countable'] + rw [toReal_ofReal (le_of_lt (lt_trans zero_lt_one h))] + apply rpow_lt_top_of_nonneg + · simp + apply le_of_not_ge Hα + · conv => + enter [1, 1, a, 1, 1] + rw [<- Real.toNNReal_eq_nnnorm_of_nonneg (HRJf_nonneg a)] + rw [Renyi_Jensen_f] + rw [<- ENNReal.ofReal.eq_1] + rw [ENNReal.ofReal_toReal (HRJf_nt a)] + rfl + conv => + enter [1, 1, a, 2] + simp [toMeasure] + simp [PMF.toOuterMeasure] + rw [Hsum_indicator] + apply Hnts + cases Hieq + · rename_i Hk + exfalso + have CG1 (z : T) : q z = 0 → p z = 0 := by apply H + have CG2 (z : T) : ¬(p z ≠ 0 ∧ q z = ⊤) := by + simp + intro + apply PMF.apply_ne_top + conv at Hk => + enter [1, 1, 1, z] + rw [Renyi_Jensen_f] + rw [<- ENNReal.toReal_mul] + arg 1 + rw [division_def] + rw [mul_mul_inv_eq_mul_cancel (CG1 z) (CG2 z)] + clear CG1 + clear CG2 + + -- Convert the LHS of Hsumeq to the ℝ-valued summand, and then contradict + conv at Hsumeq => + enter [1, 1, 1, x] + rw [division_def] + rw [mul_assoc] + rw [ENNReal.inv_mul_cancel] + · skip + · apply Hq + · apply PMF.apply_ne_top + simp at * + rw [<- ENNReal.tsum_toReal_eq ?G1] at Hk + case G1 => + intro + apply PMF.apply_ne_top + simp at * + have Hone' : (1 : ENNReal).toReal = (1 : ℝ) := by simp + rw [<- Hone'] at Hk + rw [Hsumeq] at Hk + clear Hone' + rw [ENNReal.toReal_ofReal ?G1] at Hk + case G1 => + apply tsum_nonneg + intro i + apply mul_nonneg + · apply rpow_nonneg + apply HRJf_nonneg + · exact toReal_nonneg + linarith + · rename_i Hext + -- RHS of Hext is 1, LHS is p/q + apply PMF.ext + intro x + have Hext' := Hext x + rw [Renyi_Jensen_f] at Hext' + have CG1 (z : T) : q z = 0 → p z = 0 := by apply H + have CG2 (z : T) : ¬(p z ≠ 0 ∧ q z = ⊤) := by + simp + intro + apply PMF.apply_ne_top + conv at Hext' => + rhs + arg 1 + intro z + rw [Renyi_Jensen_f] + rw [<- ENNReal.toReal_mul] + arg 1 + rw [mul_comm] + rw [division_def] + rw [mul_mul_inv_eq_mul_cancel (CG1 z) (CG2 z)] + clear CG1 + clear CG2 + rw [<- ENNReal.tsum_toReal_eq] at Hext' + · rw [PMF.tsum_coe] at Hext' + apply (@ENNReal.mul_eq_mul_right _ _ ((q x)⁻¹) ?G1 ?G2).mp + case G1 => + simp + apply PMF.apply_ne_top + case G2 => + simp + apply Hq + rw [ENNReal.mul_inv_cancel ?G1 ?G2] + case G1 => apply Hq + case G2 => apply PMF.apply_ne_top + apply (toReal_eq_toReal_iff' (HRJf_nt x) ?G3).mp + case G3 => simp + apply Hext' + · intro + apply PMF.apply_ne_top + + · -- Special case: There exists some element x0 with p x0 = ⊤ but q x0 ∈ ℝ+ + -- This means the sum in Hnts will actually be ⊤ + rename_i Hspecial + exfalso + apply Hnts + apply ENNReal.tsum_eq_top_of_eq_top + simp at Hspecial + rcases Hspecial with ⟨ x , ⟨ Hx1, ⟨ Hx2 , Hx3 ⟩ ⟩ ⟩ + exists x + apply mul_eq_top.mpr + right + apply And.intro + · apply rpow_eq_top_iff.mpr + right + apply And.intro + · apply div_eq_top.mpr + right + apply And.intro Hx1 Hx3 + · linarith + · apply Hx2 + · -- One of the series is Top, so the other series is too + rename_i Hlhs_top + simp at Hlhs_top + rw [Hlhs_top] at Hsumeq + -- This series should actually be 1 by PMF + conv at Hsumeq => + lhs + arg 1 + arg 1 + intro x + rw [PMF_mul_mul_inv_eq_mul_cancel p q H] + conv at Hsumeq => + lhs + arg 1 + rw [PMF.tsum_coe] + simp at Hsumeq + +/-- +Restriction of the PMF f to the support of q. +-/ +def reducedPMF_def (f q : PMF T) (x : { t : T // ¬q t = 0 }) : ENNReal := f x.val + +/-- +Restricted PMF has sum 1 +-/ +lemma reducedPMF_norm_acts (p q : PMF T) (H : AbsCts p q) : HasSum (reducedPMF_def p q) 1 := by + have H1 : Summable (reducedPMF_def p q) := by exact ENNReal.summable + have H2 := Summable.hasSum H1 + have H3 : (∑' (b : { t // q t ≠ 0 }), reducedPMF_def p q b) = 1 := by + have K1 : Function.support (fun x => p x) ⊆ { t : T | q t ≠ 0 } := by + rw [Function.support] + simp + intro a Hp Hcont + rw [AbsCts] at H + apply Hp + apply H + apply Hcont + have S1 : ∑' (x : ↑{t | q t ≠ 0}), p ↑x = ∑' (x : T), p x := by + apply tsum_subtype_eq_of_support_subset K1 + have T1 : ∑' (x : T), p x = 1 := by exact tsum_coe p + rw [<- T1] + rw [<- S1] + simp + rfl + rw [<- H3] + apply H2 + +/-- +Restriction of the PMF f to the support of q +-/ +noncomputable def reducedPMF {p q : PMF T} (H : AbsCts p q): PMF { t : T // ¬q t = 0 } := + ⟨ reducedPMF_def p q, reducedPMF_norm_acts p q H ⟩ + +/-- +`reducedPMF` is nonzero everywhere +-/ +lemma reducedPMF_pos {q : PMF T} (H : AbsCts q q) (a : T) (Ha : ¬q a = 0): (reducedPMF H) ⟨a, Ha⟩ ≠ 0 := by + simp + rw [reducedPMF] + unfold reducedPMF_def + rw [DFunLike.coe] + rw [PMF.instFunLike] + simp + apply Ha + +/-- +Jensen's inquality for the Renyi divergence sum between absolutely continuous PMFs +-/ +theorem Renyi_Jensen_ENNReal [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T] (p q : PMF T) {α : ℝ} (h : 1 < α) (Hac : AbsCts p q) : + (∑' x : T, (p x / q x) * q x) ^ α ≤ (∑' x : T, (p x / q x) ^ α * q x) := by + + have K1 : Function.support (fun x : T => (p x / q x) * q x) ⊆ { t : T | q t ≠ 0 } := by simp [Function.support] + have K2 : Function.support (fun x : T => (p x / q x)^α * q x) ⊆ { t : T | q t ≠ 0 } := by simp [Function.support] + rw [<- tsum_subtype_eq_of_support_subset K1] + rw [<- tsum_subtype_eq_of_support_subset K2] + simp + + have Hq : AbsCts q q := AbsCts_refl q + + have B1 (x : { x // ¬q x = 0 }) : p ↑x / q ↑x * q ↑x = reducedPMF Hac x / reducedPMF Hq x * reducedPMF Hq x := by congr + have B2 (x : { x // ¬q x = 0 }) : (p ↑x / q ↑x)^α * q ↑x = (reducedPMF Hac x / reducedPMF Hq x)^α * reducedPMF Hq x := by congr + conv => + congr + · enter [1, 1, x] + rw [B1 x] + · arg 1 + intro x + rw [B2 x] + + clear B1 + clear B2 + clear K1 + clear K2 + + apply Renyi_Jensen_ENNReal_reduct + · apply h + · rw [AbsCts] + simp + intro a Ha Hcont + exfalso + apply (reducedPMF_pos Hq a Ha Hcont) + · intro t + rcases t with ⟨ a , Ha ⟩ + apply (reducedPMF_pos Hq a Ha) + +/-- +Converse of Jensen's inquality for the Renyi divergence sum between absolutely continuous PMFs +-/ +lemma Renyi_Jensen_ENNReal_converse [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T] + (p q : PMF T) {α : ℝ} (h : 1 < α) (H : AbsCts p q) + (Hsumeq : (∑' x : T, (p x / q x) * q x) ^ α = (∑' x : T, (p x / q x) ^ α * q x)) : + (p = q) := by + + have K1 : Function.support (fun x : T => (p x / q x) * q x) ⊆ { t : T | q t ≠ 0 } := by simp [Function.support] + have K2 : Function.support (fun x : T => (p x / q x)^α * q x) ⊆ { t : T | q t ≠ 0 } := by simp [Function.support] + rw [<- tsum_subtype_eq_of_support_subset K1] at Hsumeq + rw [<- tsum_subtype_eq_of_support_subset K2] at Hsumeq + simp at Hsumeq + + have Hq : AbsCts q q := AbsCts_refl q + + have B1 (x : { x // ¬q x = 0 }) : p ↑x / q ↑x * q ↑x = reducedPMF H x / reducedPMF Hq x * reducedPMF Hq x := by congr + have B2 (x : { x // ¬q x = 0 }) : (p ↑x / q ↑x)^α * q ↑x = (reducedPMF H x / reducedPMF Hq x)^α * reducedPMF Hq x := by congr + + conv at Hsumeq => + congr + · arg 1 + arg 1 + intro x + rw [B1 x] + · arg 1 + intro x + rw [B2 x] + + clear B1 + clear B2 + clear K1 + clear K2 + + have Hreduced : (reducedPMF H = reducedPMF Hq) := by + apply (Renyi_Jensen_ENNReal_converse_reduct (reducedPMF H) (reducedPMF Hq) h) + · intro t Ht + exfalso + rcases t with ⟨ a , Ha ⟩ + apply (reducedPMF_pos Hq a Ha) + apply Ht + · intro t + rcases t with ⟨ a , Ha ⟩ + apply (reducedPMF_pos Hq a Ha) + · apply Hsumeq + + apply PMF.ext + intro x + cases (Classical.em (q x = 0)) + · rename_i Hqz + rw [Hqz] + apply H + apply Hqz + · rename_i Hqnz + have Hreduced' : reducedPMF H ⟨ x , Hqnz ⟩ = reducedPMF Hq ⟨ x , Hqnz ⟩ := by + exact congrFun (congrArg DFunLike.coe Hreduced) ⟨ x , Hqnz ⟩ + repeat rw [DFunLike.coe] at Hreduced' + repeat rw [PMF.instFunLike] at Hreduced' + repeat rw [reducedPMF] at Hreduced' + unfold reducedPMF_def at Hreduced' + simp at Hreduced' + assumption + +/-- +The ``EReal``-valued Renyi divergence is nonnegative. + +Use this lemma to perform rewrites through the ``ENNReal.ofEReal`` in the +``ENNReal``-valued ``RenyiDivergence`` +-/ +theorem RenyiDivergence_def_nonneg [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T] (p q : PMF T) (Hpq : AbsCts p q) {α : ℝ} (Hα : 1 < α) : + (0 ≤ RenyiDivergence_def p q α) := by + have H1 : eexp (((α - 1)) * 0) ≤ eexp ((α - 1) * RenyiDivergence_def p q α) := by + rw [RenyiDivergence_def_exp p q Hα] + rw [RenyiDivergenceExpectation p q Hα Hpq] + simp + apply (le_trans ?G1 (Renyi_Jensen_ENNReal p q Hα Hpq)) + have Hone : (∑' (x : T), p x / q x * q x) = 1 := by + conv => + arg 1 + arg 1 + intro x + rw [PMF_mul_mul_inv_eq_mul_cancel p q Hpq] + exact tsum_coe p + have Hle : (∑' (x : T), p x / q x * q x) ≤ (∑' (x : T), p x / q x * q x) ^ α := by + apply ENNReal.le_rpow_self_of_one_le + · rw [Hone] + · linarith + apply le_trans ?X Hle + rw [Hone] + apply eexp_mono_le.mpr at H1 + have Hone : (OfNat.ofNat 1 = Real.toEReal (1 : ℝ)) := by simp + have Hzero : (OfNat.ofNat 0 = Real.toEReal (0 : ℝ)) := by simp + + apply ereal_smul_le_left (α.toEReal - OfNat.ofNat 1) + · rw [Hone] + rw [<- EReal.coe_sub] + rw [Hzero] + apply EReal.coe_lt_coe_iff.mpr + exact sub_pos.mpr Hα + · rw [Hone] + rw [<- EReal.coe_sub] + exact EReal.coe_lt_top (α - OfNat.ofNat 1) + · assumption + +/-- +Renyi divergence between identical distributions is zero +-/ +lemma RenyiDivergence_refl_zero (p : PMF T) {α : ℝ} (Hα : 1 < α) : (0 = RenyiDivergence_def p p α) := by + have H1 : 1 = eexp ((α - 1) * RenyiDivergence_def p p α) := by + rw [RenyiDivergence_def_exp p p Hα] + rw [RenyiDivergenceExpectation p p Hα (AbsCts_refl p)] + have HRW (x : T) : ((p.val x) / (p.val x)) ^α * p.val x = p.val x := by + cases (Classical.em (p x = 0)) + · rename_i Hz + simp [DFunLike.coe] at Hz + simp [Hz] + · rename_i Hnz + rw [((@div_eq_one_iff (p.val x) (p.val x) ?GNZ) ?GNT).mpr rfl] + case GNZ => + simp [DFunLike.coe] at Hnz + simp + apply Hnz + case GNT => + have HltTop := PMF.apply_lt_top p x + apply LT.lt.ne_top HltTop + simp + conv => + rhs + arg 1 + intro x + simp [DFunLike.coe] + rw [HRW] + rcases p with ⟨ p' , Hp' ⟩ + exact Eq.symm (HasSum.tsum_eq Hp') + + have Hone : (OfNat.ofNat 1 = Real.toEReal (1 : ℝ)) := by simp + have Hzero : (OfNat.ofNat 0 = Real.toEReal (0 : ℝ)) := by simp + apply ereal_smul_eq_left (α.toEReal - OfNat.ofNat 1) + · rw [Hone] + rw [<- EReal.coe_sub] + rw [Hzero] + apply EReal.coe_lt_coe_iff.mpr + exact sub_pos.mpr Hα + · rw [Hone] + rw [<- EReal.coe_sub] + exact EReal.coe_lt_top (α - OfNat.ofNat 1) + apply eexp_injective + rw [<- H1] + simp + +/-- +Renyi divergence is zero if and only if the distributions are equal +-/ +theorem RenyiDivergence_def_eq_0_iff [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T] + (p q : PMF T) {α : ℝ} (Hα : 1 < α) (Hcts : AbsCts p q) : + (RenyiDivergence_def p q α = 0) <-> (p = q) := by + apply Iff.intro + · intro Hrdeq + apply Renyi_Jensen_ENNReal_converse + · apply Hα + · apply Hcts + · have H1 : eexp (((α - 1)) * 0) = eexp ((α - 1) * RenyiDivergence_def p q α) := by rw [Hrdeq] + simp at H1 + rw [RenyiDivergence_def_exp p q Hα] at H1 + rw [RenyiDivergenceExpectation p q Hα Hcts] at H1 + rw [<- H1] + clear H1 + have CG1 (x : T) : DFunLike.coe q x = OfNat.ofNat 0 → DFunLike.coe p x = OfNat.ofNat 0 := by apply Hcts + have CG2 (x : T) : ¬(DFunLike.coe p x ≠ OfNat.ofNat 0 ∧ DFunLike.coe q x = ⊤) := by + simp + intro + apply PMF.apply_ne_top + conv => + lhs + arg 1 + arg 1 + intro x + rw [division_def] + rw [mul_mul_inv_eq_mul_cancel (CG1 x) (CG2 x)] + simp + · intro Hpq + rw [Hpq] + symm + apply RenyiDivergence_refl_zero + apply Hα + +/-- +The logarithm in the definition of the Renyi divergence is nonnegative. +-/ +lemma RenyiDivergence_def_log_sum_nonneg [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T] + (p q : PMF T) (Hac : AbsCts p q) {α : ℝ} (Hα : 1 < α ): (0 ≤ (elog (∑' x : T, (p x)^α * (q x)^(1 - α)))) := by + have Hrd := RenyiDivergence_def_nonneg p q Hac Hα + rw [RenyiDivergence_def] at Hrd + apply ofEReal_nonneg_scal_l at Hrd + · assumption + · apply inv_pos_of_pos + linarith + +/-- +The ``ENNReal``-valued Renyi divergence between PMF's. +-/ +noncomputable def RenyiDivergence (p q : PMF T) (α : ℝ) : ENNReal := + ENNReal.ofEReal (RenyiDivergence_def p q α) + + +/-- +The Renyi divergence between absolutely continuous distributions is zero if and only if the +distributions are equal. +-/ +theorem RenyiDivergence_aux_zero [MeasurableSpace T] [MeasurableSingletonClass T] [Countable T] + (p q : PMF T) {α : ℝ} (Hα : 1 < α) (Hac : AbsCts p q) : p = q <-> RenyiDivergence p q α = 0 := by + apply Iff.intro + · intro Heq + rw [Heq] + rw [RenyiDivergence] + rw [<- RenyiDivergence_refl_zero _ Hα] + simp + · intro H + apply (RenyiDivergence_def_eq_0_iff p q Hα Hac).mp + symm + rw [RenyiDivergence] at H + have H' := RenyiDivergence_def_nonneg p q Hac Hα + refine (ofEReal_nonneg_inj ?mpr.Hw H').mpr ?mpr.a + · simp + simp [H] \ No newline at end of file diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean new file mode 100644 index 00000000..b19c7272 --- /dev/null +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean @@ -0,0 +1,597 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jean-Baptiste Tristan +-/ +import SampCert.DifferentialPrivacy.Abstract +import SampCert.DifferentialPrivacy.ZeroConcentrated.DP + +/-! +# zCDP Adaptive Composition + +This file builds up to a zCDP bound on adaptively composed zCDP queries. +-/ + +noncomputable section + +open Classical Nat Int Real ENNReal MeasureTheory Measure + +namespace SLang + +variable { T U V : Type } +variable [HU : Inhabited U] +variable [HV : Inhabited V] + + +lemma exp_non_top : ∀ (z : ENNReal) (β : ℝ), z ≠ 0 -> z ≠ ⊤ -> z ^ β ≠ ⊤ := by + intro z β Hz0 HzT + intro W + have h : z = 0 ∧ β < 0 ∨ z = ⊤ ∧ 0 < β := by + apply rpow_eq_top_iff.mp + apply W + cases h + · simp_all only [ne_eq, not_true_eq_false] + · simp_all only [ne_eq, top_ne_zero, not_false_eq_true, not_true_eq_false] + +lemma rpow_ne_zero_iff (x : ENNReal) (y : ℝ): (¬x = 0 ∨ ¬ 0 < y) ∧ (¬ x = ⊤ ∨ ¬ y < 0) -> x ^ y ≠ 0 := by + have _ := (@ENNReal.rpow_eq_zero_iff x y) + aesop + +lemma ne_top_lt_top (x : ENNReal) : (x ≠ ⊤) -> (x < ⊤) := by + exact fun a => Ne.lt_top' (id (Ne.symm a)) + +lemma lt_top_ne_top (x : ENNReal) : (x < ⊤) -> ¬ (x = ⊤) := by + exact fun a => LT.lt.ne_top a + + +/-- +``b`` is an upper bound on the Renyi divergence for particular neighbours, uniform across all values of the first query. +-/ +def RDBound (nq2 : U -> List T -> SLang V) (α : ℝ) (l₁ l₂ : List T) (b : ℝ) : Prop := + ∀ u, RenyiDivergence (nq2 u l₁) (nq2 u l₂) α ≤ b + +/-- +There exsts an upper bound on the Renyi divergence, uniform across all values of the first query. +-/ +def RDBounded (nq2 : U -> List T -> SLang V) : Prop := + ∀ α l₁ l₂, (1 < α) -> (Neighbour l₁ l₂) -> ∃ (b : ℝ), RDBound nq2 α l₁ l₂ b + +/-- +``b`` is an upper bound on the Renyi divergence, uniform across all values of the first query. +-/ +def URDBound (nq2 : U -> List T -> SLang V) (b : ℝ -> List T -> List T -> ℝ) : Prop := + ∀ α l₁ l₂, (1 < α) -> (Neighbour l₁ l₂) -> RDBound nq2 α l₁ l₂ (b α l₁ l₂) + +lemma RDBounded_of_URDBound (nq2 : U -> List T -> SLang V) (b : ℝ -> List T -> List T -> ℝ) : URDBound nq2 b -> RDBounded nq2 := by + rw [URDBound, RDBounded] + aesop + + +-- lemma URDBound_of_sup (nq2 : U -> List T -> SLang V) : URDBound nq2 (fun α l₁ l₂ => ⨆ u, RenyiDivergence (nq2 u l₁) (nq2 u l₂) α) := by +-- -- Is this provable? +-- -- I think only if the supremum exists, since we're working in ℝ instead of ENNReal +-- sorry + +/-- +Equation for the Renyi divergence series in terms of the Renyi Divergence +-/ +lemma RenyiDivergence_exp (p q : SLang T) {α : ℝ} + (h : 1 < α) + (H1 : 0 < ∑' (x : T), p x ^ α * q x ^ (1 - α)) + (H2 : ∑' (x : T), p x ^ α * q x ^ (1 - α) < ⊤) : + Real.exp ((α - 1) * RenyiDivergence p q α) = (∑' x : T, (p x)^α * (q x)^(1 - α)).toReal := by + simp only [RenyiDivergence] + rw [<- mul_assoc] + have test : (α - 1) * (α - 1)⁻¹ = 1 := by + refine mul_inv_cancel ?h + linarith + rw [test] + clear test + simp + rw [Real.exp_log] + apply ENNReal.toReal_pos_iff.mpr + tauto + + +/-- +Adaptive composed query distribution is nowhere zero +-/ +theorem privComposeAdaptive_NonZeroNQ {nq1 : List T → SLang U} {nq2 : U -> List T → SLang V} + (nt1 : NonZeroNQ nq1) (nt2 : ∀ u, NonZeroNQ (nq2 u)) : + NonZeroNQ (privComposeAdaptive nq1 nq2) := by + simp [NonZeroNQ] at * + simp [privComposeAdaptive] + tauto + + +/-- +All outputs of a adaptive composed query have finite probability. +-/ +theorem privComposeAdaptive_NonTopNQ {nq1 : List T → SLang U} {nq2 : U -> List T → SLang V} + (nt1 : NonTopNQ nq1) (nt2 : ∀ u, NonTopNQ (nq2 u)) : + NonTopNQ (privComposeAdaptive nq1 nq2) := by + simp [NonTopNQ] at * + intros l u v + rw [privComposeChainRule] + apply ENNReal.mul_ne_top <;> + simp_all only [ne_eq, not_false_eq_true] + +/-- +Adaptive composed query is a proper distribution +-/ +theorem privComposeAdaptive_NonTopSum {nq1 : List T → SLang U} {nq2 : U -> List T → SLang V} + (nt1 : NonTopSum nq1) + (Hubound : ∃ (z : ℝ), ∀ (u : U), ∀ l, ∑'(v : V), nq2 u l v ≤ ENNReal.ofReal z) : + NonTopSum (privComposeAdaptive nq1 nq2) := by + simp [NonTopSum] at * + intro l + simp [privComposeAdaptive] + rw [ENNReal.tsum_prod'] + conv => + right + left + right + intro a + right + intro b + simp + rw [(compose_sum_rw_adaptive _ _ a b)] + conv => + right + left + right + intro a + rw [ENNReal.tsum_mul_left] + + rcases Hubound with ⟨ z , Hubound ⟩ + apply lt_top_ne_top + apply (@LE.le.trans_lt _ _ _ (∑' (a : U), nq1 l a * ENNReal.ofReal z) _ ?goal1) + case goal1 => + apply ENNReal.tsum_le_tsum + intro a + apply mul_le_mul_of_nonneg_left + · simp_all + · simp_all only [_root_.zero_le] + rw [ENNReal.tsum_mul_right] + apply ne_top_lt_top + intro Hcont + rw [mul_eq_top] at Hcont + cases Hcont + · rename_i h + rcases h with ⟨ _ , h1 ⟩ + simp_all only [le_top, implies_true, ne_eq, ENNReal.tsum_eq_zero, not_forall, ofReal_ne_top] + · rename_i h + rcases h with ⟨ h0 , _ ⟩ + simp_all only + +/-- +Renyi divergence beteeen adaptive composed queries on neighbours are finite. +-/ +theorem privComposeAdaptive_NonTopRDNQ {nq1 : List T → SLang U} {nq2 : U -> List T → SLang V} + (nt1 : NonTopRDNQ nq1) (nt2 : ∀ u, NonTopRDNQ (nq2 u)) (nn1 : NonTopNQ nq1) (nn2 : ∀ u, NonTopNQ (nq2 u)) (nz1 : NonZeroNQ nq1) (nz2 : ∀ u, NonZeroNQ (nq2 u)) + (Hubound : RDBounded nq2) : + NonTopRDNQ (privComposeAdaptive nq1 nq2) := by + rw [NonTopRDNQ] at * + intro α h1 l₁ l₂ h2 + simp [privComposeAdaptive] + rw [ENNReal.tsum_prod'] + simp + conv => + right + left + right + intro x + right + intro y + congr + . left + rw [(compose_sum_rw_adaptive _ _ x y)] + . left + rw [(compose_sum_rw_adaptive _ _ x y)] + conv => + right + left + right + intro x + right + intro y + rw [ENNReal.mul_rpow_of_nonneg _ _ (le_of_lt (lt_trans zero_lt_one h1))] + rw [ENNReal.mul_rpow_of_ne_top (nn1 l₂ x) (nn2 x l₂ y)] + rw [mul_assoc] + right + rw [mul_comm] + rw [mul_assoc] + right + rw [mul_comm] + conv => + right + left + right + intro x + right + intro y + rw [← mul_assoc] + conv => + right + left + right + intro x + rw [ENNReal.tsum_mul_left] + + rcases (Hubound α l₁ l₂ h1 h2) with ⟨ b , Hubound ⟩ + + apply lt_top_ne_top + apply (@LE.le.trans_lt _ _ _ (∑' (x : U), nq1 l₁ x ^ α * nq1 l₂ x ^ (1 - α) * ENNReal.ofReal (rexp ((α - 1) * b))) _ ?goal1) + + case goal1 => + apply ENNReal.tsum_le_tsum + intro a + refine (ENNReal.mul_le_mul_left ?h.h0 ?h.hinf).mpr ?h.a + · apply mul_ne_zero_iff.mpr + apply And.intro + · refine rpow_ne_zero_iff (nq1 l₁ a) α ?h.h0.left.a + apply And.intro + · left + aesop + · left + aesop + · refine rpow_ne_zero_iff (nq1 l₂ a) (1 - α) ?h.h0.right.a + apply And.intro + · left + aesop + · left + aesop + · intro H + rw [mul_eq_top] at H + cases H + · rename_i Hk + rcases Hk with ⟨ hk1, hk2 ⟩ + have Hcont : nq1 l₂ a ^ (1-α) ≠ ⊤ := by + apply exp_non_top + · aesop + · aesop + aesop + · rename_i Hk + rcases Hk with ⟨ hk1, hk2 ⟩ + have Hcont : nq1 l₁ a ^ (α) ≠ ⊤ := by + apply exp_non_top + · aesop + · apply nn1 + aesop + · refine ((ENNReal.toReal_le_toReal ?g1 ?g2).mp ?g3) + case g1 => exact nt2 a α h1 l₁ l₂ h2 + case g2 => exact Ne.symm top_ne_ofReal + case g3 => + + have GH1 : ∀ i, 0 < ∑' (x : V), nq2 i l₁ x ^ α * nq2 i l₂ x ^ (1 - α) := by + intro i + rcases HV with ⟨ v0 ⟩ + have Hle : nq2 i l₁ v0 ^ α * nq2 i l₂ v0 ^ (1 - α) <= ∑' (x : V), nq2 i l₁ x ^ α * nq2 i l₂ x ^ (1 - α) := by apply ENNReal.le_tsum v0 + apply (LE.le.trans_lt' Hle) + clear Hle + apply ENNReal.mul_pos + · have Hlt : (0 < nq2 i l₁ v0 ^ α) := by + apply ENNReal.rpow_pos + · have H1 : 0 <= nq2 i l₁ v0 := by simp + have H2 : 0 ≠ nq2 i l₁ v0 := by + exact fun a => nz2 i l₁ v0 (id (Eq.symm a)) + apply LE.le.lt_or_eq at H1 + cases H1 + · assumption + · contradiction + · exact nn2 i l₁ v0 + intro Hk + rw [Hk] at Hlt + apply (lt_self_iff_false 0).mp Hlt + · intro Hk + have Hlt : (0 < nq2 i l₂ v0 ^ (1 - α)) := by + apply ENNReal.rpow_pos + · have H1 : 0 <= nq2 i l₂ v0 := by simp + have H2 : 0 ≠ nq2 i l₂ v0 := by exact fun a => nz2 i l₂ v0 (id (Eq.symm a)) + apply LE.le.lt_or_eq at H1 + cases H1 + · assumption + · contradiction + · exact nn2 i l₂ v0 + rw [Hk] at Hlt + apply (lt_self_iff_false 0).mp Hlt + + have GH2 : ∀ i, ∑' (x : V), nq2 i l₁ x ^ α * nq2 i l₂ x ^ (1 - α) < ⊤ := by + exact fun i => ne_top_lt_top (∑' (x : V), nq2 i l₁ x ^ α * nq2 i l₂ x ^ (1 - α)) (nt2 i α h1 l₁ l₂ h2) + + rw [<- RenyiDivergence_exp (nq2 a l₁) (nq2 a l₂) h1 ?H1 ?H2] + case H1 => apply GH1 + case H2 => apply GH2 + rw [ENNReal.toReal_ofReal] + · apply Real.exp_le_exp_of_le + rw [RDBound] at Hubound + apply mul_le_mul_of_nonneg_left + · apply Hubound + · linarith + · apply (exp_nonneg ((α - 1) * b)) + + rw [ENNReal.tsum_mul_right] + apply ne_top_lt_top + intro H + rw [mul_eq_top] at H + cases H + . rename_i h3 + rcases h3 with ⟨ _ , h31 ⟩ + aesop + . rename_i h3 + rcases h3 with ⟨ h30, _ ⟩ + aesop + + +/-- +Bound on Renyi divergence on adaptively composed queries +-/ +lemma privComposeAdaptive_renyi_bound {nq1 : List T → SLang U} {nq2 : U -> List T → SLang V} (α : ℝ) (Hα : 1 < α) (l₁ l₂ : List T) + (HNT1 : NonTopNQ nq1) (HNTRDNQ1 : NonTopRDNQ nq1) (HNTRDNQ2 : ∀ u, NonTopRDNQ (nq2 u)) + (HN : Neighbour l₁ l₂) (HNZ1 : NonZeroNQ nq1) (HNZ2 : ∀ u, NonZeroNQ (nq2 u)) (HNT2 : ∀ u, NonTopNQ (nq2 u)) + (b : ℝ) + (Hubound : RDBound nq2 α l₁ l₂ b) + (Hubound2 : RDBounded nq2) : + RenyiDivergence (privComposeAdaptive nq1 nq2 l₁) (privComposeAdaptive nq1 nq2 l₂) α ≤ + RenyiDivergence (nq1 l₁) (nq1 l₂) α + b := by + apply (RenyiDivergence_mono_sum _ _ α Hα) + rw [RenyiDivergence_exp (privComposeAdaptive nq1 nq2 l₁) (privComposeAdaptive nq1 nq2 l₂) Hα ?H1 ?H2] + case H1 => + rcases HV with ⟨ v0 ⟩ + rcases HU with ⟨ u0 ⟩ + have Hle : (privComposeAdaptive nq1 nq2 l₁ (u0, v0) ^ α * privComposeAdaptive nq1 nq2 l₂ (u0, v0) ^ (1 - α)) ≤ (∑' (x : U × V), privComposeAdaptive nq1 nq2 l₁ x ^ α * privComposeAdaptive nq1 nq2 l₂ x ^ (1 - α)) := by + exact ENNReal.le_tsum (u0, v0) + apply (LE.le.trans_lt' Hle) + clear Hle + apply ENNReal.mul_pos + · apply rpow_ne_zero_iff + apply And.intro + · left + apply privComposeAdaptive_NonZeroNQ <;> aesop + · left + apply privComposeAdaptive_NonTopNQ <;> aesop + · apply rpow_ne_zero_iff + apply And.intro + · left + apply privComposeAdaptive_NonZeroNQ <;> aesop + · left + apply privComposeAdaptive_NonTopNQ <;> aesop + case H2 => + apply ne_top_lt_top + apply privComposeAdaptive_NonTopRDNQ <;> aesop + + rw [left_distrib] + rw [Real.exp_add] + + rw [RenyiDivergence_exp (nq1 l₁) (nq1 l₂) Hα ?H1 ?H2] + case H1 => + rcases HU with ⟨ u0 ⟩ + have Hle : nq1 l₁ u0 ^ α * nq1 l₂ u0 ^ (1 - α) <= ∑' (x : U), nq1 l₁ x ^ α * nq1 l₂ x ^ (1 - α) := ENNReal.le_tsum u0 + apply (LE.le.trans_lt' Hle) + clear Hle + apply ENNReal.mul_pos + · apply rpow_ne_zero_iff + apply And.intro + · left + apply HNZ1 + · left + apply HNT1 + · apply rpow_ne_zero_iff + apply And.intro + · left + apply HNZ1 + · left + apply HNT1 + case H2 => + apply ne_top_lt_top + apply HNTRDNQ1 <;> aesop + + have hexp_b : ∀ u, (rexp ((α - 1) * RenyiDivergence (nq2 u l₁) (nq2 u l₂) α) <= rexp ((α - 1) * b)) := by + rw [RDBound] at Hubound + intro u + let _ := (Hubound u) + apply Real.exp_le_exp_of_le + aesop + rw [mul_comm] + rw [<- (ENNReal.toReal_ofReal_mul _ _ ?h1)] + case h1 => + exact exp_nonneg ((α - 1) * b) + rw [mul_comm] + rw [← ENNReal.tsum_mul_right] + apply (toReal_mono' _ ?goal2) + case goal2 => + intro H + exfalso + rw [ENNReal.tsum_mul_right] at H + rw [mul_eq_top] at H + cases H + · rename_i h + rcases h with ⟨ _ , h1 ⟩ + apply (@ENNReal.top_ne_ofReal (rexp ((α - 1) * b))) + aesop + · rename_i h + rcases h with ⟨ h0 , _ ⟩ + apply (HNTRDNQ1 α Hα l₁ l₂ HN) + apply h0 + + apply (@LE.le.trans _ _ _ ((∑' (i : U), nq1 l₁ i ^ α * nq1 l₂ i ^ (1 - α) * ENNReal.ofReal (rexp ((α - 1) * RenyiDivergence (nq2 i l₁) (nq2 i l₂) α)))) _ _ ?goal2) + case goal2 => + apply (tsum_le_tsum _ ENNReal.summable ENNReal.summable) + intro i + refine (ENNReal.mul_le_mul_left ?h.h.h0 ?h.h.hinf).mpr ?h.h.a + · apply mul_ne_zero_iff.mpr + apply And.intro + · apply rpow_ne_zero_iff + apply And.intro + · left + apply HNZ1 + · left + apply HNT1 + · apply rpow_ne_zero_iff + apply And.intro + · left + apply HNZ1 + · left + apply HNT1 + · apply ENNReal.mul_ne_top + · apply exp_non_top + · apply HNZ1 + · apply HNT1 + · apply exp_non_top + · apply HNZ1 + · apply HNT1 + · apply ENNReal.ofReal_le_ofReal + apply hexp_b + + have GH1 : ∀ i, 0 < ∑' (x : V), nq2 i l₁ x ^ α * nq2 i l₂ x ^ (1 - α) := by + intro i + rcases HV with ⟨ v0 ⟩ + have Hle : nq2 i l₁ v0 ^ α * nq2 i l₂ v0 ^ (1 - α) <= ∑' (x : V), nq2 i l₁ x ^ α * nq2 i l₂ x ^ (1 - α) := ENNReal.le_tsum v0 + apply (LE.le.trans_lt' Hle) + clear Hle + apply ENNReal.mul_pos + · have Hlt : (0 < nq2 i l₁ v0 ^ α) := by + apply ENNReal.rpow_pos + · exact pos_iff_ne_zero.mpr (HNZ2 i l₁ v0) + · apply HNT2 + intro Hk + simp_all only [exp_le_exp, gt_iff_lt, sub_pos, _root_.mul_le_mul_left, lt_self_iff_false] + · have Hlt : (0 < nq2 i l₂ v0 ^ (1 - α)) := by + apply ENNReal.rpow_pos + · exact pos_iff_ne_zero.mpr (HNZ2 i l₂ v0) + · exact HNT2 i l₂ v0 + intro Hk + simp_all only [exp_le_exp, gt_iff_lt, sub_pos, _root_.mul_le_mul_left, lt_self_iff_false] + + have GH2 : ∀ i, ∑' (x : V), nq2 i l₁ x ^ α * nq2 i l₂ x ^ (1 - α) < ⊤ := by + exact fun i => ne_top_lt_top (∑' (x : V), nq2 i l₁ x ^ α * nq2 i l₂ x ^ (1 - α)) (HNTRDNQ2 i α Hα l₁ l₂ HN) + + -- After this point the argument is tight + apply Eq.le + conv => + rhs + congr + intro i + rw [RenyiDivergence_exp (nq2 i l₁) (nq2 i l₂) Hα] + rfl + · apply GH1 + · apply GH2 + + conv => + lhs + congr + intro + rw [privComposeChainRule] + rw [privComposeChainRule] + + conv => + rhs + congr + intro x + rw [<- (@ENNReal.ofReal_toReal (nq1 l₁ x ^ α * nq1 l₂ x ^ (1 - α)) ?goal2)] + · rw [<- ENNReal.ofReal_mul] + · rw [<- ENNReal.toReal_mul] + rw [(@ENNReal.ofReal_toReal (nq1 l₁ x ^ α * nq1 l₂ x ^ (1 - α) * ∑' (x_1 : V), nq2 x l₁ x_1 ^ α * nq2 x l₂ x_1 ^ (1 - α)) ?goal4)] + rfl + apply ENNReal.mul_ne_top + · apply ENNReal.mul_ne_top + · apply exp_non_top + · apply HNZ1 + · apply HNT1 + · apply exp_non_top + · apply HNZ1 + · apply HNT1 + · apply HNTRDNQ2 + apply Hα + apply HN + · apply ENNReal.toReal_nonneg + · apply ENNReal.mul_ne_top + · apply exp_non_top + · apply HNZ1 + · apply HNT1 + · apply exp_non_top + · apply HNZ1 + · apply HNT1 + + conv => + rhs + arg 1 + intro x + rw [<- ENNReal.tsum_mul_left] + + rw [<- ENNReal.tsum_prod] + congr + apply funext + intro p + rcases p with ⟨ u , v ⟩ + simp + rw [ENNReal.mul_rpow_of_nonneg _ _ ?sc1] + case sc1 => linarith + rw [mul_rpow_of_ne_zero] + · exact mul_mul_mul_comm (nq1 l₁ u ^ α) (nq2 u l₁ v ^ α) (nq1 l₂ u ^ (1 - α)) (nq2 u l₂ v ^ (1 - α)) + · apply HNZ1 + · apply HNZ2 + +/-- +Adaptively Composed queries satisfy zCDP Renyi divergence bound. +-/ +theorem privComposeAdaptive_zCDPBound {nq1 : List T → SLang U} {nq2 : U -> List T → SLang V} {ε₁ ε₂ ε₃ ε₄ : ℕ+} + (h1 : zCDPBound nq1 ((ε₁ : ℝ) / ε₂)) + (h2 : ∀ u, zCDPBound (nq2 u) ((ε₃ : ℝ) / ε₄)) + (nn1 : NonZeroNQ nq1) + (nn2 : ∀ u, NonZeroNQ (nq2 u)) + (nt1 : NonTopRDNQ nq1) + (nt2 : ∀ u, NonTopRDNQ (nq2 u)) (nts1 : NonTopNQ nq1) (nts2 : ∀ u, NonTopNQ (nq2 u)) + (HB : RDBounded nq2) + (HB' : URDBound nq2 (fun α l₁ l₂ => ⨆ u, RenyiDivergence (nq2 u l₁) (nq2 u l₂) α)) : + zCDPBound (privComposeAdaptive nq1 nq2) (((ε₁ : ℝ) / ε₂) + ((ε₃ : ℝ) / ε₄)) := by + rw [zCDPBound] + intro α Hα l₁ l₂ Hneighbours + -- Loose step + apply (@LE.le.trans _ _ _ (1/2 * (↑↑ε₁ / ↑↑ε₂)^2 * α + 1/2 * (↑↑ε₃ / ↑↑ε₄)^2 * α) _ _ ?case_sq) + case case_sq => + -- Binomial bound + rw [add_sq] + rw [<- right_distrib] + apply (mul_le_mul_of_nonneg_right _ ?goal1) + case goal1 => linarith + rw [<- left_distrib] + apply (mul_le_mul_of_nonneg_left _ ?goal1) + case goal1 => linarith + apply add_le_add_right + have hrw : (↑↑ε₁ / ↑↑ε₂ : ℝ) ^ 2 = (↑↑ε₁ / ↑↑ε₂) ^ 2 + 0 := by linarith + conv => + lhs + rw [hrw] + clear hrw + apply add_le_add_left + have h : 0 <= (↑↑ε₁ / ↑↑ε₂) * (↑↑ε₃ / ↑↑ε₄ : ℝ) := by + apply mul_nonneg <;> apply div_nonneg <;> linarith + linarith + -- Rewrite the upper bounds in terms of Renyi divergences of nq1/nq2 + rw [zCDPBound] at h1 + have marginal_ub := h1 α Hα l₁ l₂ Hneighbours + have conditional_ub : (⨆ (u : U), RenyiDivergence (nq2 u l₁) (nq2 u l₂) α ≤ 1 / 2 * (↑↑ε₃ / ↑↑ε₄) ^ 2 * α) := + ciSup_le fun x => h2 x α Hα l₁ l₂ Hneighbours + apply (@LE.le.trans _ _ _ (RenyiDivergence (nq1 l₁) (nq1 l₂) α + ⨆ (u : U), RenyiDivergence (nq2 u l₁) (nq2 u l₂) α) _ _ ?case_alg) + case case_alg => linarith + apply (privComposeAdaptive_renyi_bound _ _ _ _) <;> aesop + +/-- +``privComposeAdaptive`` satisfies zCDP +-/ +theorem privComposeAdaptive_zCDP {nq1 : List T → SLang U} {nq2 : U -> List T → SLang V} {ε₁ ε₂ ε₃ ε₄ : ℕ+} + (h : zCDP nq1 ((ε₁ : ℝ) / ε₂)) + (h' : ∀ u, zCDP (nq2 u) ((ε₃ : ℝ) / ε₄)) + (NonTopSum_Uniform : ∃ (z : ℝ), ∀ (u : U), ∀ l, ∑'(v : V), nq2 u l v ≤ ENNReal.ofReal z) + (RenyiBound_Uniform : URDBound nq2 (fun α l₁ l₂ => ⨆ u, RenyiDivergence (nq2 u l₁) (nq2 u l₂) α)) : + zCDP (privComposeAdaptive nq1 nq2) (((ε₁ : ℝ) / ε₂) + ((ε₃ : ℝ) / ε₄)) := by + simp [zCDP] at * + have _ : RDBounded nq2 := RDBounded_of_URDBound nq2 (fun α l₁ l₂ => ⨆ u, RenyiDivergence (nq2 u l₁) (nq2 u l₂) α) RenyiBound_Uniform + repeat any_goals constructor + · apply privComposeAdaptive_zCDPBound <;> aesop + · apply privComposeAdaptive_NonZeroNQ <;> aesop + · apply privComposeAdaptive_NonTopSum <;> aesop + · apply privComposeAdaptive_NonTopNQ <;> aesop + · apply privComposeAdaptive_NonTopRDNQ <;> aesop +end SLang diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Composition.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Composition.lean index 92fec776..c74d6647 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Composition.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Composition.lean @@ -22,225 +22,230 @@ namespace SLang variable { T U V : Type } variable [Inhabited U] variable [Inhabited V] - -lemma ENNReal_toReal_NZ (x : ENNReal) (h1 : x ≠ 0) (h2 : x ≠ ⊤) : - x.toReal ≠ 0 := by - unfold ENNReal.toReal - unfold ENNReal.toNNReal - simp - constructor ; any_goals trivial - -lemma simp_α_1 {α : ℝ} (h : 1 < α) : 0 < α := by - apply @lt_trans _ _ _ 1 _ _ h - simp only [zero_lt_one] - -/-- -The Renyi Divergence between neighbouring inputs of noised queries is nonzero. --/ -theorem Renyi_noised_query_NZ {nq : List T → SLang U} {α ε : ℝ} (h1 : 1 < α) {l₁ l₂ : List T} (h2 : Neighbour l₁ l₂) (h3 : zCDPBound nq ε) (h4 : NonZeroNQ nq) (h5 : NonTopRDNQ nq) (nts : NonTopNQ nq) : - (∑' (i : U), nq l₁ i ^ α * nq l₂ i ^ (1 - α)).toReal ≠ 0 := by - simp [zCDPBound] at h3 - replace h3 := h3 α h1 l₁ l₂ h2 - simp [RenyiDivergence] at h3 - simp [NonZeroNQ] at h4 - simp [NonTopRDNQ] at h5 - replace h5 := h5 α h1 l₁ l₂ h2 - have h6 := h4 l₁ - have h7 := h4 l₂ - apply ENNReal_toReal_NZ - . by_contra CONTRA - rw [ENNReal.tsum_eq_zero] at CONTRA - replace CONTRA := CONTRA default - replace h6 := h6 default - replace h7 := h7 default - rw [_root_.mul_eq_zero] at CONTRA - cases CONTRA - . rename_i h8 - rw [rpow_eq_zero_iff_of_pos] at h8 - contradiction - apply simp_α_1 h1 - . rename_i h8 - rw [ENNReal.rpow_eq_zero_iff] at h8 - cases h8 - . rename_i h8 - cases h8 - contradiction - . rename_i h8 - cases h8 - rename_i h8 h9 - replace nts := nts l₂ default - contradiction - . exact h5 +variable [MeasurableSpace U] [MeasurableSingletonClass U] [Countable U] +variable [MeasurableSpace V] [MeasurableSingletonClass V] [Countable V] /-- Composed queries satisfy zCDP Renyi divergence bound. -/ -theorem privCompose_zCDPBound {nq1 : List T → SLang U} {nq2 : List T → SLang V} {ε₁ ε₂ ε₃ ε₄ : ℕ+} (h1 : zCDPBound nq1 ((ε₁ : ℝ) / ε₂)) (h2 : zCDPBound nq2 ((ε₃ : ℝ) / ε₄)) (nn1 : NonZeroNQ nq1) (nn2 : NonZeroNQ nq2) (nt1 : NonTopRDNQ nq1) (nt2 : NonTopRDNQ nq2) (nts1 : NonTopNQ nq1) (nts2 : NonTopNQ nq2) : +theorem privCompose_zCDPBound {nq1 : Mechanism T U} {nq2 : Mechanism T V} {ε₁ ε₂ ε₃ ε₄ : ℕ+} + (h1 : zCDPBound nq1 ((ε₁ : ℝ) / ε₂)) (h2 : zCDPBound nq2 ((ε₃ : ℝ) / ε₄)) + (Ha1 : ACNeighbour nq1) (Ha2 : ACNeighbour nq2) : zCDPBound (privCompose nq1 nq2) (((ε₁ : ℝ) / ε₂) + ((ε₃ : ℝ) / ε₄)) := by simp [privCompose, RenyiDivergence, zCDPBound] intro α h3 l₁ l₂ h4 - have X := h1 - have Y := h2 simp [zCDPBound] at h1 h2 replace h1 := h1 α h3 l₁ l₂ h4 replace h2 := h2 α h3 l₁ l₂ h4 simp [RenyiDivergence] at h1 h2 - rw [tsum_prod' ENNReal.summable (fun b : U => ENNReal.summable)] - . simp - conv => - left - right - right - right - right - intro b - right - intro c - rw [compose_sum_rw] - rw [compose_sum_rw] - rw [ENNReal.mul_rpow_of_nonneg _ _ (le_of_lt (lt_trans zero_lt_one h3))] - rw [ENNReal.mul_rpow_of_ne_top (nts1 l₂ b) (nts2 l₂ c)] - rw [mul_assoc] - right - rw [mul_comm] - rw [mul_assoc] - right - rw [mul_comm] - conv => - left - right - right - right - right - intro b - right - intro c - rw [← mul_assoc] - conv => - left - right - right - right - right - intro b - rw [ENNReal.tsum_mul_left] - rw [ENNReal.tsum_mul_right] - rw [ENNReal.toReal_mul] - rw [Real.log_mul] - . rw [mul_add] - have D := _root_.add_le_add h1 h2 - apply le_trans D - rw [← add_mul] - rw [mul_le_mul_iff_of_pos_right] - . rw [← mul_add] - rw [mul_le_mul_iff_of_pos_left] - . ring_nf - simp - . simp - . apply lt_trans zero_lt_one h3 - . apply Renyi_noised_query_NZ h3 h4 X nn1 nt1 nts1 - . apply Renyi_noised_query_NZ h3 h4 Y nn2 nt2 nts2 - -/-- -All outputs of a composed query have finite probability. --/ -theorem privCompose_NonTopNQ {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nt1 : NonTopNQ nq1) (nt2 : NonTopNQ nq2) : - NonTopNQ (privCompose nq1 nq2) := by - simp [NonTopNQ] at * - intro l a b - replace nt1 := nt1 l a - replace nt2 := nt2 l b - simp [privCompose] - rw [compose_sum_rw] - rw [mul_eq_top] - intro H - cases H - . rename_i H - cases H - contradiction - . rename_i H - cases H - contradiction - -/-- -Renyi divergence beteeen composed queries on neighbours are finite. --/ -theorem privCompose_NonTopRDNQ {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nt1 : NonTopRDNQ nq1) (nt2 : NonTopRDNQ nq2) (nn1 : NonTopNQ nq1) (nn2 : NonTopNQ nq2) : - NonTopRDNQ (privCompose nq1 nq2) := by - simp [NonTopRDNQ] at * - intro α h1 l₁ l₂ h2 - replace nt1 := nt1 α h1 l₁ l₂ h2 - replace nt2 := nt2 α h1 l₁ l₂ h2 - simp [privCompose] - rw [ENNReal.tsum_prod'] + unfold RenyiDivergence_def + unfold RenyiDivergence_def at h1 h2 + rw [DFunLike.coe] + rw [PMF.instFunLike] simp + repeat rw [SLang.toPMF] + have CG1 (b : U) : (nq1 l₂).val b ≠ ⊤ := by + have H := PMF.apply_ne_top (nq1 l₂) b + simp [DFunLike.coe, PMF.instFunLike] at H + apply H + have CG2 (b : V) : (nq2 l₂).val b ≠ ⊤ := by + have H := PMF.apply_ne_top (nq2 l₂) b + simp [DFunLike.coe, PMF.instFunLike] at H + apply H + simp + rw [tsum_prod' ENNReal.summable (fun b : U => ENNReal.summable)] + simp [PMF.bind, PMF.pure, DFunLike.coe, PMF.instFunLike] conv => - right - left - right - intro x - right - intro y - congr - . left - rw [compose_sum_rw] - . left - rw [compose_sum_rw] - conv => - right - left - right - intro x - right - intro y - rw [ENNReal.mul_rpow_of_nonneg _ _ (le_of_lt (lt_trans zero_lt_one h1))] - rw [ENNReal.mul_rpow_of_ne_top (nn1 l₂ x) (nn2 l₂ y)] + enter [1, 1, 2, 1, 1, b, 1, c] + rw [compose_sum_rw] + rw [compose_sum_rw] + rw [ENNReal.mul_rpow_of_nonneg _ _ (le_of_lt (lt_trans zero_lt_one h3))] + rw [ENNReal.mul_rpow_of_ne_top (CG1 b) (CG2 c)] rw [mul_assoc] right rw [mul_comm] rw [mul_assoc] right rw [mul_comm] + clear CG1 + clear CG2 conv => - right - left - right - intro x - right - intro y + enter [1, 1, 2, 1, 1, b, 1, c] rw [← mul_assoc] conv => - right - left - right - intro x + enter [1, 1, 2, 1, 1, b] rw [ENNReal.tsum_mul_left] rw [ENNReal.tsum_mul_right] - intro H - rw [mul_eq_top] at H - cases H - . rename_i h3 - cases h3 - rename_i h4 h5 - contradiction - . rename_i h3 - cases h3 - rename_i h4 h5 - contradiction + rw [← elog_mul] + + have log_nonneg_1 : 0 ≤ (∑' (i : U), (nq1 l₁).val i ^ α * (nq1 l₂).val i ^ (1 - α)).elog := by + have Hac1 : AbsCts (nq1 l₁) (nq1 l₂) := by exact Ha1 l₁ l₂ h4 + apply (RenyiDivergence_def_log_sum_nonneg (nq1 l₁) (nq1 l₂) Hac1 h3) + have log_nonneg_2 : 0 ≤ (∑' (i : V), (nq2 l₁).val i ^ α * (nq2 l₂).val i ^ (1 - α)).elog := by + have Hac2 : AbsCts (nq2 l₁) (nq2 l₂) := by exact Ha2 l₁ l₂ h4 + have Hnn2 := (RenyiDivergence_def_log_sum_nonneg (nq2 l₁) (nq2 l₂) Hac2 h3) + apply Hnn2 + + -- Split up the series + rw [ofEReal_mul_nonneg] + · simp only [ofEReal_real] + -- In order to distribute ofReal, we need the logarithms to be nonegative + rw [ofEReal_plus_nonneg log_nonneg_1 log_nonneg_2] + + -- Distribute + rw [CanonicallyOrderedCommSemiring.left_distrib] + apply (@le_trans _ _ _ (ENNReal.ofReal (2⁻¹ * (↑↑ε₁ ^ 2 / ↑↑ε₂ ^ 2) * α) + ENNReal.ofReal (2⁻¹ * (↑↑ε₃ ^ 2 / ↑↑ε₄ ^ 2) * α))) + · apply _root_.add_le_add + · rw [ofEReal_mul_nonneg] at h1 + · apply h1 + · apply EReal.coe_nonneg.mpr + apply inv_nonneg.mpr + linarith + · apply log_nonneg_1 + · rw [ofEReal_mul_nonneg] at h2 + · apply h2 + · apply EReal.coe_nonneg.mpr + apply inv_nonneg.mpr + linarith + · apply log_nonneg_2 + · clear h1 h2 + rw [<- ENNReal.ofReal_add] + · apply ofReal_le_ofReal_iff'.mpr + left + rw [← add_mul] + rw [mul_le_mul_iff_of_pos_right] + · rw [← mul_add] + rw [mul_le_mul_iff_of_pos_left] + · ring_nf + simp only [inv_pow, add_le_add_iff_right, le_add_iff_nonneg_left, gt_iff_lt, inv_pos, Nat.cast_pos, PNat.pos, + mul_pos_iff_of_pos_right, mul_pos_iff_of_pos_left, mul_nonneg_iff_of_pos_left, Nat.ofNat_nonneg] + · simp only [inv_pos, Nat.ofNat_pos] + · linarith + · apply mul_nonneg + · apply mul_nonneg + · simp + · apply div_nonneg + · exact sq_nonneg ε₁.val.cast + · exact sq_nonneg ε₂.val.cast + · linarith + · apply mul_nonneg + · apply mul_nonneg + · simp + · apply div_nonneg + · exact sq_nonneg ε₃.val.cast + · exact sq_nonneg ε₄.val.cast + · linarith + · simp + linarith + · apply Left.add_nonneg + · apply log_nonneg_1 + · apply log_nonneg_2 + + +/- +Renyi divergence beteeen composed queries on neighbours are finite. +-/ +-- theorem privCompose_NonTopRDNQ {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nt1 : NonTopRDNQ nq1) (nt2 : NonTopRDNQ nq2) (nn1 : NonTopNQ nq1) (nn2 : NonTopNQ nq2) : +-- NonTopRDNQ (privCompose nq1 nq2) := by +-- simp [NonTopRDNQ] at * +-- intro α h1 l₁ l₂ h2 +-- replace nt1 := nt1 α h1 l₁ l₂ h2 +-- replace nt2 := nt2 α h1 l₁ l₂ h2 +-- simp [privCompose] +-- rw [ENNReal.tsum_prod'] +-- simp +-- conv => +-- right +-- left +-- right +-- intro x +-- right +-- intro y +-- congr +-- . left +-- rw [compose_sum_rw] +-- . left +-- rw [compose_sum_rw] +-- conv => +-- right +-- left +-- right +-- intro x +-- right +-- intro y +-- rw [ENNReal.mul_rpow_of_nonneg _ _ (le_of_lt (lt_trans zero_lt_one h1))] +-- rw [ENNReal.mul_rpow_of_ne_top (nn1 l₂ x) (nn2 l₂ y)] +-- rw [mul_assoc] +-- right +-- rw [mul_comm] +-- rw [mul_assoc] +-- right +-- rw [mul_comm] +-- conv => +-- right +-- left +-- right +-- intro x +-- right +-- intro y +-- rw [← mul_assoc] +-- conv => +-- right +-- left +-- right +-- intro x +-- rw [ENNReal.tsum_mul_left] +-- rw [ENNReal.tsum_mul_right] +-- intro H +-- rw [mul_eq_top] at H +-- cases H +-- . rename_i h3 +-- cases h3 +-- rename_i h4 h5 +-- contradiction +-- . rename_i h3 +-- cases h3 +-- rename_i h4 h5 +-- contradiction + +/-- +``privCompose`` preserves absolute continuity between neighbours +-/ +def privCompose_AC (nq1 : Mechanism T U) (nq2 : Mechanism T V) (Hac1 : ACNeighbour nq1) (Hac2 : ACNeighbour nq2) : + ACNeighbour (privCompose nq1 nq2) := by + rw [ACNeighbour] at * + intro l₁ l₂ Hn + have Hac1 := Hac1 l₁ l₂ Hn + have Hac2 := Hac2 l₁ l₂ Hn + rw [AbsCts] at * + intro x + rcases x with ⟨ u, v ⟩ + intro Hk + simp [privCompose] at * + intro i + cases (Hk i) + · rename_i Hk + left + apply Hac1 + apply Hk + · rename_i Hk + right + intro H + apply Hac2 + apply Hk + apply H + /-- ``privCompose`` satisfies zCDP -/ -theorem privCompose_zCDP (nq1 : List T → SLang U) (nq2 : List T → SLang V) (ε₁ ε₂ ε₃ ε₄ : ℕ+) (h : zCDP nq1 ((ε₁ : ℝ) / ε₂)) (h' : zCDP nq2 ((ε₃ : ℝ) / ε₄)) : - zCDP (privCompose nq1 nq2) (((ε₁ : ℝ) / ε₂) + ((ε₃ : ℝ) / ε₄)) := by +theorem privCompose_zCDP (nq1 : Mechanism T U) (nq2 : Mechanism T V) (ε₁ ε₂ ε₃ ε₄ : ℕ+) (h : zCDP nq1 ((ε₁ : ℝ) / ε₂)) (h' : zCDP nq2 ((ε₃ : ℝ) / ε₄)) : + zCDP (privCompose nq1 nq2) (((ε₁ : ℝ) / ε₂) + ((ε₃ : ℝ) / ε₄)) := by simp [zCDP] at * - cases h ; rename_i h1 h2 ; cases h2 ; rename_i h2 h3 ; cases h3 ; rename_i h3 h4 ; cases h4 ; rename_i h4 h5 - cases h' ; rename_i h'1 h'2 ; cases h'2 ; rename_i h'2 h'3 ; cases h'3 ; rename_i h'3 h'4 ; cases h'4 ; rename_i h'4 h'5 - repeat any_goals constructor - . apply privCompose_zCDPBound h1 h'1 h2 h'2 h5 h'5 h4 h'4 - . apply privCompose_NonZeroNQ h2 h'2 - . apply privCompose_NonTopSum h3 h'3 - . apply privCompose_NonTopNQ h4 h'4 - . apply privCompose_NonTopRDNQ h5 h'5 h4 h'4 + rcases h with ⟨ Hac1, Hb1 ⟩ + rcases h' with ⟨ Hac2, Hb2 ⟩ + apply And.intro + · exact privCompose_AC nq1 nq2 Hac1 Hac2 + · exact privCompose_zCDPBound Hb1 Hb2 Hac1 Hac2 end SLang diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean index 04cbc211..9d360b3c 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean @@ -14,8 +14,8 @@ import SampCert.Samplers.GaussianGen.Basic /-! # Concentrated Bound -This file derives a cDP bound for the discrete Gaussian. In particular, it bounds -the Renyi divergence between discrete Gaussian evaluations with integer means. +This file derives a cDP bound on the discrete Gaussian, and for the discrete Gaussian +sampler. -/ open Real Nat @@ -84,8 +84,7 @@ lemma SG_Renyi_simplify {σ : ℝ} (h : σ ≠ 0) (μ ν : ℤ) (α : ℝ) : rfl /-- -Alternative definition for the Renyi Divergence. -FIXME: is there any reason to not get rid of this? +Real-valued Renyi Divergence. -/ noncomputable def RenyiDivergence' (p q : T → ℝ) (α : ℝ) : ℝ := (1 / (α - 1)) * Real.log (∑' x : T, (p x)^α * (q x)^(1 - α)) @@ -526,43 +525,88 @@ theorem Renyi_Gauss_summable {σ : ℝ} (h : σ ≠ 0) (μ ν : ℤ) (α : ℝ) apply Summable.mul_right apply summable_gauss_term' h + /-- Upper bound on Renyi divergence between discrete Gaussians. -/ theorem Renyi_Gauss_divergence_bound' {σ α : ℝ} (h : σ ≠ 0) (h' : 1 < α) (μ ν : ℤ) : - RenyiDivergence (fun (x : ℤ) => ENNReal.ofReal (discrete_gaussian σ μ x)) - (fun (x : ℤ) => ENNReal.ofReal (discrete_gaussian σ ν x)) - α ≤ α * (((μ - ν) : ℤ)^2 / (2 * σ^2)) := by - have A : RenyiDivergence (fun (x : ℤ) => ENNReal.ofReal (discrete_gaussian σ μ x)) - (fun (x : ℤ) => ENNReal.ofReal (discrete_gaussian σ ν x)) - α = RenyiDivergence' (fun (x : ℤ) => discrete_gaussian σ μ x) - (fun (x : ℤ) => discrete_gaussian σ ν x) - α := by + RenyiDivergence (discrete_gaussian_pmf h μ) + (discrete_gaussian_pmf h ν) + α ≤ (ENNReal.ofReal α) * (ENNReal.ofReal ((((μ - ν) : ℤ)^2 : ℝ) / (2 * σ^2))) := by + have A : RenyiDivergence (discrete_gaussian_pmf h μ) (discrete_gaussian_pmf h ν) α = + ENNReal.ofReal (RenyiDivergence' (fun (x : ℤ) => discrete_gaussian σ μ x) (fun (x : ℤ) => discrete_gaussian σ ν x) α) := by unfold RenyiDivergence + unfold RenyiDivergence_def unfold RenyiDivergence' congr simp - have A₁ : ∀ x : ℤ, 0 ≤ discrete_gaussian σ μ x ^ α := by - intro x - apply Real.rpow_nonneg - apply discrete_gaussian_nonneg h μ x + unfold discrete_gaussian_pmf + + have Hdg_pos (x : ℤ) (w : ℝ) : OfNat.ofNat 0 < discrete_gaussian σ w x.cast := by + exact discrete_gaussian_pos h w x + have Hdg_pow_pos (x : ℤ) w : OfNat.ofNat 0 ≤ discrete_gaussian σ w x.cast ^ α := by + apply rpow_nonneg + exact discrete_gaussian_nonneg h w x + conv => - left - right - right + lhs + arg 1 + arg 2 + arg 1 + arg 1 intro x - rw [ENNReal.ofReal_rpow_of_pos (discrete_gaussian_pos h μ x)] - rw [ENNReal.ofReal_rpow_of_pos (discrete_gaussian_pos h ν x)] - rw [← ENNReal.ofReal_mul (A₁ x)] - rw [← ENNReal.ofReal_tsum_of_nonneg] - . simp - apply tsum_nonneg - intro i - apply Renyi_sum_SG_nonneg h - . apply Renyi_sum_SG_nonneg h - . apply Renyi_Gauss_summable h + simp [DFunLike.coe] + rw [ENNReal.ofReal_rpow_of_pos (Hdg_pos x μ.cast)] + rw [ENNReal.ofReal_rpow_of_pos (Hdg_pos x ν.cast)] + rw [<- ENNReal.ofReal_mul (Hdg_pow_pos x μ.cast)] + rw [<- ENNReal.ofEReal_ofReal_toENNReal] + simp + congr + cases (Classical.em (0 = ∑' (x : ℤ), discrete_gaussian σ μ.cast x.cast ^ α * discrete_gaussian σ ν.cast x.cast ^ (1 - α))) + · rename_i Hzero + rw [<- Hzero] + simp + rw [<- ENNReal.ofReal_tsum_of_nonneg] + · rw [<- Hzero] + exfalso + symm at Hzero + have Hzero' : (ENNReal.ofReal (∑' (x : ℤ), discrete_gaussian σ ↑μ ↑x ^ α * discrete_gaussian σ ↑ν ↑x ^ (1 - α)) = 0) := by + simp [Hzero] + rw [ENNReal.ofReal_tsum_of_nonneg ?G1 ?G2] at Hzero' + case G1 => exact fun n => Renyi_sum_SG_nonneg h μ ν n + case G2 => exact Renyi_Gauss_summable h μ ν α + apply ENNReal.tsum_eq_zero.mp at Hzero' + have Hzero'' := Hzero' (0 : ℤ) + simp at Hzero'' + have C : (0 < discrete_gaussian σ (↑μ) 0 ^ α * discrete_gaussian σ (↑ν) 0 ^ (1 - α)) := by + apply Real.mul_pos + · apply Real.rpow_pos_of_pos + have A := discrete_gaussian_pos h μ (0 : ℤ) + simp at A + apply A + · apply Real.rpow_pos_of_pos + have A := discrete_gaussian_pos h ν (0 : ℤ) + simp at A + apply A + linarith + · exact fun n => Renyi_sum_SG_nonneg h μ ν n + · exact Renyi_Gauss_summable h μ ν α + · rename_i Hnz + rw [<- ENNReal.elog_ENNReal_ofReal_of_pos] + · rw [ENNReal.ofReal_tsum_of_nonneg ?Hnn] + · exact Renyi_Gauss_summable h μ ν α + · intro n + exact Renyi_sum_SG_nonneg h μ ν n + apply lt_of_le_of_ne + · apply tsum_nonneg + intro i + exact Renyi_sum_SG_nonneg h μ ν i + · apply Hnz rw [A] - apply Renyi_divergence_bound_pre h h' + rw [<- ENNReal.ofReal_mul] + apply ENNReal.ofReal_le_ofReal + apply Renyi_divergence_bound_pre h h' μ ν + linarith namespace SLang @@ -570,18 +614,51 @@ namespace SLang Upper bound on Renyi divergence between outputs of the ``SLang`` discrete Gaussian sampler. -/ theorem discrete_GaussianGenSample_ZeroConcentrated {α : ℝ} (h : 1 < α) (num : PNat) (den : PNat) (μ ν : ℤ) : - RenyiDivergence ((DiscreteGaussianGenSample num den μ)) (DiscreteGaussianGenSample num den ν) α ≤ - α * (((μ - ν) : ℤ)^2 / (2 * ((num : ℝ) / (den : ℝ))^2)) := by + RenyiDivergence ((DiscreteGaussianGenPMF num den μ)) (DiscreteGaussianGenPMF num den ν) α ≤ + (ENNReal.ofReal α) * (ENNReal.ofReal (((μ - ν) : ℤ)^2 : ℝ) / (((2 : ENNReal) * ((num : ENNReal) / (den : ENNReal))^2 : ENNReal))) := by have A : (num : ℝ) / (den : ℝ) ≠ 0 := by simp only [ne_eq, div_eq_zero_iff, cast_eq_zero, PNat.ne_zero, or_self, not_false_eq_true] + have Hpmf (w : ℤ) : (discrete_gaussian_pmf A w = DiscreteGaussianGenPMF num den w) := by + simp [discrete_gaussian_pmf] + simp [DiscreteGaussianGenPMF] + congr + apply funext + intro z + rw [← DiscreteGaussianGenSample_apply] conv => left congr - . intro x - rw [DiscreteGaussianGenSample_apply] - . intro x - rw [DiscreteGaussianGenSample_apply] + . rw [<- Hpmf] + . rw [<- Hpmf] . skip - apply Renyi_Gauss_divergence_bound' A h + apply le_trans + · apply (Renyi_Gauss_divergence_bound') + apply h + · have X : (OfNat.ofNat 2 * (num.val.cast / den.val.cast) ^ OfNat.ofNat 2) = ENNReal.ofReal (OfNat.ofNat 2 * (num.val.cast / den.val.cast) ^ OfNat.ofNat 2) := by + simp + rw [ENNReal.ofReal_mul ?Hnn] + case Hnn => simp + congr + · simp + · rw [ENNReal.ofReal_div_of_pos ?Hpos] + case Hpos => simp + repeat rw [sq] + rw [ENNReal.ofReal_mul ?Hnn1] + case Hnn1 => simp + rw [ENNReal.ofReal_mul ?Hnn2] + case Hnn2 => simp + simp + repeat rw [ENNReal.div_eq_inv_mul] + rw [mul_mul_mul_comm] + congr + rw [ENNReal.mul_inv] + · right + simp + · left + simp + rw [X] + rw [ENNReal.ofReal_div_of_pos] + congr + simp end SLang diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean index 1d8dda8d..d9f6a36f 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean @@ -31,12 +31,9 @@ Inequality defining ``(ε^2)/2``-zCDP. All ``ε``-DP mechanisms satisfy this bound (though not all mechanisms satisfying this bound are ``ε``-DP). -/ -def zCDPBound (q : List T → SLang U) (ε : ℝ) : Prop := +def zCDPBound (q : List T → PMF U) (ε : ℝ) : Prop := ∀ α : ℝ, 1 < α → ∀ l₁ l₂ : List T, Neighbour l₁ l₂ → - RenyiDivergence (q l₁) (q l₂) α ≤ (1/2) * ε ^ 2 * α - -def NonTopNQ (nq : List T → SLang U) := - ∀ l : List T, ∀ n : U, nq l n ≠ ⊤ + RenyiDivergence (q l₁) (q l₂) α ≤ ENNReal.ofReal ((1/2) * ε ^ 2 * α) /-- The Renyi divergence between neighbouring elements of the output of ``nq`` is finite. @@ -45,12 +42,12 @@ def NonTopRDNQ (nq : List T → SLang U) : Prop := ∀ α : ℝ, 1 < α → ∀ l₁ l₂ : List T, Neighbour l₁ l₂ → ∑' (x : U), nq l₁ x ^ α * nq l₂ x ^ (1 - α) ≠ ⊤ +/-- +All neighbouring queries are absolutely continuous +-/ +def ACNeighbour (p : List T -> PMF U) : Prop := ∀ l₁ l₂, Neighbour l₁ l₂ -> AbsCts (p l₁) (p l₂) + /-- The mechanism ``q`` is ``(ε^2)/2``-zCDP -/ -def zCDP (q : List T → SLang U) (ε : ℝ) : Prop := - zCDPBound q ε - ∧ NonZeroNQ q - ∧ NonTopSum q - ∧ NonTopNQ q - ∧ NonTopRDNQ q +def zCDP (q : List T → PMF U) (ε : ℝ) : Prop := ACNeighbour q ∧ zCDPBound q ε diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Code.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Code.lean index 7af53520..232c510e 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Code.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Code.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ -import SampCert.Samplers.GaussianGen.Code +import SampCert.Samplers.GaussianGen.Properties /-! # ``privNoisedQuery`` Implementation @@ -18,7 +18,7 @@ namespace SLang /-- Mechanism obtained by postcomposing query with by gaussian noise (of variance ``(Δ ε₁ / ε₂)^2``). -/ -def privNoisedQuery (query : List T → ℤ) (Δ : ℕ+) (ε₁ ε₂ : ℕ+) (l : List T) : SLang ℤ := do - DiscreteGaussianGenSample (Δ * ε₂) ε₁ (query l) +def privNoisedQuery (query : List T → ℤ) (Δ : ℕ+) (ε₁ ε₂ : ℕ+) (l : List T) : PMF ℤ := do + DiscreteGaussianGenPMF (Δ * ε₂) ε₁ (query l) end SLang diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean index 393dc881..381ec5f1 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean @@ -28,13 +28,93 @@ theorem privNoisedQuery_zCDPBound (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ have A := @discrete_GaussianGenSample_ZeroConcentrated α h1 (Δ * ε₂) ε₁ (query l₁) (query l₂) apply le_trans A clear A + + -- Pull out the ENNReal.ofReal, reducing it to a Real case + rw [ENNReal.div_eq_inv_mul] + have L : (OfNat.ofNat 2 * ((Δ * ε₂).val.cast / ε₁.val.cast) ^ OfNat.ofNat 2)⁻¹ = ENNReal.ofReal ((OfNat.ofNat 2 * ((Δ * ε₂).val.cast / ε₁.val.cast) ^ OfNat.ofNat 2)⁻¹ ) := by + simp + rw [← div_pow] + conv => + rhs + arg 1 + rw [mul_comm] + rw [ENNReal.mul_inv] + · rw [ENNReal.ofReal_mul ?G1] + case G1 => + simp + congr + · rw [ENNReal.ofReal_inv_of_pos] + congr + simp + exact zero_lt_two + · rw [ENNReal.inv_pow] + rw [ENNReal.ofReal_pow ?G] + case G => + apply div_nonneg + · simp + · simp + congr + repeat rewrite [ENNReal.div_eq_inv_mul] + rw [ENNReal.mul_inv ?G1 ?G2] + case G1 => + left + simp + case G2 => + left + simp + simp + rw [div_eq_mul_inv] + rw [ENNReal.ofReal_mul] + · simp + congr + rw [ENNReal.mul_inv] + · rw [ENNReal.ofReal_mul] + · rw [mul_comm] + congr + · rw [ENNReal.ofReal_inv_of_pos] + · congr + simp + · simp + · rw [ENNReal.ofReal_inv_of_pos] + · congr + simp + · simp + · simp + · left ; simp + · left ; simp + · simp + · left ; simp + · left ; simp + rw [L] + have H1 : OfNat.ofNat 0 ≤ ((OfNat.ofNat (OfNat.ofNat 2) * ((Δ * ε₂).val.cast / ε₁.val.cast) ^ OfNat.ofNat (OfNat.ofNat 2))⁻¹ : ℝ) := by + simp + apply div_nonneg + · simp + · simp + have H2 : OfNat.ofNat 0 ≤ α := by linarith + conv => + lhs + arg 2 + rw [<- ENNReal.ofReal_mul] + · skip + . apply H1 + conv => + lhs + rw [<- ENNReal.ofReal_mul] + · skip + · apply H2 + clear H1 + clear H2 + apply ofReal_le_ofReal_iff'.mpr + + replace bounded_sensitivity := bounded_sensitivity l₁ l₂ h2 ring_nf simp conv => left left - right + left rw [mul_pow] conv => left @@ -42,79 +122,61 @@ theorem privNoisedQuery_zCDPBound (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ right rw [mul_comm] rw [← mul_assoc] + + left + -- Move α to left conv => - left + rhs rw [mul_assoc] - right - rw [← mul_assoc] - left rw [mul_comm] - rw [← mul_assoc] - rw [← mul_assoc] - rw [← mul_assoc] - simp only [inv_pow] - rw [mul_inv_le_iff'] - . have A : (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹) ≤ (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹) := le_refl (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹) - have B : 0 ≤ (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹) := by - simp - apply @le_trans ℝ _ 0 1 α (zero_le_one' ℝ) (le_of_lt h1) - apply mul_le_mul A _ _ B - . apply sq_le_sq.mpr - simp only [abs_cast] - rw [← Int.cast_sub] - rw [← Int.cast_abs] - apply Int.cast_le.mpr - rw [← Int.natCast_natAbs] - apply Int.ofNat_le.mpr - trivial - . apply sq_nonneg - . rw [pow_two] - rw [_root_.mul_pos_iff] - left - simp - -/-- -All outputs of the zCDP mechanism have nonzero probability. --/ -theorem privNoisedQuery_NonZeroNQ (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) : - NonZeroNQ (privNoisedQuery query Δ ε₁ ε₂) := by - simp [NonZeroNQ, privNoisedQuery, DiscreteGaussianGenSample] - intros l n - exists (n - query l) - simp - have A : ((Δ : ℝ) * ε₂ / ε₁) ≠ 0 := by - simp - have X := @discrete_gaussian_pos (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) A 0 (n - query l) - simp at X - trivial - -/-- -All outputs of the zCDP mechanism have finite probability. --/ -theorem privNoisedQuery_NonTopNQ (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) : - NonTopNQ (privNoisedQuery query Δ ε₁ ε₂) := by - simp [NonTopNQ, privNoisedQuery, DiscreteGaussianGenSample] - intro l n - rw [ENNReal.tsum_eq_add_tsum_ite (n - query l)] - simp - have X : ∀ x : ℤ, (@ite ℝ≥0∞ (x = n - query l) (propDecidable (x = n - query l)) 0 - (@ite ℝ≥0∞ (n = x + query l) (n.instDecidableEq (x + query l)) - (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x)) 0)) = 0 := by - intro x - split - . simp - . split - . rename_i h1 h2 - subst h2 - simp at h1 - . simp + -- Move ε₁^2 to the left conv => - right + lhs + rw [<- mul_assoc] + arg 1 + rw [mul_assoc] + arg 2 + rw [mul_comm] + conv => + lhs + rw [<- mul_assoc] + rw [<- mul_assoc] + -- Add factor of 1 on the right + conv => + rhs + rw [<- (mul_one (α * ε₁ ^ 2 * ((ε₂ : ℝ)^ 2)⁻¹ : ℝ))] + -- Reassocaite on left + conv => + lhs + rw [mul_assoc] + apply mul_le_mul + · simp only [inv_pow, le_refl] + · simp + rw [inv_mul_eq_div] + rw [div_le_one_iff] left - right - intro x - rw [X] - simp + apply And.intro + · apply sq_pos_iff.mpr + simp + · apply sq_le_sq.mpr + clear L h2 h1 α + rw [<- Int.dist_eq] + rw [Int.dist_eq'] + have X : ((query l₁ - query l₂).natAbs : ℝ) ≤ (Δ.val : ℝ) := by + apply Nat.cast_le.mpr + apply bounded_sensitivity + rw [abs_eq_natAbs] + simp only [abs_cast] + exact X + · apply mul_nonneg + · apply sq_nonneg + · apply sq_nonneg + · apply mul_nonneg + · apply mul_nonneg + · linarith + · apply sq_nonneg + · apply inv_nonneg.mpr + apply sq_nonneg lemma discrete_gaussian_shift {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (τ x : ℤ) : discrete_gaussian σ μ (x - τ) = discrete_gaussian σ (μ + τ) (x) := by @@ -125,143 +187,116 @@ lemma discrete_gaussian_shift {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (τ x : ℤ) ring_nf . rw [shifted_gauss_sum h] -/-- -The zCDP mechanism is normalizable. +/- +The Renyi divergence of the zCDP mechanism is finite on neighbouring inputs. -/ -theorem privNoisedQuery_NonTopSum (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) : - NonTopSum (privNoisedQuery query Δ ε₁ ε₂) := by - simp [NonTopSum, privNoisedQuery, DiscreteGaussianGenSample] - intro l - have X : ∀ n: ℤ, ∀ x : ℤ, (@ite ℝ≥0∞ (x = n - query l) (propDecidable (x = n - query l)) 0 - (@ite ℝ≥0∞ (n = x + query l) (n.instDecidableEq (x + query l)) - (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x)) 0)) = 0 := by - intro n x - split - . simp - . split - . rename_i h1 h2 - subst h2 - simp at h1 - . simp - conv => - right - left - right - intro n - rw [ENNReal.tsum_eq_add_tsum_ite (n - query l)] - simp - right - right - intro x - rw [X] - simp - have A : (Δ : ℝ) * ε₂ / ε₁ ≠ 0 := by - simp - conv => - right - left - right - intro n - rw [discrete_gaussian_shift A] - simp - rw [← ENNReal.ofReal_tsum_of_nonneg] - . rw [discrete_gaussian_normalizes A] - simp - . apply discrete_gaussian_nonneg A - . apply discrete_gaussian_summable' A (query l) +-- theorem privNoisedQuery_NonTopRDNQ (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) : +-- NonTopRDNQ (privNoisedQuery query Δ ε₁ ε₂) := by +-- simp [NonTopRDNQ, privNoisedQuery, DiscreteGaussianGenSample] +-- intro α _ l₁ l₂ _ +-- have A : ∀ x_1 x : ℤ, (@ite ℝ≥0∞ (x_1 = x - query l₁) (propDecidable (x_1 = x - query l₁)) 0 +-- (@ite ℝ≥0∞ (x = x_1 + query l₁) (x.instDecidableEq (x_1 + query l₁)) +-- (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x_1)) 0 )) = 0 := by +-- intro x y +-- split +-- . simp +-- . split +-- . rename_i h1 h2 +-- subst h2 +-- simp at h1 +-- . simp +-- have B : ∀ x_1 x : ℤ, (@ite ℝ≥0∞ (x_1 = x - query l₂) (propDecidable (x_1 = x - query l₂)) 0 +-- (@ite ℝ≥0∞ (x = x_1 + query l₂) (x.instDecidableEq (x_1 + query l₂)) +-- (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x_1)) 0)) = 0 := by +-- intro x y +-- split +-- . simp +-- . split +-- . rename_i h1 h2 +-- subst h2 +-- simp at h1 +-- . simp +-- conv => +-- right +-- left +-- right +-- intro x +-- left +-- rw [ENNReal.tsum_eq_add_tsum_ite (x - query l₁)] +-- simp +-- left +-- right +-- right +-- intro y +-- rw [A] +-- simp +-- conv => +-- right +-- left +-- right +-- intro x +-- right +-- rw [ENNReal.tsum_eq_add_tsum_ite (x - query l₂)] +-- simp +-- left +-- right +-- right +-- intro y +-- rw [B] +-- simp +-- clear A B +-- have P : (Δ : ℝ) * ε₂ / ε₁ ≠ 0 := by +-- simp +-- have A : ∀ x : ℤ, ∀ l : List T, 0 < discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 (↑x - ↑(query l)) := by +-- intro x l +-- have A' := @discrete_gaussian_pos _ P 0 (x - query l) +-- simp at A' +-- trivial +-- have B : ∀ x : ℤ, 0 ≤ discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 (↑x - ↑(query l₁)) ^ α := by +-- intro x +-- have A' := @discrete_gaussian_nonneg _ P 0 (x - query l₁) +-- simp at A' +-- apply rpow_nonneg A' +-- conv => +-- right +-- left +-- right +-- intro x +-- rw [ENNReal.ofReal_rpow_of_pos (A x l₁)] +-- rw [ENNReal.ofReal_rpow_of_pos (A x l₂)] +-- rw [← ENNReal.ofReal_mul (B x)] +-- rw [← ENNReal.ofReal_tsum_of_nonneg] +-- . simp +-- . intro n +-- have X := @Renyi_sum_SG_nonneg _ α P (query l₁) (query l₂) n +-- rw [discrete_gaussian_shift P] +-- rw [discrete_gaussian_shift P] +-- simp [X] +-- . have X := @Renyi_Gauss_summable _ P (query l₁) (query l₂) +-- conv => +-- right +-- intro x +-- rw [discrete_gaussian_shift P] +-- rw [discrete_gaussian_shift P] +-- simp [X] + /-- -The Renyi divergence of the zCDP mechanism is finite on neighbouring inputs. +privNoisedQuery preserves absolute continuity between neighbours -/ -theorem privNoisedQuery_NonTopRDNQ (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) : - NonTopRDNQ (privNoisedQuery query Δ ε₁ ε₂) := by - simp [NonTopRDNQ, privNoisedQuery, DiscreteGaussianGenSample] - intro α _ l₁ l₂ _ - have A : ∀ x_1 x : ℤ, (@ite ℝ≥0∞ (x_1 = x - query l₁) (propDecidable (x_1 = x - query l₁)) 0 - (@ite ℝ≥0∞ (x = x_1 + query l₁) (x.instDecidableEq (x_1 + query l₁)) - (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x_1)) 0 )) = 0 := by - intro x y - split - . simp - . split - . rename_i h1 h2 - subst h2 - simp at h1 - . simp - have B : ∀ x_1 x : ℤ, (@ite ℝ≥0∞ (x_1 = x - query l₂) (propDecidable (x_1 = x - query l₂)) 0 - (@ite ℝ≥0∞ (x = x_1 + query l₂) (x.instDecidableEq (x_1 + query l₂)) - (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x_1)) 0)) = 0 := by - intro x y - split - . simp - . split - . rename_i h1 h2 - subst h2 - simp at h1 - . simp - conv => - right - left - right - intro x - left - rw [ENNReal.tsum_eq_add_tsum_ite (x - query l₁)] - simp - left - right - right - intro y - rw [A] - simp - conv => - right - left - right - intro x - right - rw [ENNReal.tsum_eq_add_tsum_ite (x - query l₂)] - simp - left - right - right - intro y - rw [B] - simp - clear A B - have P : (Δ : ℝ) * ε₂ / ε₁ ≠ 0 := by - simp - have A : ∀ x : ℤ, ∀ l : List T, 0 < discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 (↑x - ↑(query l)) := by - intro x l - have A' := @discrete_gaussian_pos _ P 0 (x - query l) - simp at A' - trivial - have B : ∀ x : ℤ, 0 ≤ discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 (↑x - ↑(query l₁)) ^ α := by - intro x - have A' := @discrete_gaussian_nonneg _ P 0 (x - query l₁) - simp at A' - apply rpow_nonneg A' - conv => - right - left - right - intro x - rw [ENNReal.ofReal_rpow_of_pos (A x l₁)] - rw [ENNReal.ofReal_rpow_of_pos (A x l₂)] - rw [← ENNReal.ofReal_mul (B x)] - rw [← ENNReal.ofReal_tsum_of_nonneg] - . simp - . intro n - have X := @Renyi_sum_SG_nonneg _ α P (query l₁) (query l₂) n - rw [discrete_gaussian_shift P] - rw [discrete_gaussian_shift P] - simp [X] - . have X := @Renyi_Gauss_summable _ P (query l₁) (query l₂) - conv => - right - intro x - rw [discrete_gaussian_shift P] - rw [discrete_gaussian_shift P] - simp [X] +def privNoisedQuery_AC (query : List T -> ℤ) (Δ ε₁ ε₂ : ℕ+) : ACNeighbour (privNoisedQuery query Δ ε₁ ε₂) := by + rw [ACNeighbour] + intro l₁ l₂ _ + rw [AbsCts] + intro n Hk + exfalso + simp [privNoisedQuery, DiscreteGaussianGenPMF, DiscreteGaussianGenSample, DFunLike.coe] at Hk + have Hk := Hk (n - query l₂) + simp at Hk + have A : ((Δ : ℝ) * ε₂ / ε₁) ≠ 0 := by simp + have X := @discrete_gaussian_pos (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) A 0 (n - query l₂) + simp at X + linarith /-- The zCDP mechanism is ``(Δε₂/ε₁)^2``-zCDP. @@ -269,13 +304,11 @@ The zCDP mechanism is ``(Δε₂/ε₁)^2``-zCDP. theorem privNoisedQuery_zCDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_sensitivity : sensitivity query Δ) : zCDP (privNoisedQuery query Δ ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by simp [zCDP] - repeat any_goals constructor - . apply privNoisedQuery_zCDPBound - exact bounded_sensitivity - . apply privNoisedQuery_NonZeroNQ - . apply privNoisedQuery_NonTopSum - . apply privNoisedQuery_NonTopNQ - . apply privNoisedQuery_NonTopRDNQ + apply And.intro + · exact privNoisedQuery_AC query Δ ε₁ ε₂ + · repeat any_goals constructor + . apply privNoisedQuery_zCDPBound + exact bounded_sensitivity end SLang diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean index c89fff25..4ed59926 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean @@ -28,106 +28,25 @@ variable [count : Countable U] variable [disc : DiscreteMeasurableSpace U] variable [Inhabited U] -lemma Integrable_rpow (f : T → ℝ) (nn : ∀ x : T, 0 ≤ f x) (μ : Measure T) (α : ENNReal) (mem : Memℒp f α μ) (h1 : α ≠ 0) (h2 : α ≠ ⊤) : - MeasureTheory.Integrable (fun x : T => (f x) ^ α.toReal) μ := by - have X := @MeasureTheory.Memℒp.integrable_norm_rpow T ℝ t1 μ _ f α mem h1 h2 - revert X - conv => - left - left - intro x - rw [← norm_rpow_of_nonneg (nn x)] - intro X - simp [Integrable] at * - constructor - . cases X - rename_i left right - rw [@aestronglyMeasurable_iff_aemeasurable] - apply AEMeasurable.pow_const - simp [Memℒp] at mem - cases mem - rename_i left' right' - rw [aestronglyMeasurable_iff_aemeasurable] at left' - simp [left'] - . rw [← hasFiniteIntegral_norm_iff] - simp [X] - /-- -Jensen's ineuquality for the exponential applied to Renyi's sum +privPostProcess preserves absolute continuity between neighbours -/ -theorem Renyi_Jensen (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 < α) (h2 : ∀ x : T, 0 ≤ f x) (mem : Memℒp f (ENNReal.ofReal α) (PMF.toMeasure q)) : - ((∑' x : T, (f x) * (q x).toReal)) ^ α ≤ (∑' x : T, (f x) ^ α * (q x).toReal) := by +def privPostProcess_AC {f : U -> V} (nq : Mechanism T U) (Hac : ACNeighbour nq) : ACNeighbour (privPostProcess nq f) := by + rw [ACNeighbour] at * + unfold AbsCts at * + intro l₁ l₂ Hn v + have Hac := Hac l₁ l₂ Hn + simp [privPostProcess] + intro Hppz i fi + apply Hac + apply Hppz + apply fi - conv => - left - left - right - intro x - rw [mul_comm] - rw [← smul_eq_mul] - conv => - right - right - intro x - rw [mul_comm] - rw [← smul_eq_mul] - rw [← PMF.integral_eq_tsum] - rw [← PMF.integral_eq_tsum] - - have A := @convexOn_rpow α (le_of_lt h) - have B : ContinuousOn (fun (x : ℝ) => x ^ α) (Set.Ici 0) := by - apply ContinuousOn.rpow - . exact continuousOn_id' (Set.Ici 0) - . exact continuousOn_const - . intro x h' - simp at h' - have OR : x = 0 ∨ 0 < x := by exact LE.le.eq_or_gt h' - cases OR - . rename_i h'' - subst h'' - right - apply lt_trans zero_lt_one h - . rename_i h'' - left - by_contra - rename_i h3 - subst h3 - simp at h'' - have C : @IsClosed ℝ UniformSpace.toTopologicalSpace (Set.Ici 0) := by - exact isClosed_Ici - have D := @ConvexOn.map_integral_le T ℝ t1 _ _ _ (PMF.toMeasure q) (Set.Ici 0) f (fun (x : ℝ) => x ^ α) (PMF.toMeasure.isProbabilityMeasure q) A B C - simp at D - apply D - . exact MeasureTheory.ae_of_all (PMF.toMeasure q) h2 - . apply MeasureTheory.Memℒp.integrable _ mem - rw [one_le_ofReal] - apply le_of_lt h - . rw [Function.comp_def] - have X : ENNReal.ofReal α ≠ 0 := by - simp - apply lt_trans zero_lt_one h - have Y : ENNReal.ofReal α ≠ ⊤ := by - simp - have Z := @Integrable_rpow T t1 f h2 (PMF.toMeasure q) (ENNReal.ofReal α) mem X Y - rw [toReal_ofReal] at Z - . exact Z - . apply le_of_lt - apply lt_trans zero_lt_one h - . have X : ENNReal.ofReal α ≠ 0 := by - simp - apply lt_trans zero_lt_one h - have Y : ENNReal.ofReal α ≠ ⊤ := by - simp - have Z := @Integrable_rpow T t1 f h2 (PMF.toMeasure q) (ENNReal.ofReal α) mem X Y - rw [toReal_ofReal] at Z - . exact Z - . apply le_of_lt - apply lt_trans zero_lt_one h - . apply MeasureTheory.Memℒp.integrable _ mem - rw [one_le_ofReal] - apply le_of_lt h - -def δ (nq : SLang U) (f : U → V) (a : V) : {n : U | a = f n} → ENNReal := fun x : {n : U | a = f n} => nq x * (∑' (x : {n | a = f n}), nq x)⁻¹ +/-- +Normalized fiber +-/ +def δ (nq : SLang U) (f : U → V) (a : V) : {n : U | a = f n} → ENNReal := + fun x : {n : U | a = f n} => nq x * (∑' (x : {n | a = f n}), nq x)⁻¹ lemma δ_normalizes (nq : SLang U) (f : U → V) (a : V) (h1 : ∑' (i : ↑{n | a = f n}), nq ↑i ≠ 0) (h2 : ∑' (i : ↑{n | a = f n}), nq ↑i ≠ ⊤) : HasSum (δ nq f a) 1 := by @@ -136,6 +55,9 @@ lemma δ_normalizes (nq : SLang U) (f : U → V) (a : V) (h1 : ∑' (i : ↑{n | rw [ENNReal.tsum_mul_right] rw [ENNReal.mul_inv_cancel h1 h2] +/-- +Normalized fiber distribution +-/ def δpmf (nq : SLang U) (f : U → V) (a : V) (h1 : ∑' (i : ↑{n | a = f n}), nq ↑i ≠ 0) (h2 : ∑' (i : ↑{n | a = f n}), nq ↑i ≠ ⊤) : PMF {n : U | a = f n} := ⟨ δ nq f a , δ_normalizes nq f a h1 h2 ⟩ @@ -167,10 +89,6 @@ theorem norm_simplify (x : ENNReal) (h : x ≠ ⊤) : simp rfl -theorem RD1 (p q : T → ENNReal) (α : ℝ) (h : 1 < α) (RD : ∑' (x : T), p x ^ α * q x ^ (1 - α) ≠ ⊤) (nz : ∀ x : T, q x ≠ 0) (nt : ∀ x : T, q x ≠ ⊤) : - ∑' (x : T), (p x / q x) ^ α * q x ≠ ⊤ := by - rw [← RenyiDivergenceExpectation p q h nz nt] - trivial theorem convergent_subset {p : T → ENNReal} (f : T → V) (conv : ∑' (x : T), p x ≠ ⊤) : ∑' (x : { y : T| x = f y }), p x ≠ ⊤ := by @@ -217,329 +135,307 @@ theorem tsum_pos_int {f : ℤ → ENNReal} (h1 : ∑' x : ℤ, f x ≠ ⊤) (h2 apply toReal_strict_mono h1 apply ENNReal.tsum_pos_int h1 h2 -theorem DPostPocess_pre {nq : List T → SLang U} {ε₁ ε₂ : ℕ+} (h : zCDPBound nq ((ε₁ : ℝ) / ε₂)) (nn : NonZeroNQ nq) (nt : NonTopRDNQ nq) (nts : NonTopNQ nq) (conv : NonTopSum nq) (f : U → V) {α : ℝ} (h1 : 1 < α) {l₁ l₂ : List T} (h2 : Neighbour l₁ l₂) : - (∑' (x : V), - (∑' (a : U), if x = f a then nq l₁ a else 0) ^ α * - (∑' (a : U), if x = f a then nq l₂ a else 0) ^ (1 - α)) ≤ - (∑' (x : U), nq l₁ x ^ α * nq l₂ x ^ (1 - α)) := by - simp [zCDPBound, RenyiDivergence] at h +lemma rpow_nonzero (x : ENNReal) (y : ℝ) (H : ¬(x = 0 ∧ 0 < y ∨ x = ⊤ ∧ y < 0)) : x ^ y ≠ 0 := by + intro Hk + apply H + apply (ENNReal.rpow_eq_zero_iff).mp + apply Hk + + +/-- +Jensen's inequality for privPostProcess, restructed to types where ``nq l₁`` is nonzero +-/ +theorem privPostPocess_DP_pre_reduct {U : Type} [m2 : MeasurableSpace U] [count : Countable U] [disc : DiscreteMeasurableSpace U] [Inhabited U] + {nq : List T → SLang U} + (f : U → V) {α : ℝ} (h1 : 1 < α) {l₁ l₂ : List T} + (HNorm1 : HasSum (nq l₁) 1) + (HNorm2 : HasSum (nq l₂) 1) + (Habs : AbsCts (nq l₁) (nq l₂)) + (Hnq2 : ∀ (u : U), nq l₁ u ≠ 0) + (h2 : Neighbour l₁ l₂) : + (∑' (x : V), (∑' (a : U), if x = f a then nq l₁ a else 0) ^ α * (∑' (a : U), if x = f a then nq l₂ a else 0) ^ (1 - α)) ≤ (∑' (x : U), nq l₁ x ^ α * nq l₂ x ^ (1 - α)) := by + + -- By absolute continuity, nq1 is nonzero + have Hnql1 : (∀ (u : U), nq l₂ u ≠ 0) := by + rw [AbsCts] at Habs + intro u HK + apply Hnq2 + apply Habs + apply HK + + -- Noised query is not ⊤ + have nq_nts1 : ∑' n : U, nq l₁ n ≠ ⊤ := by simp [HasSum.tsum_eq HNorm1] + have nq_nts2 : ∑' n : U, nq l₂ n ≠ ⊤ := by simp [HasSum.tsum_eq HNorm2] -- Rewrite as cascading expectations - rw [@RenyiDivergenceExpectation _ (nq l₁) (nq l₂) _ h1 (nn l₂) (nts l₂)] + rw [RenyiDivergenceExpectation] + case h => apply h1 + case H => + simp [AbsCts] + intro v Hv i vEq + apply Habs + apply Hv + apply vEq + simp + rw [RenyiDivergenceExpectation (fun x => nq l₁ x) (fun x => nq l₂ x) h1 Habs] -- Shuffle the sum rw [fiberwisation (fun x => (nq l₁ x / nq l₂ x) ^ α * nq l₂ x) f] - apply ENNReal.tsum_le_tsum - intro i + simp - -- Get rid of elements with probability 0 in the pushforward + -- Eliminate elements with probability zero split - . rename_i empty - rw [condition_to_subset] - have ZE : (∑' (x_1 : ↑{n | i = f n}), nq l₁ ↑x_1) = 0 := by - simp - intro a H - have I₁ : a ∈ {b | i = f b} := by - simp [H] - have I2 : {b | i = f b} ≠ ∅ := by - apply ne_of_mem_of_not_mem' I₁ - simp - contradiction - rw [ZE] - simp only [toReal_mul, zero_toReal, ge_iff_le] - - rw [ENNReal.zero_rpow_of_pos] - . simp - . apply lt_trans zero_lt_one h1 - - -- Part 2: apply Jensen's inequality - . rename_i NotEmpty - - have MasterRW : ∀ l : List T, ∑' (a : ↑{a | i = f a}), nq l ↑a ≠ ⊤ := by - intro l - apply convergent_subset - simp [NonTopSum] at conv - have conv := conv l - apply conv - - have MasterZero : ∀ l : List T, ∑' (a : ↑{a | i = f a}), nq l ↑a ≠ 0 := by - intro l - simp - have T := witness NotEmpty - cases T - rename_i z w - exists z - constructor - . trivial - . apply nn l - - have S2 : (∑' (a : ↑{n | i = f n}), nq l₁ ↑a / nq l₂ ↑a * (δpmf (nq l₂) f i (MasterZero l₂) (MasterRW l₂)) a) ^ α ≠ ⊤ := by - conv => - left - left - right - intro a - rw [← δpmf_conv] - rw [division_def] - rw [mul_assoc] - right - rw [← mul_assoc] - rw [ENNReal.inv_mul_cancel (nn l₂ a) (nts l₂ a)] - rw [one_mul] - rw [ENNReal.tsum_mul_right] - apply ENNReal.rpow_ne_top_of_nonneg (le_of_lt (lt_trans zero_lt_one h1 )) - apply mul_ne_top - . apply convergent_subset _ (conv l₁) - . apply inv_ne_top.mpr (MasterZero l₂) - - have S1 : ∀ (a : ↑{n | i = f n}), nq l₁ ↑a / nq l₂ ↑a * (δpmf (nq l₂) f i (MasterZero l₂) (MasterRW l₂)) a ≠ ⊤ := by - intro a - apply mul_ne_top - . rw [division_def] - apply mul_ne_top (nts l₁ a) - apply inv_ne_top.mpr (nn l₂ a) - . rw [← δpmf_conv] - apply mul_ne_top (nts l₂ a) - apply inv_ne_top.mpr (MasterZero l₂) - - have S3 : ∑' (a : ↑{n | i = f n}), (nq l₁ ↑a / nq l₂ ↑a) ^ α * (δpmf (nq l₂) f i (MasterZero l₂) (MasterRW l₂)) a ≠ ⊤ := by - conv => - left - right - intro a - rw [← δpmf_conv] - rw [← mul_assoc] - rw [ENNReal.tsum_mul_right] - apply mul_ne_top - . rw [← RenyiDivergenceExpectation _ _ h1] - . replace nt := nt α h1 l₁ l₂ h2 - apply convergent_subset _ nt - . intro x - apply nn - . intro x - apply nts - . apply inv_ne_top.mpr (MasterZero l₂) - - have S4 : ∀ (a : ↑{n | i = f n}), (nq l₁ ↑a / nq l₂ ↑a) ^ α * (δpmf (nq l₂) f i (MasterZero l₂) (MasterRW l₂)) a ≠ ⊤ := by - intro a - apply ENNReal.ne_top_of_tsum_ne_top S3 - - rw [condition_to_subset] - rw [condition_to_subset] - - -- Introduce Q(f⁻¹ i) - let κ := ∑' x : {n : U | i = f n}, nq l₂ x - have P4 : κ / κ = 1 := by - rw [division_def] - rw [ENNReal.mul_inv_cancel] - . simp [κ] -- Use here for δ normalization - have T := witness NotEmpty - cases T - rename_i z w - exists z - constructor - . trivial - . apply nn l₂ - . simp only [κ] - apply MasterRW l₂ - - conv => - right - right - intro a - rw [← mul_one ((nq l₁ ↑a / nq l₂ ↑a) ^ α * nq l₂ ↑a)] - right - rw [← P4] - clear P4 - simp only [κ] - - conv => - right - right - intro a - right - rw [division_def] - rw [mul_comm] - - conv => - right - right - intro a - rw [← mul_assoc] - - rw [ENNReal.tsum_mul_right] - - -- Jensen's inequality - - have P5 : ∀ (x : ↑{n | i = f n}), 0 ≤ (fun a => (nq l₁ ↑a / nq l₂ ↑a).toReal) x := by - intro x - simp only [toReal_nonneg] - - have XXX : @Memℒp ℝ Real.normedAddCommGroup (↑{n | i = f n}) Subtype.instMeasurableSpace (fun a => (nq l₁ ↑a / nq l₂ ↑a).toReal) - (ENNReal.ofReal α) (PMF.toMeasure (δpmf (nq l₂) f i (MasterZero l₂) (MasterRW l₂))) := by - simp [Memℒp] - constructor - . apply MeasureTheory.StronglyMeasurable.aestronglyMeasurable - apply Measurable.stronglyMeasurable - apply Measurable.ennreal_toReal - conv => - right - intro x - rw [division_def] - apply Measurable.mul - . -- MeasurableSingletonClass.toDiscreteMeasurableSpace - apply measurable_discrete - . apply Measurable.inv - apply measurable_discrete - . simp [snorm] - split - . simp - . simp [snorm'] - rw [MeasureTheory.lintegral_countable'] -- Uses countable - rw [toReal_ofReal (le_of_lt (lt_trans zero_lt_one h1))] - have OTHER : ∀ a, nq l₁ a / nq l₂ a ≠ ⊤ := by - intro a - rw [division_def] - rw [ne_iff_lt_or_gt] - left - rw [mul_lt_top_iff] - left - constructor - . exact Ne.lt_top' (id (Ne.symm (nts l₁ a))) - . simp - exact pos_iff_ne_zero.mpr (nn l₂ a) - - conv => - left - left - right - intro a - rw [norm_simplify _ (OTHER a)] - have Z : 0 < α⁻¹ := by - simp - apply lt_trans zero_lt_one h1 - rw [rpow_lt_top_iff_of_pos Z] - conv => - left - right - intro a - rw [PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton a)] - - apply Ne.lt_top' (id (Ne.symm _)) - apply S3 - - - have Jensen's := @Renyi_Jensen {n : U | i = f n} Subtype.instMeasurableSpace Subtype.instMeasurableSingletonClass (fun a => (nq l₁ a / nq l₂ a).toReal) (δpmf (nq l₂) f i (MasterZero l₂) (MasterRW l₂)) α h1 P5 XXX - clear P5 - - have P6 : 0 ≤ (∑' (x : ↑{n | i = f n}), nq l₂ ↑x).toReal := by - simp only [toReal_nonneg] - have A' := mul_le_mul_of_nonneg_left Jensen's P6 - clear Jensen's P6 - - conv => - right - rw [mul_comm] - right - right - intro a - rw [mul_assoc] - rw [δpmf_conv] + case h.inl => + rename_i H + repeat rw [condition_to_subset] + rw [H] + simp - -- Here + -- Normalize each fiber into a PMF + rename_i NotEmpty + repeat rw [condition_to_subset] - replace A' := ofReal_le_ofReal A' - rw [ofReal_mul toReal_nonneg] at A' - rw [ofReal_mul toReal_nonneg] at A' - rw [ofReal_toReal_eq_iff.2 (MasterRW l₂)] at A' - simp only at A' + have nq_restriction_nts1 : ∑' (a : ↑{a | i = f a}), nq l₁ ↑a ≠ ⊤ := by exact convergent_subset (fun y => f y) nq_nts1 + have nq_restriction_nts2 : ∑' (a : ↑{a | i = f a}), nq l₂ ↑a ≠ ⊤ := by exact convergent_subset (fun y => f y) nq_nts2 - revert A' - conv => - left - right - right - right - right - intro x - rw [toReal_rpow] - rw [← toReal_mul] - conv => + have nq_restriction_nzs (l' : List T) (Hl : ∀ u : U, nq l' u ≠ 0) : ∑' (a : ↑{a | i = f a}), nq l' ↑a ≠ 0 := by + simp + have T := witness NotEmpty + cases T + rename_i z w + exists z + constructor + . trivial + . exact Hl z + simp + + let δF₁ := (δpmf (nq l₁) f i (nq_restriction_nzs l₁ Hnq2) nq_restriction_nts1) + let δF₂ := (δpmf (nq l₂) f i (nq_restriction_nzs l₂ Hnql1) nq_restriction_nts2) + have δF₁_Eq : δF₁ = (δpmf (nq l₁) f i (nq_restriction_nzs l₁ Hnq2) nq_restriction_nts1) := by exact rfl + have δF₂_Eq : δF₂ = (δpmf (nq l₂) f i (nq_restriction_nzs l₂ Hnql1) nq_restriction_nts2) := by exact rfl + + -- Normalized fibers are absolutely continuous + have HAC_Fiber : AbsCts δF₁ δF₂ := by + simp [AbsCts] + rw [δF₁_Eq] + rw [δF₂_Eq] + intro a b + repeat rw [δpmf] + unfold δ + simp + rw [DFunLike.coe] + simp [PMF.instFunLike] + intro H + cases H + · rename_i Hl2z left - right - right - right - rw [← ENNReal.tsum_toReal_eq S4] - intro A' - rw [ofReal_toReal_eq_iff.2 S3] at A' - - apply le_trans _ A' - clear A' - apply le_of_eq + apply Habs + apply Hl2z + · exfalso + apply nq_restriction_nts2 + simp + assumption - -- Part 3: + have δF₂_NT (x : { x // i = f x }) : δF₂ x ≠ ⊤ := by + rw [δF₂_Eq] + exact PMF.apply_ne_top ((nq l₂).δpmf f i (nq_restriction_nzs l₂ Hnql1) (nq_restriction_nts2)) x + -- Normalized fibers avoid the bad case for rewriting the Jensen term + have Hspecial (x : { x // i = f x }) : ¬(δF₁ x ≠ 0 ∧ δF₂ x = ⊤) := by + simp + intro _ Hcont + exfalso + apply δF₂_NT + apply Hcont + + -- Apply Jensen's inequality to the normalized fibers + have HJ := Renyi_Jensen_ENNReal δF₁ δF₂ h1 HAC_Fiber + + -- Cancel and simplify the LHS of HJ to 1 + conv at HJ => + lhs + arg 1 + arg 1 + intro x + rw [division_def] + rw [mul_mul_inv_eq_mul_cancel (HAC_Fiber x) (Hspecial x)] + conv at HJ => + lhs + arg 1 + rw [PMF.tsum_coe] + simp at HJ + + -- Name the normalization constants for each fiber + let N (l : List T) := (∑' (x : {n // i = f n}), nq l x)⁻¹ + have N_def (l : List T) : N l = (∑' (x : {n // i = f n}), nq l x)⁻¹ := by exact rfl + have N_inv (l : List T) : (∑' (x : {n // i = f n}), nq l x) = (N l)⁻¹ := by + exact Eq.symm (inv_inv (∑' (x : { n // i = f n }), (nq l) ↑x)) + have N1_nz : N l₁ ≠ 0 := ENNReal.inv_ne_zero.mpr (nq_restriction_nts1) + have N2_nz : N l₂ ≠ 0 := ENNReal.inv_ne_zero.mpr (nq_restriction_nts2) + + -- Unfold normalization constants in HJ + conv at HJ => + rhs + arg 1 + intro x + repeat rw [DFunLike.coe] + repeat rw [PMF.instFunLike] + simp + rw [δF₁_Eq] + rw [δF₂_Eq] + simp [δpmf] + unfold δ + repeat rw [DFunLike.coe] + repeat rw [PMF.instFunLike] + simp + rw [<- N_def] + rw [<- N_def] + + -- Fold constants in goal + rw [N_inv] + rw [N_inv] + + -- Pull out constants from the sum in HJ + have conv1 (x : { x // i = f x }) : (nq l₁ x.val * N l₁ / (nq l₂ x.val * N l₂)) ^ α = (N l₁ / N l₂) ^ α * (nq l₁ x.val / nq l₂ x.val) ^ α := by + simp [division_def] + rw [ENNReal.mul_rpow_of_ne_top ?G1 ?G2] + case G1 => + apply mul_ne_top + · exact ENNReal.ne_top_of_tsum_ne_top (nq_nts1) ↑x + · exact inv_ne_top.mpr (nq_restriction_nzs l₁ Hnq2) + case G2 => + apply inv_ne_top.mpr + exact mul_ne_zero (Hnql1 ↑x) N2_nz + rw [ENNReal.mul_rpow_of_ne_top ?G1 ?G2] + case G1 => + exact ENNReal.ne_top_of_tsum_ne_top (nq_nts1) ↑x + case G2 => + exact inv_ne_top.mpr (nq_restriction_nzs l₁ Hnq2) + rw [ENNReal.mul_rpow_of_ne_top ?G1 ?G2] + case G1 => + exact inv_ne_top.mpr (nq_restriction_nzs l₁ Hnq2) + case G2 => + exact inv_ne_top.mpr N2_nz + rw [ENNReal.mul_rpow_of_ne_top ?G1 ?G2] + case G1 => + exact ENNReal.ne_top_of_tsum_ne_top (nq_nts1) ↑x + case G2 => + exact inv_ne_top.mpr (Hnql1 ↑x) conv => - right - right - right - left - right - intro x - rw [← toReal_mul] - rw [← ENNReal.tsum_toReal_eq S1] - rw [toReal_rpow] - rw [ofReal_toReal_eq_iff.2 S2] - + arg 1 + rw [mul_assoc] + rw [mul_comm] + skip + repeat rw [mul_assoc] + congr 1 conv => + arg 2 + arg 2 + rw [mul_comm] + rw [<- mul_assoc] + congr 1 + rw [ENNReal.mul_inv ?G1 ?G2] + case G1 => right + exact inv_ne_top.mpr (nq_restriction_nzs l₂ Hnql1) + case G2 => right - left - right - intro x - rw [division_def] - rw [← δpmf_conv] - rw [mul_assoc] - right - rw [← mul_assoc] - left - rw [ENNReal.inv_mul_cancel (nn l₂ x) (nts l₂ x)] - simp only [one_mul] - - rw [ENNReal.tsum_mul_right] - have H4 : (∑' (a : ↑{a | i = f a}), nq l₂ ↑a)⁻¹ ≠ ⊤ := by - apply inv_ne_top.mpr - simp - have T := witness NotEmpty - cases T - rename_i z w - exists z - constructor - . trivial - . apply nn l₂ - rw [ENNReal.mul_rpow_of_ne_top (MasterRW l₁) H4] + exact N2_nz + rw [ENNReal.mul_rpow_of_ne_top ?G1 ?G2] + case G1 => exact inv_ne_top.mpr (Hnql1 ↑x) + case G2 => exact inv_ne_top.mpr N2_nz + rw [mul_comm] + conv at HJ => + rhs + arg 1 + intro x + rw [conv1 x] + rw [mul_assoc] + arg 2 + rw [mul_comm] + rw [mul_assoc] + rw [mul_comm] + rw [mul_assoc] + clear conv1 + rw [ENNReal.tsum_mul_left] at HJ + rw [ENNReal.tsum_mul_left] at HJ + rw [<- mul_assoc] at HJ + + -- Move constants to the left-hand side of HJ + -- Super haunted bug: When I apply this as normal to HJ (with placeholders) + -- Lean it lights up all of my "have" and "let" statements because it \"doesn't + -- know how to synthesize\" a placeholder. The placeholder it points me to is in + -- Pure/Postprocessing, where the same lemma is also applied with placeholders. + have W := + @ENNReal.div_le_iff_le_mul + 1 + ((N l₁ / N l₂) ^ α * N l₂) + (∑' (i_1 : { x // i = f x }), (nq l₁ i_1.val / nq l₂ i_1.val) ^ α * nq l₂ i_1.val) + ?G1 + ?G2 + case G1 => + left + apply mul_ne_zero_iff.mpr + apply And.intro + · apply (rpow_nonzero (N l₁ / N l₂) α) + intro Hk + rcases Hk with ⟨ H1 , _ ⟩ | ⟨ _ , H2 ⟩ + · have Hk' : 0 < N l₁ / N l₂ := by + apply ENNReal.div_pos_iff.mpr + apply And.intro + · exact N1_nz + · exact inv_ne_top.mpr (nq_restriction_nzs l₂ Hnql1) + rw [H1] at Hk' + simp at Hk' + · linarith + · apply N2_nz + case G2 => + left + apply mul_ne_top + · apply rpow_ne_top_of_nonneg + · linarith + · intro Hk + have Hk' : (N l₁ / N l₂ < ⊤) := by + apply ENNReal.div_lt_top + · exact inv_ne_top.mpr (nq_restriction_nzs l₁ Hnq2) + · exact N2_nz + rw [Hk] at Hk' + simp at Hk' + · exact inv_ne_top.mpr (nq_restriction_nzs l₂ Hnql1) + rw [mul_comm] at HJ + apply W.mpr at HJ + clear W + + -- Apply transitivity + apply (le_trans ?G3 HJ) + clear HJ + + -- These terms are equal + apply Eq.le + repeat rw [division_def] + simp + rw [ENNReal.mul_inv ?G1 ?G2] + case G1 => + right + exact inv_ne_top.mpr (nq_restriction_nzs l₂ Hnql1) + case G2 => + right + exact N2_nz + congr + rw [<- ENNReal.inv_rpow] + congr + rw [ENNReal.mul_inv ?G1 ?G2] + case G1 => + left + exact N1_nz + case G2 => + left + exact inv_ne_top.mpr (nq_restriction_nzs l₁ Hnq2) + simp - have H3 : ∑' (a : ↑{a | i = f a}), nq l₂ ↑a ≠ 0 := by - simp - have T := witness NotEmpty - cases T - rename_i z w - exists z - constructor - . trivial - . apply nn l₂ - rw [ENNReal.rpow_sub _ _ H3 (MasterRW l₂)] - rw [ENNReal.rpow_one] - rw [division_def] - rw [← mul_assoc] - rw [← mul_assoc] - congr 1 - . rw [mul_comm] - . congr 1 - rw [ENNReal.inv_rpow] theorem tsum_ne_zero_of_ne_zero {T : Type} [Inhabited T] (f : T → ENNReal) (h : ∀ x : T, f x ≠ 0) : ∑' x : T, f x ≠ 0 := by @@ -549,121 +445,172 @@ theorem tsum_ne_zero_of_ne_zero {T : Type} [Inhabited T] (f : T → ENNReal) (h have B := CONTRA default contradiction -theorem privPostProcess_zCDPBound {nq : List T → SLang U} {ε₁ ε₂ : ℕ+} (h : zCDPBound nq ((ε₁ : ℝ) / ε₂)) (nn : NonZeroNQ nq) (nt : NonTopRDNQ nq) (nts : NonTopNQ nq) (conv : NonTopSum nq) (f : U → V) : +/-- +Jensen's inequality for privPostProcess. + +Implementation note: This reduction only works because neighbours are symmetric. A different reduction may +be able to relax this requirement. +-/ +theorem privPostPocess_DP_pre {nq : List T → PMF U} (HNorm : ∀ l, HasSum (nq l) 1) + (f : U → V) {α : ℝ} (h1 : 1 < α) {l₁ l₂ : List T} (HN : Neighbour l₁ l₂) + (Habs : AbsCts (nq l₁) (nq l₂)) (Habs' : AbsCts (nq l₂) (nq l₁)) : + (∑' (x : V), + (∑' (a : U), if x = f a then nq l₁ a else 0) ^ α * + (∑' (a : U), if x = f a then nq l₂ a else 0) ^ (1 - α)) ≤ + (∑' (x : U), nq l₁ x ^ α * nq l₂ x ^ (1 - α)) := by + -- Restruct the sum to a type where nq l₁ is nonzero + have HSup1 (x : V) : Function.support (fun (a : U) => if x = f a then nq l₁ a else 0) ⊆ { u : U | nq l₁ u ≠ 0 } := by simp [Function.support] + have HSup2 (x : V) : Function.support (fun (a : U) => if x = f a then nq l₂ a else 0) ⊆ { u : U | nq l₁ u ≠ 0 } := by + simp [Function.support] + exact fun a _ a_2 a_3 => a_2 (Habs' a a_3) + have HSup3 : Function.support (fun (a : U) => nq l₁ a ^ α * nq l₂ a ^ (1 - α)) ⊆ { u : U | nq l₁ u ≠ 0 } := by + simp only [Function.support, Set.setOf_subset_setOf] + intro a Hnz + apply mul_ne_zero_iff.mp at Hnz + rcases Hnz with ⟨ H1 , _ ⟩ + intro Hk + apply H1 + apply (ENNReal.rpow_eq_zero_iff).mpr + left + apply And.intro + · apply Hk + · linarith + rw [<- tsum_subtype_eq_of_support_subset HSup3] + conv => + lhs + arg 1 + intro v + rw [<- tsum_subtype_eq_of_support_subset (HSup1 v)] + rw [<- tsum_subtype_eq_of_support_subset (HSup2 v)] + clear HSup1 + clear HSup2 + clear HSup3 + simp + + cases (Classical.em (∃ x : U, ¬ nq l₁ x = 0)) + · rename_i x_witness + have HR := @privPostPocess_DP_pre_reduct T V {x // ¬ nq l₁ x = 0} + _ _ _ ?TC + (fun t u => nq t u) (fun x => f x) α h1 + l₁ l₂ ?GNorm1 ?GNorm2 ?Gac ?Gnz HN + case TC => + apply inhabited_of_nonempty + exact Set.Nonempty.to_subtype x_witness + case GNorm1 => + simp + rw [<- HasSum.tsum_eq (HNorm l₁)] + have HSup4 : Function.support (fun u => nq l₁ u) ⊆ { u | nq l₁ u ≠ 0 } := by simp [Function.support] + rw [<- tsum_subtype_eq_of_support_subset HSup4] + simp + apply Summable.hasSum + exact ENNReal.summable + case GNorm2 => + simp + rw [<- HasSum.tsum_eq (HNorm l₂)] + have HSup4 : Function.support (fun u => nq l₂ u) ⊆ { u | nq l₁ u ≠ 0 } := by + simp [Function.support] + intro a Hk1 Hk2 + apply Hk1 + apply Habs' + apply Hk2 + rw [<- tsum_subtype_eq_of_support_subset HSup4] + simp + apply Summable.hasSum + exact ENNReal.summable + case Gac => + rw [AbsCts] + simp + intro a _ H2 + exact Habs a (Habs' a (Habs a H2)) + case Gnz => simp + simp at HR + apply HR + · rename_i x_empty + simp at * + have Hempty : IsEmpty {x // ¬nq l₁ x = 0} := by + exact Subtype.isEmpty_of_false fun a a_1 => a_1 (x_empty a) + rw [@tsum_empty _ _ _ _ _ Hempty] + conv => + lhs + arg 1 + intro + rw [@tsum_empty _ _ _ _ _ Hempty] + rw [@tsum_empty _ _ _ _ _ Hempty] + simp + intro + left + linarith + +/-- +privPostProcess satisfies the zCDP bound +-/ +theorem privPostProcess_zCDPBound {nq : Mechanism T U} {ε₁ ε₂ : ℕ+} + (h : zCDPBound nq ((ε₁ : ℝ) / ε₂)) (f : U → V) (Hac : ACNeighbour nq) : zCDPBound (privPostProcess nq f) ((ε₁ : ℝ) / ε₂) := by simp [privPostProcess, zCDPBound, RenyiDivergence] intro α h1 l₁ l₂ h2 have h' := h simp [zCDPBound, RenyiDivergence] at h' replace h' := h' α h1 l₁ l₂ h2 - - -- Part 1, removing fluff - apply le_trans _ h' clear h' - - -- remove the α scaling - have A : 0 ≤ (α - 1)⁻¹ := by + unfold RenyiDivergence_def + rw [DFunLike.coe] + rw [PMF.instFunLike] + simp + conv => + enter [1, 1, 2, 1, 1, x] + repeat rw [SLang.toPMF] simp - apply le_of_lt h1 - apply mul_le_mul_of_nonneg_left _ A - clear A - - have RDConvegence : ∑' (x : U), nq l₁ x ^ α * nq l₂ x ^ (1 - α) ≠ ⊤ := by - simp [NonTopRDNQ] at nt - have nt := nt α h1 l₁ l₂ h2 - trivial - - have B := DPostPocess_pre h nn nt nts conv f h1 h2 - have B' : ∑' (x : V), (∑' (a : U), if x = f a then nq l₁ a else 0) ^ α * (∑' (a : U), if x = f a then nq l₂ a else 0) ^ (1 - α) ≠ ⊤ := by - by_contra CONTRA - rw [CONTRA] at B - simp at B - contradiction - - -- remove the log - apply log_le_log _ (toReal_mono RDConvegence B) - apply toReal_pos _ B' - apply (tsum_ne_zero_iff ENNReal.summable).mpr - exists (f default) - - rw [ENNReal.tsum_eq_add_tsum_ite default] conv => - left - right - rw [ENNReal.tsum_eq_add_tsum_ite default] - simp only [reduceIte] - apply mul_ne_zero - . by_contra CONTRA - rw [ENNReal.rpow_eq_zero_iff_of_pos (lt_trans zero_lt_one h1)] at CONTRA - simp at CONTRA - cases CONTRA - rename_i left right - have Y := nn l₁ default - contradiction - . by_contra CONTRA - rw [ENNReal.rpow_eq_zero_iff] at CONTRA - cases CONTRA - . rename_i CONTRA - cases CONTRA - rename_i left right - simp at left - cases left - rename_i le1 le2 - have Y := nn l₂ default - contradiction - . rename_i CONTRA - cases CONTRA - rename_i left right - simp at left - cases left - . rename_i left - have Y := nts l₂ default - contradiction - . rename_i left - have Rem := conv l₂ - have X : (∑' (x : U), if x = default then 0 else if f default = f x then nq l₂ x else 0) ≤ ∑' (n : U), nq l₂ n := by - apply ENNReal.tsum_le_tsum - intro a - split - . simp - . split - . simp - . simp - replace Rem := Ne.symm Rem - have Y := Ne.lt_top' Rem - have Z : (∑' (x : U), if x = default then 0 else if f default = f x then nq l₂ x else 0) < ⊤ := by - apply lt_of_le_of_lt X Y - rw [lt_top_iff_ne_top] at Z - contradiction - -theorem privPostProcess_NonTopRDNQ {nq : List T → SLang U} {ε₁ ε₂ : ℕ+} (f : U → V) (dp :zCDPBound nq ((ε₁ : ℝ) / ε₂)) (nt : NonTopRDNQ nq) (nz : NonZeroNQ nq) (nts : NonTopNQ nq) (ntsum: NonTopSum nq) : - NonTopRDNQ (privPostProcess nq f) := by - simp [NonTopRDNQ, NonTopSum, privPostProcess] at * - intros α h1 l₁ l₂ h2 - have ntrdnq := nt - replace nt := nt α h1 l₁ l₂ h2 - have A := @DPostPocess_pre T U V _ _ _ nq ε₁ ε₂ dp nz ntrdnq nts ntsum f α h1 l₁ l₂ h2 - apply @LT.lt.ne_top _ _ _ _ ⊤ - rw [Eq.comm] at nt - have B := Ne.lt_top' nt - exact lt_of_le_of_lt A B + enter [2, 1, 2, 1, 1, x] + repeat rw [SLang.toPMF] + repeat rw [DFunLike.coe] + repeat rw [PMF.instFunLike] + simp + apply ofEReal_le_mono + apply mul_le_mul_of_nonneg_left ?G1 ?G2 + case G2 => + apply EReal.coe_nonneg.mpr + apply inv_nonneg_of_nonneg + linarith + apply elog_mono_le.mp + simp [PMF.bind, PMF.pure] + simp [PMF.instFunLike] + apply privPostPocess_DP_pre + · exact fun l => PMF.hasSum_coe_one (nq l) + · exact h1 + · exact h2 + · exact Hac l₁ l₂ h2 + · apply Hac l₂ l₁ + exact Neighbour_symm l₁ l₂ h2 + + +-- theorem privPostProcess_NonTopRDNQ {nq : List T → SLang U} {HNorm : ∀ l, HasSum (nq l) 1} {ε₁ ε₂ : ℕ+} (f : U → V) +-- (dp : zCDPBound nq HNorm ((ε₁ : ℝ) / ε₂)) (nt : NonTopRDNQ nq) (nz : NonZeroNQ nq) (nts : NonTopNQ nq) (ntsum: NonTopSum nq) : +-- NonTopRDNQ (privPostProcess nq f) := by +-- simp [NonTopRDNQ, NonTopSum, privPostProcess] at * +-- intros α h1 l₁ l₂ h2 +-- have ntrdnq := nt +-- replace nt := nt α h1 l₁ l₂ h2 +-- sorry +-- -- have A := @DPostPocess_pre T U V _ _ _ nq ε₁ ε₂ dp nz ntrdnq nts ntsum f α h1 l₁ l₂ h2 +-- -- apply @LT.lt.ne_top _ _ _ _ ⊤ +-- -- rw [Eq.comm] at nt +-- -- have B := Ne.lt_top' nt +-- -- exact lt_of_le_of_lt A B + /-- Postprocessing preserves zCDP -/ -theorem privPostProcess_zCDP {f : U → V} (sur : Function.Surjective f) (nq : List T → SLang U) (ε₁ ε₂ : ℕ+) (h : zCDP nq ((ε₁ : ℝ) / ε₂)) : +theorem privPostProcess_zCDP {f : U → V} + (nq : Mechanism T U) (ε₁ ε₂ : ℕ+) (h : zCDP nq ((ε₁ : ℝ) / ε₂)) : zCDP (privPostProcess nq f) (((ε₁ : ℝ) / ε₂)) := by + rcases h with ⟨ Hac1, Hb1 ⟩ simp [zCDP] at * - cases h ; rename_i h1 h2 ; cases h2 ; rename_i h2 h3 ; cases h3 ; rename_i h3 h4 ; cases h4 ; rename_i h4 h5 - repeat any_goals constructor - . apply privPostProcess_zCDPBound h1 h2 h5 h4 h3 - . apply privPostProcess_NonZeroNQ h2 sur - . apply privPostProcess_NonTopSum f h3 - . simp [NonTopNQ] - intro l - apply ENNReal.ne_top_of_tsum_ne_top - apply privPostProcess_NonTopSum f h3 - . apply privPostProcess_NonTopRDNQ f h1 h5 h2 h4 h3 + apply And.intro + · exact privPostProcess_AC nq Hac1 + · exact (privPostProcess_zCDPBound Hb1 f Hac1) end SLang diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean index a7bbbe8b..27a5e77c 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/System.lean @@ -7,6 +7,7 @@ import SampCert.DifferentialPrivacy.Abstract import SampCert.DifferentialPrivacy.ZeroConcentrated.DP import SampCert.DifferentialPrivacy.ZeroConcentrated.Mechanism.Basic import SampCert.DifferentialPrivacy.ZeroConcentrated.Composition +import SampCert.DifferentialPrivacy.ZeroConcentrated.AdaptiveComposition import SampCert.DifferentialPrivacy.ZeroConcentrated.Postprocessing /-! @@ -27,6 +28,14 @@ noncomputable instance gaussian_zCDPSystem : DPSystem T where noise := privNoisedQuery noise_prop := privNoisedQuery_zCDP compose_prop := privCompose_zCDP - postprocess_prop := privPostProcess_zCDP +-- adaptive_unif_prop := fun {Z U} nq2 => +-- ((∃ (z : ℝ), ∀ (u : U), ∀ l, ∑'(v : Z), nq2 u l v ≤ ENNReal.ofReal z) ∧ +-- (URDBound nq2 (fun α l₁ l₂ => ⨆ u, RenyiDivergence (nq2 u l₁) (nq2 u l₂) α))) +-- adaptive_compose_prop := by +-- intros +-- apply privComposeAdaptive_zCDP <;> aesop +-- postprocess_prop := privPostProcess_zCDP + postprocess_prop_f _ := True + postprocess_prop _ := privPostProcess_zCDP end SLang diff --git a/SampCert/Samplers/GaussianGen/Properties.lean b/SampCert/Samplers/GaussianGen/Properties.lean index 230c88d9..9db662f5 100644 --- a/SampCert/Samplers/GaussianGen/Properties.lean +++ b/SampCert/Samplers/GaussianGen/Properties.lean @@ -53,4 +53,34 @@ theorem DiscreteGaussianGenSample_apply (num : PNat) (den : PNat) (μ x : ℤ) : . simp [gauss_term_ℝ] . rw [shifted_gauss_sum_0 A] +/-- +DiscreteGaussianGen has sum 1 +-/ +theorem DiscreteGaussianGen_sum (num : PNat) (den : PNat) (μ : ℤ) : HasSum (DiscreteGaussianGenSample num den μ) 1 := by + rw [Summable.hasSum_iff ENNReal.summable] + conv => + lhs + arg 1 + intro b + rw [DiscreteGaussianGenSample_apply] + + have Hnz : (num / den : ℝ) ≠ 0 := by simp + have Hcoe : (OfNat.ofNat 1 = ENNReal.ofReal (OfNat.ofNat 1)) := by simp + rw [Hcoe] + rw [<- (discrete_gaussian_normalizes Hnz μ)] + symm + apply (ENNReal.ofReal_tsum_of_nonneg ?hf_nonneg ?hf) + · exact fun n => discrete_gaussian_nonneg Hnz (↑μ) n + · apply discrete_gaussian_summable' + apply Hnz + +/-- +DiscreteGaussianGen as a PMF +-/ +def DiscreteGaussianGenPMF (num : PNat) (den : PNat) (μ : ℤ) : PMF ℤ := + ⟨ DiscreteGaussianGenSample num den μ , DiscreteGaussianGen_sum num den μ ⟩ + + + + end SLang diff --git a/SampCert/Samplers/LaplaceGen/Properties.lean b/SampCert/Samplers/LaplaceGen/Properties.lean index 3870123b..b63dda5d 100644 --- a/SampCert/Samplers/LaplaceGen/Properties.lean +++ b/SampCert/Samplers/LaplaceGen/Properties.lean @@ -29,103 +29,32 @@ theorem DiscreteLaplaceGenSample_periodic (num : PNat) (den : PNat) (μ x : ℤ) rw [tsum_eq_single (x - μ) (by aesop)] simp --- theorem DiscreteLaplaceSampleGen_normalizes (num den : PNat) (μ : ℤ) : --- ∑' x : ℤ, (DiscreteLaplaceGenSample num den μ) x = 1 := by --- conv => --- left --- right --- intro x --- rw [DiscreteLaplaceGenSample_periodic] --- rw [Int.sub_eq_add_neg] --- have X : ∀ (μ : ℤ), Summable fun x => (DiscreteLaplaceSample num den (x + μ)).toReal := by --- intro μ --- simp --- conv => --- right --- intro x --- rw [ENNReal.ofReal_mul sorrrrry] --- apply Summable.mul_left --- sorrrryyyy - --- have A : (∑' (x : ℤ), DiscreteLaplaceSample num den (x + -μ)).toReal = (1 : ENNReal).toReal := by --- rw [ENNReal.tsum_toReal_eq] --- . - --- have B := @tsum_shift (fun a : ℤ => (DiscreteLaplaceSample num den a).toReal) (- μ) X --- simp only at B --- rw [B] --- rw [← ENNReal.tsum_toReal_eq] --- . rw [DiscreteLaplaceSample_normalizes] --- . sorrrryyyy -- OK --- . sorrrryyyy -- OK - --- exact (ENNReal.toReal_eq_one_iff (∑' (x : ℤ), DiscreteLaplaceSample num den (x + -μ))).mp A - - - --- -- simp only [DiscreteLaplaceGenSample, Bind.bind, Pure.pure, bind_apply, pure_apply, mul_ite, --- -- mul_one, mul_zero] --- -- conv => --- -- left --- -- right --- -- intro x --- -- rw [tsum_eq_single (x - μ) (by aesop)] --- -- simp only [sub_add_cancel, ↓reduceIte] - --- -- simp only [DiscreteLaplaceSample, Bind.bind, Pure.pure, SLang.bind_apply] --- -- have A := DiscreteLaplaceSampleLoop_normalizes num den --- -- conv => --- -- left --- -- right --- -- intro x --- -- right --- -- intro a --- -- rw [prob_until_apply_norm _ _ _ A] --- -- simp only [ENNReal.tsum_prod'] - --- -- rw [ENNReal.tsum_comm] --- -- conv => --- -- left --- -- right --- -- intro b --- -- rw [ENNReal.tsum_comm] --- -- right --- -- intro c --- -- rw [ENNReal.tsum_mul_left] --- -- right --- -- simp - --- -- conv => --- -- left --- -- right --- -- intro b --- -- right --- -- intro x --- -- left --- -- rw [mul_comm] --- -- conv => --- -- left --- -- right --- -- intro b --- -- right --- -- intro x --- -- rw [mul_assoc] --- -- conv => --- -- left --- -- right --- -- intro b --- -- rw [ENNReal.tsum_mul_left] --- -- conv => --- -- left --- -- rw [ENNReal.tsum_mul_left] - --- -- simp only [not_and, decide_implies, decide_not, dite_eq_ite, Bool.if_true_right, --- -- Bool.decide_eq_true, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not, tsum_bool, --- -- true_or, ↓reduceIte, Bool.true_eq_false, false_or, ite_not, ite_mul, zero_mul, --- -- Bool.false_eq_true] - --- -- sorrrryyyy - +/-- +Discrete Laplace has sum 1 +-/ +theorem DiscreteLaplaceGenSample_sum (num : PNat) (den : PNat) (μ : ℤ) : HasSum (DiscreteLaplaceGenSample num den μ) 1 := by + rw [Summable.hasSum_iff ENNReal.summable] + conv => + enter [1, 1, b] + rw [DiscreteLaplaceGenSample_periodic] + rw [<- DiscreteLaplaceSample_normalizes num den] + apply tsum_eq_tsum_of_ne_zero_bij ?Bij + case Bij => exact (fun w => w + μ) + · intro _ _ H + simp at H + exact SetCoe.ext H + · simp + intro z HZ + exists (z - μ) + simp + apply HZ + · simp + +/-- +Discrete Laplace as a PMF +-/ +def DiscreteLaplaceGenSamplePMF (num : PNat) (den : PNat) (μ : ℤ) : PMF ℤ := + ⟨ DiscreteLaplaceGenSample num den μ , DiscreteLaplaceGenSample_sum num den μ ⟩ end SLang diff --git a/SampCert/Util/Gaussian/DiscreteGaussian.lean b/SampCert/Util/Gaussian/DiscreteGaussian.lean index f522f308..33623a93 100644 --- a/SampCert/Util/Gaussian/DiscreteGaussian.lean +++ b/SampCert/Util/Gaussian/DiscreteGaussian.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jean-Baptiste Tristan -/ import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable +import Mathlib.Probability.ProbabilityMassFunction.Basic /-! # Discrete Guassian Definitions @@ -334,3 +335,23 @@ theorem discrete_gaussian_normalizes {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) : rw [tsum_div_const] rw [div_eq_one_iff_eq] apply sum_gauss_term_ne_zero h + + +/-- +Discrete Gaussian cast to ENNReal has sum 1 +-/ +def discrete_gaussian_normal {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) : HasSum (fun z : ℤ => ENNReal.ofReal (discrete_gaussian σ μ z)) 1 := by + rw [Summable.hasSum_iff ENNReal.summable] + rw [<- ENNReal.ofReal_tsum_of_nonneg] + case hf_nonneg => + exact fun n => discrete_gaussian_nonneg h μ n + case hf => + apply discrete_gaussian_summable' + apply h + simp [discrete_gaussian_normalizes h μ] + +/-- +The discrete Gaussian as a PMF +-/ +def discrete_gaussian_pmf {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) : PMF ℤ := + ⟨ (fun z : ℤ => ENNReal.ofReal (discrete_gaussian σ μ z)) , discrete_gaussian_normal h μ ⟩ diff --git a/SampCert/Util/Log.lean b/SampCert/Util/Log.lean new file mode 100644 index 00000000..064db04b --- /dev/null +++ b/SampCert/Util/Log.lean @@ -0,0 +1,761 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jean-Baptiste Tristan, Markus de Medeiros +-/ + +import Mathlib.Data.ENNReal.Basic +import Mathlib.Data.Real.EReal +import Mathlib.Analysis.SpecialFunctions.Log.Basic +import Mathlib.Analysis.SpecialFunctions.Pow.NNReal +import Lean.Elab.Tactic + + +/-! +# Logarithm on ENNReal + +In this file we extend the logarithm to ``ENNReal``. + +The main definitions in this file are +- ``ofEReal : EReal -> ENNReal`` : Casting ``EReal`` to ``ENNReal`` by truncation +- ``eexp : EReal -> ENNReal`` : Exponential extended to the ``EReal``s +- ``elog : ENNReal -> EReal`` : Logarithm extended to the ``ENNReal``s +-/ + +noncomputable section + +open scoped Classical +open ENNReal EReal Real + + + +section EReal_conv_cases +/-! +### Case analysis lemmas + +Most conversion proofs follow by splitting into cases, and then simplifying. However +explicitly performing case analysis can be unwieldy and lead to lots of duplicate work, +depending on which simplification rules are used. These tactics allow us to fine-tune the +case splits at the start of a conversion proof in order to reduce the number of cases we must +prove by hand. + + +Tactic overview: + +Real numbers: +- ``case_Real_zero``: A real number is zero or nonzero +- ``case_Real_sign``: A real number is negative, zero, or positive +- ``case_nonneg_zero``: Given ``0 ≤ r``, `r` is zero or positive +- ``case_Real_nonnegative`` : A real number is negative or nonnegative + +Extended nonnegative real numbers: +- ``case_ENNReal_isReal``: An ``ENNReal`` is ⊤, or the cast of a real number +- ``case_ENNReal_isReal_zero``: An ``ENNReal`` is ⊤, zero, or the cast of a real number + +Extended reals: +- ``case_EReal_isReal``: An ``EReal`` is ⊤, ⊥, or the cast of a real number +- ``case_EReal_isENNReal``: An `EReal`` is negative, or the cast of an ``ENNReal`` +-/ + + +/-- +A real number is either zero or nonzero +-/ +lemma Real_cases_zero (r : ℝ) : r = 0 ∨ r ≠ 0 := by + exact eq_or_ne r (OfNat.ofNat 0) + +syntax "case_Real_zero" term : tactic +macro_rules +| `(tactic| case_Real_zero $r:term ) => + `(tactic| rcases (eq_or_ne $r (OfNat.ofNat 0)) with _ | _ <;> try simp_all) + + + +/-- +A real number is either negative, zero, or postive +-/ +lemma Real_cases_sign (r : ℝ) : r < 0 ∨ r = 0 ∨ 0 < r := by exact lt_trichotomy r (OfNat.ofNat 0) + +syntax "case_Real_sign" term : tactic +macro_rules +| `(tactic| case_Real_sign $r:term ) => + `(tactic| rcases (Real_cases_sign $r) with _ | _ | _ <;> try simp_all) + +/-- +A nonnegative number is either zero or positive +-/ +syntax "case_nonneg_zero" term : tactic +macro_rules +| `(tactic| case_nonneg_zero $H:term ) => + `(tactic| rcases (LE.le.eq_or_gt $H) with _ | _ <;> try simp_all) + + + +/-- +A real number is either negative, or nonzero +-/ +lemma Real_cases_nonnegative (r : ℝ) : r < 0 ∨ 0 ≤ r := by exact lt_or_le r (OfNat.ofNat 0) + +syntax "case_Real_nonnegative " term : tactic +macro_rules +| `(tactic| case_Real_nonnegative $r:term ) => + `(tactic| rcases (Real_cases_nonnegative $r) with _ | _ <;> try simp_all) + + +lemma ENNReal_isReal_cases (x : ENNReal) : x = ⊤ ∨ (∃ v : ℝ, x = ENNReal.ofReal v ∧ 0 ≤ v) := by + cases x + · left + simp + . right + rename_i v + rcases v with ⟨ r, Hr ⟩ + exists r + apply And.intro + · simp [ENNReal.ofReal, Real.toNNReal] + congr + rw [max_eq_left Hr] + · assumption + +syntax "case_ENNReal_isReal" term : tactic +macro_rules +| `(tactic| case_ENNReal_isReal $w:term ) => + `(tactic| rcases (ENNReal_isReal_cases $w) with _ | ⟨ _, _, _⟩ <;> try simp_all) + +/-- +An ENNReal is either top, zero, or the lift if a positive real +-/ +lemma ENNReal_isReal_zero_cases (x : ENNReal) : x = ⊤ ∨ x = 0 ∨ (∃ v : ℝ, x = ENNReal.ofReal v ∧ 0 < v) := by + case_ENNReal_isReal x + rename_i r Hr1 Hr2 + case_nonneg_zero Hr2 + right + exists r + +syntax "case_ENNReal_isReal_zero" term : tactic +macro_rules +| `(tactic| case_ENNReal_isReal_zero $w:term ) => + `(tactic| rcases (ENNReal_isReal_zero_cases $w) with _ | _ | ⟨ _, _, _⟩ <;> try simp_all) + +/-- +An EReal is either ⊤, ⊥, or the lift of some real number. +-/ +lemma EReal_isReal_cases (w : EReal) : w = ⊥ ∨ w = ⊤ ∨ (∃ v : ℝ, w = Real.toEReal v) := by + cases w + · left + rfl + rename_i w' + cases w' + · right + left + rfl + rename_i wR + right + right + exists wR + +syntax "case_EReal_isReal" term : tactic +macro_rules +| `(tactic| case_EReal_isReal $w:term ) => + `(tactic| rcases (EReal_isReal_cases $w) with _ | _ | ⟨ _, _ ⟩ <;> try simp_all) + +/-- +An EReal is either negative, or the lift of an ENNReal +-/ +lemma EReal_isENNReal_cases (w : EReal) : (w < 0) ∨ (∃ v : ENNReal, w = ENNReal.toEReal v) := by + case_EReal_isReal w + · exists ⊤ + · rename_i w' Hw' + case_Real_nonnegative w' + rename_i Hw'' + right + exists (ENNReal.ofReal w') + simp only [coe_ennreal_ofReal, EReal.coe_eq_coe_iff] + rw [max_eq_left Hw''] + +syntax "case_EReal_isENNReal" term : tactic +macro_rules +| `(tactic| case_EReal_isENNReal $w:term ) => + `(tactic| rcases (EReal_isENNReal_cases $w) with _ | ⟨ _, _ ⟩ <;> try simp_all) + + +end EReal_conv_cases + + + +namespace ENNReal + +section ofEReal +/-! +### Coercion from EReals to ENNreals +-/ + + +/-- +Truncate an `EReal` to an `ENNReal` +-/ +noncomputable def ofEReal (e : EReal) : ENNReal := + match e with + | ⊥ => some 0 + | ⊤ => ⊤ + | some (some r) => ENNReal.ofReal r + +@[simp] +lemma ofEReal_bot : ofEReal ⊥ = 0 := by simp [ofEReal] + +@[simp] +lemma ofEReal_top : ofEReal ⊤ = ⊤ := by simp [ofEReal] + +@[simp] +lemma ofEReal_zero : ofEReal 0 = 0 := by simp [ofEReal] + +@[simp] +lemma ofEReal_real (r : ℝ) : ofEReal r = ENNReal.ofReal r := by simp [Real.toEReal, ofEReal] + + +lemma ofEReal_eq_zero_iff (w : EReal) : w ≤ 0 <-> ofEReal w = 0 := by + apply Iff.intro + · intro _ + case_EReal_isReal w + · intro _ + case_EReal_isReal w + +/-- +``ofEReal`` is injective for for positive EReals +-/ +lemma ofEReal_nonneg_inj {w z : EReal} (Hw : 0 <= w) (Hz : 0 <= z) : + w = z <-> (ofEReal w = ofEReal z) := by + apply Iff.intro + · intro _ + simp_all + · intro Heq + all_goals case_EReal_isReal w + all_goals case_EReal_isReal z + +@[simp] +lemma toEReal_ofENNReal_nonneg {w : EReal} (H : 0 ≤ w) : ENNReal.toEReal (ofEReal w) = w := by case_EReal_isReal w + +@[simp] +lemma ofEReal_toENNReal {x : ENNReal} : ofEReal (ENNReal.toEReal x) = x := by case_ENNReal_isReal x + +/- +`ENNReal.ofReal` is the composition of cases from Real to EReal to ENNReal +-/ +@[simp] +lemma ofEReal_ofReal_toENNReal : ENNReal.ofEReal (Real.toEReal r) = ENNReal.ofReal r := by + simp [ofEReal, Real.toEReal, ENNReal.ofReal] + + +lemma ofEReal_le_mono {w z : EReal} (H : w ≤ z) : ofEReal w ≤ ofEReal z := by + all_goals case_EReal_isReal w + all_goals case_EReal_isReal z + apply ofReal_le_ofReal + assumption + +-- True, and provable, but unused +-- lemma ofEReal_le_mono_conv_nonneg {w z : EReal} (Hw : 0 ≤ w) (Hle : ofEReal w ≤ ofEReal z) : w ≤ z := by +-- all_goals case_EReal_isENNReal w +-- all_goals case_EReal_isENNReal z +-- · exfalso +-- rename_i Hw' _ +-- -- 0 <= w < 0 +-- sorry +-- · exfalso +-- rename_i r Hw' Hr +-- -- 0 <= w < 0 +-- sorry +-- · exfalso +-- rename_i r Hr Hz' +-- -- 0 <= w <= z < 0 +-- sorry + + + + @[simp] + lemma ofEReal_plus_nonneg (Hw : 0 ≤ w) (Hz : 0 ≤ z) : ofEReal (w + z) = ofEReal w + ofEReal z := by + all_goals case_EReal_isReal w + all_goals case_EReal_isReal z + rename_i w' z' _ _ + rw [← EReal.coe_add] + rw [ofEReal_ofReal_toENNReal] + rw [ofReal_add Hw Hz] + + + +@[simp] +lemma ofEReal_mul_nonneg (Hw : 0 ≤ w) (Hz : 0 ≤ z) : ofEReal (w * z) = ofEReal w * ofEReal z := by + all_goals case_EReal_isReal w + all_goals case_EReal_isReal z + · rename_i r _ _ + case_nonneg_zero Hz + rename_i Hr_nz + simp [top_mul_coe_of_pos Hr_nz] + · rename_i r Hr Hz' + case_nonneg_zero Hw + rename_i Hr_nz + simp [coe_mul_top_of_pos Hr_nz] + · rw [← EReal.coe_mul] + rw [ofEReal_ofReal_toENNReal] + rw [ofReal_mul' Hz] + + + +lemma ofEReal_nonneg_scal_l {r : ℝ} {w : EReal} (H1 : 0 < r) (H2 : 0 ≤ r * w) : 0 ≤ w := by + all_goals case_EReal_isReal w + · exfalso + rw [EReal.mul_bot_of_pos (EReal.coe_pos.mpr H1)] at H2 + simp at H2 + · rename_i w' Hw' + rw [← EReal.coe_mul] at H2 + apply EReal.coe_nonneg.mp at H2 + exact nonneg_of_mul_nonneg_right H2 H1 + +end ofEReal + + +/-- +``ENNReal.ofReal`` is injective for for positive EReals +-/ +lemma ofReal_injective_nonneg {r s : ℝ} (HR : 0 ≤ r) (HS : 0 ≤ s) (H : ENNReal.ofReal r = ENNReal.ofReal s) : r = s := by + apply (Real.toNNReal_eq_toNNReal_iff HR HS).mp + simp [ENNReal.ofReal] at H + assumption + + + + +section elog_eexp + +/-- +The extended logarithm +-/ +def elog (x : ENNReal) : EReal := + match x with + | ⊤ => ⊤ + | some r => if r = 0 then ⊥ else Real.log r + +/-- +The extended exponential + +Mathlib's has an extended ``rpow`` function of type ``ℝ≥0∞ → ℝ → ℝ≥0∞``, however we +want the exponent to be of type ``EReal``. +-/ +def eexp (y : EReal) : ENNReal := + match y with + | ⊥ => 0 + | ⊤ => ⊤ + | some (some r) => ENNReal.ofReal (Real.exp r) + +-- MARKUSDE: cleanup? +@[simp] +lemma elog_of_pos_real {r : ℝ} (H : 0 < r) : elog (ENNReal.ofReal r) = Real.log r := by + rw [elog] + split + · simp at * + · split + · rename_i r' heq h + exfalso + rw [h] at heq + simp at heq + linarith + · rename_i h' r' heq h + simp_all + congr + simp [ENNReal.ofReal] at heq + rw [<- heq] + exact (Real.coe_toNNReal r (le_of_lt H)) + +@[simp] +lemma elog_zero : elog 0 = ⊥ := by simp [elog] + +@[simp] +lemma elog_top : elog ⊤ = ⊤ := by simp [elog] + +@[simp] +lemma eexp_bot : eexp ⊥ = 0 := by simp [eexp] + +@[simp] +lemma eexp_top : eexp ⊤ = ⊤ := by simp [eexp] + +@[simp] +lemma eexp_zero : eexp 0 = 1 := by simp [eexp] + +@[simp] +lemma eexp_ofReal {r : ℝ} : eexp r = ENNReal.ofReal (Real.exp r) := by + simp [ENNReal.ofReal, eexp, elog] + rfl + +@[simp] +lemma elog_eexp {x : ENNReal} : eexp (elog x) = x := by + rw [elog] + split + · simp + · rename_i _ r' + split + · simp + rename_i _ h + rw [h] + · rename_i _ H + simp + rw [NNReal.toReal] + simp + rw [Real.exp_log] + rw [ofReal_coe_nnreal] + rcases r' with ⟨ v , Hv ⟩ + apply lt_of_le_of_ne + · simpa + · simp + intro Hk + apply H + apply NNReal.coe_eq_zero.mp + simp + rw [Hk] + +@[simp] +lemma eexp_elog {w : EReal} : (elog (eexp w)) = w := by + cases w + · simp [eexp, elog] + rfl + · simp [eexp, elog] + rename_i v' + cases v' + · simp + rfl + · simp + rename_i v'' + simp [ENNReal.ofReal] + split + · rename_i Hcont + have Hcont' : 0 < rexp v'' := by exact exp_pos v'' + linarith + · rename_i H + have RW : (max (rexp v'') 0) = (rexp v'') := by + apply max_eq_left_iff.mpr + linarith + simp [RW] + clear RW + simp [Real.toEReal] + + +lemma elog_ENNReal_ofReal_of_pos {x : ℝ} (H : 0 < x) : (ENNReal.ofReal x).elog = x.log.toEReal := by + simp [ENNReal.ofReal, ENNReal.elog, ENNReal.toEReal] + rw [ite_eq_iff'] + apply And.intro + · intro + exfalso + linarith + · intro H + simp at H + rw [max_eq_left_of_lt H] + +@[simp] +lemma elog_mul {x y : ENNReal} : elog x + elog y = elog (x * y) := by + all_goals case_ENNReal_isReal_zero x + all_goals case_ENNReal_isReal_zero y + rename_i r₁ Hr₁ HPr₁ r₂ Hr₂ HPr₂ + rw [← EReal.coe_add] + rw [<- Real.log_mul ?G1 ?G2] + case G1 => linarith + case G2 => linarith + rw [<- elog_ENNReal_ofReal_of_pos ?G1] + case G1 => exact Real.mul_pos HPr₁ HPr₂ + rw [ENNReal.ofReal_mul] + linarith + + +@[simp] +lemma eexp_add {w z : EReal} : eexp w * eexp z = eexp (w + z) := by + all_goals case_EReal_isReal w + all_goals case_EReal_isReal z + · apply top_mul + simp + apply exp_pos + · apply mul_top + simp + apply exp_pos + rw [← EReal.coe_add] + rw [<- ENNReal.ofReal_mul ?G1] + case G1 => apply exp_nonneg + rw [← exp_add] + rw [eexp_ofReal] + + +lemma eexp_injective {w z : EReal} : eexp w = eexp z -> w = z := by + rw [eexp, eexp] + intro H + cases w <;> cases z <;> try tauto + · rename_i v + cases v <;> simp at * + rename_i v' + have Hv' := exp_pos v' + linarith + · rename_i v + cases v <;> simp at * + rename_i v' + have Hv' := exp_pos v' + linarith + · rename_i v₁ v₂ + cases v₁ <;> cases v₂ <;> simp at * + congr + rename_i v₁' v₂' + simp [ENNReal.ofReal] at H + apply NNReal.coe_inj.mpr at H + simp at H + have RW (r : ℝ) : (max (rexp r) 0) = (rexp r) := by + apply max_eq_left_iff.mpr + exact exp_nonneg r + rw [RW v₁'] at H + rw [RW v₂'] at H + exact exp_eq_exp.mp H + + +lemma elog_injective {x y : ENNReal} : elog x = elog y -> x = y := by + all_goals case_ENNReal_isReal_zero x + all_goals case_ENNReal_isReal_zero y + rename_i r₁ Hr₁ HPr₁ r₂ Hr₂ HPr₂ + intro Hlog_eq + suffices r₁ = r₂ by simp [this] + apply Real.log_injOn_pos + all_goals simp_all + + +lemma eexp_zero_iff {w : EReal} : eexp w = 0 <-> w = ⊥ := by + apply Iff.intro + · intro H + all_goals case_EReal_isReal w + rename_i r _ + have Hcont := exp_pos r + linarith + · simp_all + + +lemma elog_bot_iff {x : ENNReal} : elog x = ⊥ <-> x = 0 := by + apply Iff.intro + · intro H + all_goals case_ENNReal_isReal_zero x + · simp_all + + + +lemma eexp_mono_lt {w z : EReal} : (w < z) <-> eexp w < eexp z := by + apply Iff.intro + · intro H + all_goals case_EReal_isReal w + · apply bot_lt_iff_ne_bot.mpr + apply bot_lt_iff_ne_bot.mp at H + intro HK + apply H + apply eexp_zero_iff.mp + simp_all + all_goals case_EReal_isReal z + apply (ENNReal.ofReal_lt_ofReal_iff_of_nonneg ?G1).mpr + case G1 => apply exp_nonneg + exact exp_lt_exp.mpr H + · intro H + all_goals case_EReal_isReal w + · apply bot_lt_iff_ne_bot.mpr + intro HK + have H'' : 0 ≠ eexp z := by exact ne_of_lt H + apply H'' + symm + apply eexp_zero_iff.mpr + assumption + all_goals case_EReal_isReal z + rename_i a _ _ _ + have C1 : OfNat.ofNat 0 ≤ rexp a := by exact exp_nonneg a + apply (ENNReal.ofReal_lt_ofReal_iff_of_nonneg C1).mp at H + exact exp_lt_exp.mp H + + + +lemma eexp_mono_le {w z : EReal} : (w <= z) <-> eexp w <= eexp z := by + apply Iff.intro + · intro H + cases (LE.le.lt_or_eq H) + · apply LT.lt.le + apply eexp_mono_lt.mp + assumption + · simp_all + · intro H + cases (LE.le.lt_or_eq H) + · apply LT.lt.le + apply eexp_mono_lt.mpr + assumption + · apply Eq.le + apply eexp_injective + assumption + + + +lemma elog_mono_lt {x y : ENNReal} : (x < y) <-> elog x < elog y := by + apply Iff.intro + · intro H + all_goals case_ENNReal_isReal_zero x + · apply Ne.bot_lt' + intro HK + symm at HK + apply elog_bot_iff.mp at HK + simp [HK] at H + all_goals case_ENNReal_isReal_zero y + apply log_lt_log + · assumption + · assumption + · intro H + all_goals case_ENNReal_isReal_zero x + · apply Ne.bot_lt' + intro HK + symm at HK + simp [HK] at H + all_goals case_ENNReal_isReal_zero y + apply (Real.log_lt_log_iff ?G1 ?G2).mp <;> assumption + + + + +lemma elog_mono_le {x y : ENNReal} : (x <= y) <-> elog x <= elog y := by + apply Iff.intro + · intro H + cases (LE.le.lt_or_eq H) + · apply LT.lt.le + apply elog_mono_lt.mp + assumption + · simp_all + · intro H + cases (LE.le.lt_or_eq H) + · apply LT.lt.le + apply elog_mono_lt.mpr + assumption + · apply Eq.le + apply elog_injective + assumption + + +end elog_eexp + + + + + +section misc + + +lemma mul_mul_inv_le_mul_cancel {x y : ENNReal} : (x * y⁻¹) * y ≤ x := by + cases x + · simp_all + rename_i x' + cases (Classical.em (x' = 0)) + · simp_all + rename_i Hx' + cases y + · simp_all + rename_i y' + cases (Classical.em (y' = 0)) + · simp_all + rename_i Hy' + simp + rw [← coe_inv Hy'] + rw [← coe_mul] + rw [← coe_mul] + rw [mul_right_comm] + rw [mul_inv_cancel_right₀ Hy' x'] + +lemma mul_mul_inv_eq_mul_cancel {x y : ENNReal} (H : y = 0 -> x = 0) (H2 : ¬(x ≠ 0 ∧ y = ⊤)) : (x * y⁻¹) * y = x := by + cases x + · simp_all + rename_i x' + cases (Classical.em (x' = 0)) + · simp_all + rename_i Hx' + cases y + · simp_all + rename_i y' + cases (Classical.em (y' = 0)) + · simp_all + rename_i Hy' + simp + rw [← coe_inv Hy'] + rw [← coe_mul] + rw [← coe_mul] + rw [mul_right_comm] + rw [mul_inv_cancel_right₀ Hy' x'] + +lemma ereal_smul_le_left {w z : EReal} (s : EReal) (Hr1 : 0 < s) (Hr2 : s < ⊤) (H : s * w ≤ s * z) : w ≤ z := by + have defTop : some none = (⊤ : EReal) := by simp [Top.top] + have defBot : none = (⊥ : EReal) := by simp [Bot.bot] + + cases s + · exfalso + rw [defBot] at Hr1 + simp_all only [not_lt_bot] + rename_i s_nnr + cases s_nnr + · rw [defTop] at Hr2 + exfalso + simp_all only [EReal.zero_lt_top, lt_self_iff_false] + rename_i s_R + have Hsr : some (some s_R) = Real.toEReal s_R := by simp [Real.toEReal] + rw [Hsr] at H + rw [Hsr] at Hr1 + rw [Hsr] at Hr2 + clear Hsr + + cases w + · apply left_eq_inf.mp + rfl + rename_i w_nnr + cases w_nnr + · simp [defTop] at H + rw [EReal.mul_top_of_pos Hr1] at H + have X1 : z = ⊤ := by + cases z + · exfalso + simp at H + rw [defBot] at H + rw [EReal.mul_bot_of_pos] at H + · cases H + · apply Hr1 + rename_i z_nnr + cases z_nnr + · simp [Top.top] + exfalso + apply top_le_iff.mp at H + rename_i z_R + have Hzr : some (some z_R) = Real.toEReal z_R := by simp [Real.toEReal] + rw [Hzr] at H + rw [<- EReal.coe_mul] at H + cases H + rw [defTop, X1] + rename_i w_R + cases z + · simp [defBot] at H + rw [EReal.mul_bot_of_pos] at H + apply le_bot_iff.mp at H + · rw [defBot] + have Hwr : some (some w_R) = Real.toEReal w_R := by simp [Real.toEReal] + rw [Hwr] at H + rw [<- EReal.coe_mul] at H + cases H + · apply Hr1 + rename_i z_nnr + cases z_nnr + · exact right_eq_inf.mp rfl + rename_i z_R + have Hwr : some (some w_R) = Real.toEReal w_R := by simp [Real.toEReal] + have Hzr : some (some z_R) = Real.toEReal z_R := by simp [Real.toEReal] + rw [Hwr, Hzr] at H + rw [Hwr, Hzr] + clear Hwr + clear Hzr + apply EReal.coe_le_coe_iff.mpr + repeat rw [<- EReal.coe_mul] at H + apply EReal.coe_le_coe_iff.mp at H + apply le_of_mul_le_mul_left H + exact EReal.coe_pos.mp Hr1 + +lemma ereal_smul_eq_left {w z : EReal} (s : EReal) (Hr1 : 0 < s) (Hr2 : s < ⊤) (H : s * w = s * z) : w = z := by + apply LE.le.antisymm + · apply ereal_smul_le_left s Hr1 Hr2 (le_of_eq H) + · apply ereal_smul_le_left s Hr1 Hr2 (le_of_eq (id (Eq.symm H))) + +end misc + +end ENNReal