Complete proof all the way to mean query

SampCert/DiffPrivacy/BoundedAvg.lean

@@ -14,36 +14,46 @@ noncomputable section
 
 namespace SLang
 
--- def NoisedBoundedAvgQuery (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) (l : List ℤ) : SLang ℤ := do
---   let S ← NoisedBoundedSumQuery L U h ε₁ (2 * ε₂) l
---   let C ← NoisedCountingQuery ε₁ (2 * ε₂) l
---   return S / C
-
--- def NoisedBoundedAvgQuery' (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) (l : List ℤ) : SLang ℤ :=
---   let X := Compose (NoisedBoundedSumQuery L U h ε₁ (2 * ε₂)) (NoisedCountingQuery ε₁ (2 * ε₂))
---   PostProcess X (fun z => z.1 / z.2) l
-
--- theorem NoisedBoundedAvgQueryIdentical (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) :
---   NoisedBoundedAvgQuery' L U h ε₁ ε₂ = NoisedBoundedAvgQuery L U h ε₁ ε₂  := by
---   ext l x
---   simp [NoisedBoundedAvgQuery, NoisedBoundedAvgQuery', PostProcess, Compose]
-
--- theorem BoundedSumQueryDP (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) : DP (NoisedBoundedAvgQuery L U h ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by
---   rw [← NoisedBoundedAvgQueryIdentical]
---   unfold NoisedBoundedAvgQuery'
---   simp only
-
---   have A₁ := @NoisedCountingQueryDP ℤ ε₁ (2 * ε₂)
---   have A₂ := @NoisedCountingQuery_NonZeroNQ ℤ ε₁ (2 * ε₂)
---   have A₃ := @NoisedCountingQuery_NonTopNQ ℤ ε₁ (2 * ε₂)
---   have A₄ := @NoisedCountingQuery_NonTopRDNQ ℤ ε₁ (2 * ε₂)
---   sorry
-  -- have B := @NoisedBoundedSumQueryDP L U h ε₁ (2 * ε₂)
-  -- have C := DPCompose B A
-  -- simp at C
-  -- ring_nf at C
-  -- rw [← division_def] at C
-  -- have D := DPPostProcess C (fun z => z.1 / z.2)
-  -- exact D
+def NoisedBoundedAvgQuery (U : ℕ+) (ε₁ ε₂ : ℕ+) (l : List ℕ) : SLang ℤ := do
+  let S ← NoisedBoundedSumQuery U ε₁ (2 * ε₂) l
+  let C ← NoisedCountingQuery ε₁ (2 * ε₂) l
+  return S / C
+
+def NoisedBoundedAvgQuery' (U : ℕ+) (ε₁ ε₂ : ℕ+) (l : List ℕ) : SLang ℤ :=
+  let X := Compose (NoisedBoundedSumQuery U ε₁ (2 * ε₂)) (NoisedCountingQuery ε₁ (2 * ε₂))
+  PostProcess X (fun z => z.1 / z.2) l
+
+theorem NoisedBoundedAvgQueryIdentical (U : ℕ+) (ε₁ ε₂ : ℕ+) :
+  NoisedBoundedAvgQuery' U ε₁ ε₂ = NoisedBoundedAvgQuery U ε₁ ε₂  := by
+  ext l x
+  simp [NoisedBoundedAvgQuery, NoisedBoundedAvgQuery', PostProcess, Compose]
+
+theorem BoundedSumQueryDP (U : ℕ+) (ε₁ ε₂ : ℕ+) : DP (NoisedBoundedAvgQuery U ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by
+  rw [← NoisedBoundedAvgQueryIdentical]
+  unfold NoisedBoundedAvgQuery'
+  simp only
+
+  have A₁ := @NoisedCountingQueryDP ℕ ε₁ (2 * ε₂)
+  have A₂ := @NoisedCountingQuery_NonZeroNQ ℕ ε₁ (2 * ε₂)
+  have A₃ := @NoisedCountingQuery_NonTopNQ ℕ ε₁ (2 * ε₂)
+  have A₄ := @NoisedCountingQuery_NonTopRDNQ ℕ ε₁ (2 * ε₂)
+  have A₅ := @NoisedCountingQuery_NonTopSum ℕ ε₁ (2 * ε₂)
+
+  have B₁ := NoisedBoundedSumQueryDP U ε₁ (2 * ε₂)
+  have B₂ := NoisedBoundedSumQuery_NonZeroNQ U ε₁ (2 * ε₂)
+  have B₃ := NoisedBoundedSumQuery_NonTopNQ U ε₁ (2 * ε₂)
+  have B₄ := NoisedBoundedSumQuery_NonTopRDNQ U ε₁ (2 * ε₂)
+  have B₅ := NoisedBoundedSumQuery_NonTopSum U ε₁ (2 * ε₂)
+
+  have C₁ := DPCompose B₁ A₁ B₂ A₂ B₄ A₄ B₃ A₃
+  have C₂ := DPCompose_NonZeroNQ B₂ A₂
+  have C₃ := DPCompose_NonTopNQ B₃ A₃
+  have C₄ := DPCompose_NonTopRDNQ B₄ A₄ B₂ A₂
+  have C₅ := DPCompose_NonTopSum B₅ A₅
+  simp at *
+  ring_nf at *
+  rw [← division_def] at *
+  have D := DPPostProcess C₁ C₂ C₄ C₃ C₅ (fun z => z.1 /z.2)
+  exact D
 
 end SLang

SampCert/DiffPrivacy/BoundedSum.lean

@@ -15,58 +15,121 @@ noncomputable section
 
 namespace SLang
 
-def BoundedSumQuery (L U : ℤ) (l : List ℤ) : ℤ :=
-  let center := |U - L| / 2
-  let L := L - center
-  let U := U - center
-  let S := List.sum (List.map (fun n : ℤ => max (min (n - center) U) L) l)
-  S + center * List.length l
-
-theorem natAbs1 {n : ℕ} {x : ℤ} (h : n ≤ x) :
-  n ≤ natAbs x := by
-  cases x
-  . rename_i m
+def BoundedSumQuery (U : ℕ+) (l : List ℕ) : ℤ :=
+  List.sum (List.map (fun n : ℕ => (Nat.min n U)) l)
+
+-- theorem natAbs1 {n : ℕ} {x : ℤ} (h : n ≤ x) :
+--   n ≤ natAbs x := by
+--   cases x
+--   . rename_i m
+--     simp
+--     exact Int.ofNat_le.mp h
+--   . rename_i m
+--     simp
+--     have A : -[m+1] < 0 := negSucc_lt_zero m
+--     have B : n < (0 : ℤ) := by
+--       apply Int.lt_of_le_of_lt h A
+--     contradiction
+
+-- def maxBoundPos (L U : ℤ) (h : L < U) :
+--   0 < max (Int.natAbs L) (Int.natAbs U) := by
+--   have A : ¬ (L = 0 ∧ U = 0) := by
+--     by_contra h'
+--     cases h'
+--     rename_i h1 h2
+--     subst h1 h2
+--     contradiction
+--   simp at A
+--   have B : L = 0 ∨ L ≠ 0 := by exact eq_or_ne L 0
+--   cases B
+--   . rename_i h'
+--     subst h'
+--     simp at A
+--     simp
+--     trivial
+--   . rename_i h'
+--     simp
+--     left
+--     trivial
+
+-- def maxBound (L U : ℤ) (h : L < U) : ℕ+ :=
+--   ⟨ max (Int.natAbs L) (Int.natAbs U) , maxBoundPos L U h ⟩
+
+theorem BoundedSumQuerySensitivity (U : ℕ+) : sensitivity (BoundedSumQuery U) U := by
+  simp [sensitivity, BoundedSumQuery]
+  intros l₁ l₂ H
+  have A : ∀ n : ℕ, (@min ℤ instMinInt (n : ℤ) (U : ℤ) = n) ∨ (@min ℤ instMinInt n U = U) := by
+    intro n
     simp
-    exact Int.ofNat_le.mp h
-  . rename_i m
+    exact Nat.le_total n ↑U
+  cases H
+  . rename_i l l' n h1 h2
+    subst h1 h2
     simp
-    have A : -[m+1] < 0 := negSucc_lt_zero m
-    have B : n < (0 : ℤ) := by
-      apply Int.lt_of_le_of_lt h A
-    contradiction
-
-def maxBoundPos (L U : ℤ) (h : L < U) :
-  0 < max (Int.natAbs L) (Int.natAbs U) := by
-  have A : ¬ (L = 0 ∧ U = 0) := by
-    by_contra h'
-    cases h'
-    rename_i h1 h2
+    cases A n
+    . rename_i h
+      rw [h]
+      simp at *
+      trivial
+    . rename_i h
+      rw [h]
+      simp
+  . rename_i l n l' h1 h2
     subst h1 h2
-    contradiction
-  simp at A
-  have B : L = 0 ∨ L ≠ 0 := by exact eq_or_ne L 0
-  cases B
-  . rename_i h'
-    subst h'
-    simp at A
     simp
-    trivial
-  . rename_i h'
+    cases A n
+    . rename_i h
+      rw [h]
+      simp at *
+      trivial
+    . rename_i h
+      rw [h]
+      simp
+  . rename_i l n l' m h1 h2
+    subst h1 h2
     simp
-    left
-    trivial
+    cases A n
+    . rename_i h
+      cases A m
+      . rename_i h'
+        rw [h, h']
+        simp at *
+        apply Int.natAbs_coe_sub_coe_le_of_le h h'
+      . rename_i h'
+        rw [h, h']
+        simp at *
+        apply Int.natAbs_coe_sub_coe_le_of_le h le_rfl
+    . rename_i h
+      cases A m
+      . rename_i h'
+        rw [h, h']
+        simp at *
+        apply Int.natAbs_coe_sub_coe_le_of_le le_rfl h'
+      . rename_i h'
+        rw [h, h']
+        simp at *
+
+def NoisedBoundedSumQuery (U : ℕ+) (ε₁ ε₂ : ℕ+) (l : List ℕ) : SLang ℤ := do
+  NoisedQuery (BoundedSumQuery U) U ε₁ ε₂ l
+
+theorem NoisedBoundedSumQueryDP (U : ℕ+) (ε₁ ε₂ : ℕ+) : DP (NoisedBoundedSumQuery U ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by
+  apply NoisedQueryDP
+  apply BoundedSumQuerySensitivity
 
-def maxBound (L U : ℤ) (h : L < U) : ℕ+ :=
-  ⟨ max (Int.natAbs L) (Int.natAbs U) , maxBoundPos L U h ⟩
+theorem NoisedBoundedSumQuery_NonZeroNQ (U : ℕ+) (ε₁ ε₂ : ℕ+) :
+  @NonZeroNQ ℕ ℤ (NoisedBoundedSumQuery U ε₁ ε₂) := by
+  apply NoisedQuery_NonZeroNQ
 
--- theorem BoundedSumQuerySensitivity (L U : ℤ) (h : L < U) : sensitivity (BoundedSumQuery L U) (maxBound L U h) := by
---   sorry
+theorem NoisedBoundedSumQuery_NonTopNQ (U : ℕ+) (ε₁ ε₂ : ℕ+) :
+  @NonTopNQ ℕ ℤ (NoisedBoundedSumQuery U ε₁ ε₂) := by
+  apply NoisedQuery_NonTopNQ
 
--- def NoisedBoundedSumQuery (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) (l : List ℤ) : SLang ℤ := do
---   NoisedQuery (BoundedSumQuery L U) (maxBound L U h) ε₁ ε₂ l
+theorem NoisedBoundedSumQuery_NonTopRDNQ (U : ℕ+) (ε₁ ε₂ : ℕ+) :
+  @NonTopRDNQ ℕ ℤ (NoisedBoundedSumQuery U ε₁ ε₂) := by
+  apply NoisedQuery_NonTopRDNQ
 
--- theorem NoisedBoundedSumQueryDP (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) : DP (NoisedBoundedSumQuery L U h ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by
---   apply NoisedQueryDP
---   apply BoundedSumQuerySensitivity
+theorem NoisedBoundedSumQuery_NonTopSum (U : ℕ+) (ε₁ ε₂ : ℕ+) :
+  @NonTopSum ℕ ℤ (NoisedBoundedSumQuery U ε₁ ε₂) := by
+  apply NoisedQuery_NonTopSum
 
 end SLang

SampCert/DiffPrivacy/Count.lean

@@ -51,4 +51,8 @@ theorem NoisedCountingQuery_NonTopRDNQ (ε₁ ε₂ : ℕ+) :
   @NonTopRDNQ T ℤ (NoisedCountingQuery ε₁ ε₂) := by
   apply NoisedQuery_NonTopRDNQ
 
+theorem NoisedCountingQuery_NonTopSum (ε₁ ε₂ : ℕ+) :
+  @NonTopSum T ℤ (NoisedCountingQuery ε₁ ε₂) := by
+  apply NoisedQuery_NonTopSum
+
 end SLang

SampCert/DiffPrivacy/DP.lean

@@ -1175,7 +1175,7 @@ theorem tsum_ne_zero_of_ne_zero {T : Type} [Inhabited T] (f : T → ENNReal) (h
 
 variable [Inhabited U]
 
-theorem DPPostProcess_alt1 {nq : List T → SLang U} {ε₁ ε₂ : ℕ+} (h : DP nq ((ε₁ : ℝ) / ε₂)) (nn : NonZeroNQ nq) (nt : NonTopRDNQ nq) (nts : NonTopNQ nq) (conv : NonTopSum nq) (f : U → ℤ) :
+theorem DPPostProcess {nq : List T → SLang U} {ε₁ ε₂ : ℕ+} (h : DP nq ((ε₁ : ℝ) / ε₂)) (nn : NonZeroNQ nq) (nt : NonTopRDNQ nq) (nts : NonTopNQ nq) (conv : NonTopSum nq) (f : U → ℤ) :
   DP (PostProcess nq f) ((ε₁ : ℝ) / ε₂) := by
   simp [PostProcess, DP, RenyiDivergence]
   intro α h1 l₁ l₂ h2