victory

SampCert/DifferentialPrivacy/Queries/UnboundedMax/Code.lean

@@ -59,7 +59,8 @@ def privNoiseThresh (ε₁ ε₂ : ℕ+) : SPMF ℤ := privNoiseZero ε₁ (2 *
 /-
 ## Program version 0
   - Executable
-  - Tracks single state
+  - Optimization of sv1: Tracks single state
+  (Needs sv0 sv1 equivalence proof)
 -/
 
 def sv0_state : Type := ℕ × ℤ
@@ -82,11 +83,6 @@ def sv0_privMax (ε₁ ε₂ : ℕ+) (l : List ℕ) : SLang ℕ := do
   let sk <- probWhile (sv0_privMaxC τ l) (sv0_privMaxF ε₁ ε₂) (0, v0)
   return (sv0_threshold sk)
 
-def sv0_privMax_PMF (ε₁ ε₂ : ℕ+) (l : List ℕ) : SPMF ℕ :=
-  ⟨ sv0_privMax ε₁ ε₂ l,
-    by
-      sorry ⟩
-
 /-
 ## Program version 1
   - Executable
@@ -113,52 +109,4 @@ def sv1_privMax (ε₁ ε₂ : ℕ+) (l : List ℕ) : SLang ℕ := do
   return (sv1_threshold sk)
 
 
-def sv1_privMax_PMF (ε₁ ε₂ : ℕ+) (l : List ℕ) : SPMF ℕ :=
-  ⟨ sv1_privMax ε₁ ε₂ l,
-    by
-      -- Difficult
-      sorry ⟩
-
 end SLang
-
-/-
-lemma tsum_iSup_comm (f : T -> U -> ENNReal) : ∑' (a : T), ⨆ (b : U), f a b = ⨆ (b : U), ∑' (a : T), f a b := by
-
-  sorry
-
--- A version of probWhile that proves normalization, when its arguments are all normal
-def SPMF_while (cond : T → Bool) (body : T → SPMF T) (init : T) : SPMF T :=
-  ⟨ probWhile cond (fun x => body x) init,
-    by
-      apply (Summable.hasSum_iff ENNReal.summable).mpr
-      unfold probWhile
-      rw [tsum_iSup_comm]
-      conv =>
-        enter [1, 1, cut]
-      -- We can establish the ≤ direction easily
-      -- ≥ is not true
-
-
-
-      -- apply iSup_eq_of_tendsto
-      -- · sorry
-      -- sorry
-
-      -- rw [ENNReal.tsum_eq_iSup_sum]
-      -- apply eq_iff_le_not_lt.mpr
-      -- apply And.intro
-      -- · apply iSup_le_iff.mpr
-      --   sorry
-      -- · simp
-      --   apply le_iSup_iff.mpr
-      --   intro b H
-      --   sorry
-      ⟩
-
-lemma SPMF_while_eq (cond : T → Bool) (body : T → SPMF T) (init : T) :
-    ((SPMF_while cond body init) : SLang T) = (probWhile cond (fun x => body x) init) := by
-  simp [SPMF_while]
-
-
-
--/

SampCert/DifferentialPrivacy/Queries/UnboundedMax/Properties.lean

@@ -2647,13 +2647,26 @@ lemma sv1_lb ε₁ ε₂ l : 1 ≤ ∑'s, (@sv1_privMax PureDPSystem laplace_pur
 
       -- Conclude by simplification
       simp only [sv1_privMaxF, bind, pure, bind_apply, pure_apply, mul_ite, mul_one, mul_zero]
+      apply le_trans _ ?G1
+      case G1 =>
+        apply ENNReal.tsum_le_tsum
+        intro a
+        apply ENNReal.tsum_lb_single (H ++ [v])
+        apply ENNReal.tsum_lb_single a.1
+        rfl
+      simp
+      rw [<- Hρ_1]
+      rw [ENNReal.tsum_split PLucky]
+      rw [add_comm]
 
 
-      sorry
-
-
-
-
+def sv1_privMax_PMF (ε₁ ε₂ : ℕ+) (l : List ℕ) : SPMF ℕ :=
+  ⟨ sv1_privMax ε₁ ε₂ l,
+    by
+      rw [Summable.hasSum_iff ENNReal.summable]
+      apply LE.le.antisymm
+      · apply sv1_ub
+      · apply sv1_lb ⟩
 
 /--
 sv9 normalizes because sv1 normalizes

Test.lean

@@ -257,13 +257,13 @@ def sparseVector_tests : IO Unit := do
   IO.println s!"data := {samples} uniform samples of [0, {(unif_ub : ℕ)}): {(data.take 20)}..."
   IO.println ""
 
-  for i in [:num_trials] do
-    let ct <- run <| @sv0_privMax_PMF PureDPSystem laplace_pureDPSystem num den data
-    IO.println s!"#{i} sv0 max: {ct}"
-  IO.println ""
+  -- for i in [:num_trials] do
+  --   let ct <- run <| @sv0_privMax_PMF PureDPSystem laplace_pureDPSystem num den data
+  --   IO.println s!"#{i} sv0 max: {ct}"
+  -- IO.println ""
 
   for i in [:num_trials] do
-    let ct <- run <| @sv1_privMax_PMF PureDPSystem laplace_pureDPSystem num den data
+    let ct <- run <| sv1_privMax_PMF num den data
     IO.println s!"#{i} sv1 max: {ct}"
   IO.println ""