Some progress using surjectivity for post processig

SampCert/DifferentialPrivacy/Abstract.lean

@@ -26,16 +26,5 @@ class DPSystem where
   compose_prop : ∀ m₁ : Mechanism T U, ∀ m₂ : Mechanism T V, ∀ ε₁ ε₂ ε₃ ε₄ : ℕ+,
     prop m₁ (ε₁ / ε₂) → prop m₂ (ε₃ / ε₄) → prop (compose m₁ m₂) ((ε₁ / ε₂) + (ε₃ / ε₄))
   postprocess : Mechanism T U → (U → V) → Mechanism T V
-  postprocess_prop : ∀ m : Mechanism T U, ∀ ε₁ ε₂ : ℕ+, ∀ pp : U → V,
+  postprocess_prop : ∀ m : Mechanism T U, ∀ ε₁ ε₂ : ℕ+, ∀ pp : U → V, Function.Surjective pp →
     prop m (ε₁ / ε₂) → prop (postprocess m pp) (ε₁ / ε₂)
-
--- class DPSystem where
---   prop : {U : Type} → Mechanism T U → ℝ → Prop
---   noise : (List T → ℤ) → ℕ+ → ℕ+ → ℕ+ → Mechanism T ℤ
---   noise_prop : ∀ q : List T → ℤ, ∀ Δ εn εd : ℕ+, sensitivity q Δ → prop (noise q Δ εn εd) (εn / εd)
---   compose : {U V : Type} → Mechanism T U → Mechanism T V → Mechanism T (U × V)
---   compose_prop : {U V : Type} → [Inhabited U] → [Inhabited V] → ∀ m₁ : Mechanism T U, ∀ m₂ : Mechanism T V, ∀ ε₁ ε₂ ε₃ ε₄ : ℕ+,
---     prop m₁ (ε₁ / ε₂) → prop m₂ (ε₃ / ε₄) → prop (compose m₁ m₂) ((ε₁ / ε₂) + (ε₃ / ε₄))
---   postprocess : {U : Type} → Mechanism T U → (U → V) → Mechanism T V
---   postprocess_prop : {U V : Type} → [MeasurableSpace U] → [Countable U] → [DiscreteMeasurableSpace U] → [Inhabited U] → ∀ m : Mechanism T U, ∀ ε₁ ε₂ : ℕ+, ∀ pp : U → V,
---     prop m (ε₁ / ε₂) → prop (postprocess m pp) (ε₁ / ε₂)

SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean

@@ -35,9 +35,14 @@ 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 - α) ≠ ⊤
 
+-- def NonZeroRDNQ (nq : List T → SLang U) : Prop :=
+--   ∀ α : ℝ, 1 < α → ∀ l₁ l₂ : List T, Neighbour l₁ l₂ →
+--   ∑' (x : U), nq l₁ x ^ α * nq l₂ x ^ (1 - α) ≠ 0
+
 def zCDP (q : List T → SLang U) (ε : ℝ) : Prop :=
     DP q ε
   ∧ NonZeroNQ q
   ∧ NonTopSum q
   ∧ NonTopNQ q
   ∧ NonTopRDNQ q
+  -- ∧ NonZeroRDNQ q

SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Properties.lean

@@ -145,8 +145,8 @@ theorem DPCompose {nq1 : List T → SLang U} {nq2 : List T → SLang V} {ε₁ 
       intro c
       rw [compose_sum_rw]
       rw [compose_sum_rw]
-      rw [ENNReal.mul_rpow_of_ne_zero (nn1 l₁ b) (nn2 l₁ c)]
-      rw [ENNReal.mul_rpow_of_ne_zero (nn1 l₂ b) (nn2 l₂ c)]
+      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]
@@ -256,7 +256,7 @@ theorem DPCompose_NonTopSum {nq1 : List T → SLang U} {nq2 : List T → SLang V
     cases H
     contradiction
 
-theorem DPCompose_NonTopRDNQ {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nt1 : NonTopRDNQ nq1) (nt2 : NonTopRDNQ nq2) (nn1 : NonZeroNQ nq1) (nn2 : NonZeroNQ nq2) :
+theorem DPCompose_NonTopRDNQ {nq1 : List T → SLang U} {nq2 : List T → SLang V} (nt1 : NonTopRDNQ nq1) (nt2 : NonTopRDNQ nq2) (nn1 : NonTopNQ nq1) (nn2 : NonTopNQ nq2) :
   NonTopRDNQ (Compose nq1 nq2) := by
   simp [NonTopRDNQ] at *
   intro α h1 l₁ l₂ h2
@@ -284,8 +284,8 @@ theorem DPCompose_NonTopRDNQ {nq1 : List T → SLang U} {nq2 : List T → SLang
     intro x
     right
     intro y
-    rw [ENNReal.mul_rpow_of_ne_zero (nn1 l₁ x) (nn2 l₁ y)]
-    rw [ENNReal.mul_rpow_of_ne_zero (nn1 l₂ x) (nn2 l₂ 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]
@@ -329,6 +329,7 @@ theorem zCDPCompose (nq1 : List T → SLang U) (nq2 : List T → SLang V) (ε₁
   . apply DPCompose_NonZeroNQ h2 h'2
   . apply DPCompose_NonTopSum h3 h'3
   . apply DPCompose_NonTopNQ h4 h'4
-  . apply DPCompose_NonTopRDNQ h5 h'5 h2 h'2
+  . apply DPCompose_NonTopRDNQ h5 h'5 h4 h'4
+
 
 end SLang

SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Mechanism/Properties.lean

@@ -254,4 +254,5 @@ theorem NoisedQueryzCDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounde
   . apply NoisedQuery_NonTopNQ
   . apply NoisedQuery_NonTopRDNQ
 
+
 end SLang

SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Postprocessing/Properties.lean

@@ -683,13 +683,49 @@ theorem DPPostProcess {nq : List T → SLang U} {ε₁ ε₂ : ℕ+} (h : DP nq
         rw [lt_top_iff_ne_top] at Z
         contradiction
 
-theorem zCDPPostProcess (nq : List T → SLang U) (ε₁ ε₂ : ℕ+) (f : U → V) (h : zCDP nq ((ε₁ : ℝ) / ε₂)) :
+theorem DPPostPRocess_NonZeroNQ {nq : List T → SLang U} {f : U → V} (nn : NonZeroNQ nq) (sur : Function.Surjective f) :
+  NonZeroNQ (PostProcess nq f) := by
+  simp [NonZeroNQ, Function.Surjective, PostProcess] at *
+  intros l n
+  replace sur := sur n
+  cases sur
+  rename_i a h
+  exists a
+  constructor
+  . rw [h]
+  . apply nn
+
+theorem DPCompose_NonTopSum {nq : List T → SLang U} (f : U → V) (nt : NonTopSum nq) (sur : Function.Surjective f) :
+  NonTopSum (PostProcess nq f) := by
+  simp [NonTopSum, PostProcess] at *
+  intros l
+  have nt := nt l
+  rw [← ENNReal.tsum_fiberwise _ f] at nt
+  conv =>
+    right
+    left
+    right
+    intro n
+    rw [condition_to_subset]
+  unfold Set.preimage at nt
+  sorry -- looks good
+
+theorem DPCompose_NonTopRDNQ {nq : List T → SLang U} (f : U → V) (nt : NonTopRDNQ nq) (ns : NonTopSum nq) (sur : Function.Surjective f) :
+  NonTopRDNQ (PostProcess nq f) := by
+  simp [NonTopRDNQ, NonTopSum, PostProcess] at *
+  intros α h1 l₁ l₂ h2
+  replace nt := nt α h1 l₁ l₂ h2
+  have ns1 := ns l₁
+  have ns2 := ns l₂
+  sorry -- probably good but tedious work
+
+theorem zCDPPostProcess (nq : List T → SLang U) (ε₁ ε₂ : ℕ+) (f : U → V) (sur : Function.Surjective f) (h : zCDP nq ((ε₁ : ℝ) / ε₂)) :
   zCDP (PostProcess nq f) (((ε₁ : ℝ) / ε₂)) := 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
   repeat any_goals constructor
   . apply DPPostProcess h1 h2 h5 h4 h3
-  . sorry
+  . apply DPPostPRocess_NonZeroNQ h2 sur
   . sorry
   . sorry
   . sorry