Laplace done

leanprover · May 29, 2024 · 9fa33e6 · 9fa33e6
1 parent eda5ec4
commit 9fa33e6
Show file tree

Hide file tree

Showing 5 changed files with 110 additions and 116 deletions.
diff --git a/SampCert/DifferentialPrivacy/Pure/Composition.lean b/SampCert/DifferentialPrivacy/Pure/Composition.lean
@@ -17,8 +17,8 @@ namespace SLang
 theorem PureDPCompose' {nq1 : Mechanism T U} {nq2 : List T → SLang V} {ε₁ ε₂ ε₃ ε₄ : ℕ+} (h1 : PureDP nq1 ((ε₁ : ℝ) / ε₂))  (h2 : PureDP nq2 ((ε₃ : ℝ) / ε₄)) :
   DP (Compose nq1 nq2) (((ε₁ : ℝ) / ε₂) + ((ε₃ : ℝ) / ε₄)) := by
   simp [PureDP] at *
-  rcases h1 with ⟨h1a, _, _⟩
-  rcases h2 with ⟨h2a, _, _⟩
+  rcases h1 with ⟨h1a, _⟩
+  rcases h2 with ⟨h2a, _⟩
   rw [event_eq_singleton] at *
   simp [DP_singleton] at *
   intros l₁ l₂ neighbours x y
@@ -62,12 +62,10 @@ theorem PureDPCompose (nq1 : List T → SLang U) (nq2 : List T → SLang V) (ε
   simp [PureDP] at *
   have hc := h
   have h'c := h'
-  rcases h with ⟨ _ , h2 , h3 ⟩
-  rcases h' with ⟨ _ , h'2, h'3 ⟩
+  rcases h with ⟨ _ , h2 ⟩
+  rcases h' with ⟨ _ , h'2 ⟩
   constructor
   . apply PureDPCompose' hc h'c
-  . constructor
-    . apply DPCompose_NonZeroNQ h2 h'2
-    . apply DPCompose_NonTopSum h3 h'3
+  . apply DPCompose_NonZeroNQ h2 h'2
 
 end SLang
diff --git a/SampCert/DifferentialPrivacy/Pure/DP.lean b/SampCert/DifferentialPrivacy/Pure/DP.lean
@@ -29,7 +29,7 @@ def DP (m : Mechanism T U) (ε : ℝ) : Prop :=
 def PureDP (m : Mechanism T U) (ε : ℝ) : Prop :=
   DP m ε
  ∧ NonZeroNQ m
- ∧ NonTopSum m
+ -- ∧ NonTopSum m
 
 def DP_singleton (m : Mechanism T U) (ε : ℝ) : Prop :=
   ∀ l₁ l₂ : List T, Neighbour l₁ l₂ → ∀ x : U,

diff --git a/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean
@@ -27,10 +27,10 @@ theorem NoisedQuery_NonZeroNQPureDP (query : List T → ℤ) (Δ ε₁ ε₂ :
       apply add_pos A Real.zero_lt_one
   . apply exp_pos
 
-theorem NoisedQuery_NonTopSumPureDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) :
-  NonTopSum (NoisedQueryPure query Δ ε₁ ε₂) := by
-  simp [NonTopSum, NoisedQueryPure]
-  sorry
+-- theorem NoisedQuery_NonTopSumPureDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) :
+--   NonTopSum (NoisedQueryPure query Δ ε₁ ε₂) := by
+--   simp [NonTopSum, NoisedQueryPure]
+
 
 theorem natAbs_to_abs (a b : ℤ) :
   (a - b).natAbs = |(a : ℝ) - (b : ℝ)| := by
@@ -128,8 +128,6 @@ theorem NoisedQueryPureDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (boun
   constructor
   . apply NoisedQueryPureDP'
     apply bounded_sensitivity
-  . constructor
-    . apply NoisedQuery_NonZeroNQPureDP
-    . apply NoisedQuery_NonTopSumPureDP
+  . apply NoisedQuery_NonZeroNQPureDP
 
 end SLang
diff --git a/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean b/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean
@@ -17,7 +17,7 @@ namespace SLang
 theorem PureDPPostProcess' {nq : Mechanism T U} {ε₁ ε₂ : ℕ+} (h : PureDP nq ((ε₁ : ℝ) / ε₂)) (f : U → V) :
   DP (PostProcess nq f) (((ε₁ : ℝ) / ε₂)) := by
   simp [PureDP] at *
-  rcases h with ⟨ha, _, _⟩
+  rcases h with ⟨ha, _⟩
   rw [event_eq_singleton] at *
   simp [DP_singleton] at *
   intros l₁ l₂ neighbours x
@@ -41,11 +41,9 @@ theorem PureDPPostProcess {f : U → V} (sur : Function.Surjective f) (nq : List
   PureDP (PostProcess nq f) (((ε₁ : ℝ) / ε₂)) := by
   simp [PureDP] at *
   have hc := h
-  rcases h with ⟨ _ , h2 , h3 ⟩
+  rcases h with ⟨ _ , h2 ⟩
   constructor
   . apply PureDPPostProcess' hc
-  . constructor
-    . apply DPPostProcess_NonZeroNQ h2 sur
-    . apply DPPostProcess_NonTopSum f h3
+  . apply DPPostProcess_NonZeroNQ h2 sur
 
 end SLang
diff --git a/SampCert/Samplers/LaplaceGen/Properties.lean b/SampCert/Samplers/LaplaceGen/Properties.lean
@@ -29,102 +29,102 @@ 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 sorry]
-    apply Summable.mul_left
-    sorry
-
-  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]
-      . sorry -- OK
-    . sorry -- 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]
-
-  -- sorry
+-- 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