Skip to content

Commit

Permalink
sv1_ub
Browse files Browse the repository at this point in the history
  • Loading branch information
markusdemedeiros committed Nov 8, 2024
1 parent b7bd879 commit ede6a0b
Showing 1 changed file with 124 additions and 4 deletions.
128 changes: 124 additions & 4 deletions SampCert/DifferentialPrivacy/Queries/UnboundedMax/Properties.lean
Original file line number Diff line number Diff line change
Expand Up @@ -175,13 +175,133 @@ lemma gen_poisson_trial_lb (C : ℕ -> T → Bool) (F : ℕ × T -> SLang T) (I
-/


lemma sv1_ub ε₁ ε₂ l : ∑'s, sv1_privMax ε₁ ε₂ l s ≤ 1 := by
unfold sv1_privMax
lemma ENNReal.tsum_iSup_comm (f : T -> U -> ENNReal) : ∑' x, ⨆ y, f x y = ⨆ y, ∑' x, f x y := by
-- Make it finite
rw [ENNReal.tsum_eq_iSup_sum]
conv =>
rhs
enter [1, y]
rw [ENNReal.tsum_eq_iSup_sum]
rw [iSup_comm]
apply iSup_congr
intro s

-- rw [Summable.hasSum_iff ENNReal.summable]
-- Definitely true, may be annoying to prove
sorry


sorry
lemma sv1_ub ε₁ ε₂ l : ∑'s, sv1_privMax ε₁ ε₂ l s ≤ 1 := by
unfold sv1_privMax
unfold sv1_threshold
simp
-- Push the sum over s inwards
conv =>
rw [ENNReal.tsum_comm]
enter [1, 1, b]
rw [ENNReal.tsum_mul_left]
enter [2]
rw [ENNReal.tsum_comm]
enter [1, i]
rw [ENNReal.tsum_mul_left]
enter [2]
rw [ENNReal.tsum_comm]
apply
@le_trans _ _ _
(∑' (a : ℤ), (privNoiseThresh ε₁ ε₂) a * ∑' (a_1 : ℤ), (privNoiseGuess ε₁ ε₂) a_1 * 1)
_ ?G2 ?G1
case G1 =>
apply Eq.le
simp
rw [ENNReal.tsum_mul_right]
have R1 : ∑' (a : ℤ), (privNoiseThresh ε₁ ε₂) a = 1 := by
rw [<- Summable.hasSum_iff ENNReal.summable]
cases (privNoiseThresh ε₁ ε₂)
simp [DFunLike.coe, SPMF.instFunLike]
trivial
have R2 : ∑' (a : ℤ), (privNoiseGuess ε₁ ε₂) a = 1 := by
rw [<- Summable.hasSum_iff ENNReal.summable]
cases (privNoiseGuess ε₁ ε₂)
simp [DFunLike.coe, SPMF.instFunLike]
trivial
simp_all
case G2 =>
apply ENNReal.tsum_le_tsum
intro τ
apply ENNReal.mul_left_mono
apply ENNReal.tsum_le_tsum
intro v0
apply ENNReal.mul_left_mono

apply
@le_trans _ _ _
(∑' (b : sv1_state), probWhile (sv1_privMaxC τ l) (sv1_privMaxF ε₁ ε₂) ([], v0) b )
_ ?G3 ?G4
case G3 =>
apply ENNReal.tsum_le_tsum
intro a
rw [tsum_ite_eq]
case G4 =>
unfold probWhile
rw [ENNReal.tsum_iSup_comm]
apply iSup_le_iff.mpr
intro cut
suffices (∀ L, ∑' (x : sv1_state), probWhileCut (sv1_privMaxC τ l) (sv1_privMaxF ε₁ ε₂) cut (L, v0) x ≤ 1) by
apply this
revert v0
induction cut
· simp [probWhileCut]
· rename_i cut' IH
intro v0 L
simp [probWhileCut, probWhileFunctional]
split
· simp
simp [sv1_privMaxF]
conv =>
enter [1, 1, x]
conv =>
enter [1, a]
rw [<- ENNReal.tsum_mul_right]
simp
rw [ENNReal.tsum_comm]
enter [1, b]

apply
@le_trans _ _ _
(∑' (x : sv1_state) (b : ℤ), (privNoiseGuess ε₁ ε₂) b * probWhileCut (sv1_privMaxC τ l) (sv1_privMaxF ε₁ ε₂) cut' (L ++ [v0], b) x)
_ ?G5 ?G6
case G5 =>
apply ENNReal.tsum_le_tsum
intro a
apply ENNReal.tsum_le_tsum
intro b
unfold sv1_state
rw [ENNReal.tsum_eq_add_tsum_ite (L ++ [v0], b)]
simp
conv =>
rhs
rw [<- add_zero (_ * _)]
apply add_le_add
· simp
· simp
intros
aesop
case G6 =>
rw [ENNReal.tsum_comm]
conv =>
enter [1, 1, b]
rw [ENNReal.tsum_mul_left]
apply @le_trans _ _ _ (∑' (b : ℤ), (privNoiseGuess ε₁ ε₂) b * 1)
· apply ENNReal.tsum_le_tsum
intro a
apply ENNReal.mul_left_mono
apply IH
· simp
apply Eq.le
rw [<- Summable.hasSum_iff ENNReal.summable]
cases (privNoiseGuess ε₁ ε₂)
simp [DFunLike.coe, SPMF.instFunLike]
trivial
· simp


/-
Expand Down

0 comments on commit ede6a0b

Please sign in to comment.