Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Upgrade 4.10.0 #66

Merged
merged 2 commits into from
Aug 20, 2024
Merged

Upgrade 4.10.0 #66

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c0cae1a
Update to Lean 4.10
Aug 19, 2024
919bc6f
Fix cdot lint warnings
Aug 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 14 additions & 14 deletions SampCert/DifferentialPrivacy/Generic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,10 +102,10 @@ lemma compose_sum_rw (nq1 : U -> ENNReal) (nq2 : V -> ENNReal) (b : U) (c : V) :
have A : ∀ a : U, ∀ b : U, (∑' (a_1 : V), if b = a ∧ c = a_1 then nq2 a_1 else 0) = if b = a then (∑' (a_1 : V), if c = a_1 then nq2 a_1 else 0) else 0 := by
intro x y
split
. rename_i h
· rename_i h
subst h
simp
. rename_i h
· rename_i h
simp
intro h
contradiction
Expand All @@ -120,12 +120,12 @@ lemma compose_sum_rw (nq1 : U -> ENNReal) (nq2 : V -> ENNReal) (b : U) (c : V) :
have B : ∀ x : U, (if x = b then 0 else if b = x then nq1 x * ∑' (a_1 : V), if c = a_1 then nq2 a_1 else 0 else 0) = 0 := by
intro x
split
. simp
. split
. rename_i h1 h2
· simp
· split
· rename_i h1 h2
subst h2
contradiction
. simp
· simp
conv =>
left
right
Expand All @@ -139,12 +139,12 @@ lemma compose_sum_rw (nq1 : U -> ENNReal) (nq2 : V -> ENNReal) (b : U) (c : V) :
have C :∀ x : V, (if x = c then 0 else if c = x then nq2 x else 0) = 0 := by
intro x
split
. simp
. split
. rename_i h1 h2
· simp
· split
· rename_i h1 h2
subst h2
contradiction
. simp
· simp
conv =>
left
right
Expand All @@ -167,8 +167,8 @@ theorem ENNReal.HasSum_fiberwise {f : T → ENNReal} {a : ENNReal} (hf : HasSum
intro b
have F := @Summable.hasSum_iff ENNReal _ _ _ (fun c => (f ∘ ⇑(Equiv.sigmaFiberEquiv g)) { fst := b, snd := c }) ((fun c => ∑' (b : ↑(g ⁻¹' {c})), f ↑b) b) _
apply (F _).2
. rfl
. apply ENNReal.summable
· rfl
· apply ENNReal.summable

/--
Partition series into fibers. `g` maps an element to its fiber.
Expand Down Expand Up @@ -204,10 +204,10 @@ theorem fiberwisation (p : T → ENNReal) (f : T → V) :
apply tsum_congr
intro b
split
. rename_i h'
· rename_i h'
rw [h']
simp only [tsum_empty]
. simp
· simp

lemma condition_to_subset (f : U → V) (g : U → ENNReal) (x : V) :
(∑' a : U, if x = f a then g a else 0) = ∑' a : { a | x = f a }, g a := by
Expand Down
18 changes: 9 additions & 9 deletions SampCert/DifferentialPrivacy/Pure/DP.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,10 +48,10 @@ theorem singleton_to_event (m : Mechanism T U) (ε : ℝ) (h : DP_singleton m ε
have F := ENNReal.tsum_le_tsum E
rw [ENNReal.tsum_mul_left] at F
rw [← ENNReal.div_le_iff_le_mul] at F
. clear h1 A B C D
· clear h1 A B C D
trivial
. aesop
. right
· aesop
· right
simp
exact Real.exp_pos ε

Expand All @@ -63,18 +63,18 @@ theorem event_to_singleton (m : Mechanism T U) (ε : ℝ) (h : DP m ε) :
replace h1 := h l₁ l₂ h1 {x}
simp at h1
rw [tsum_eq_single x] at h1
. simp at h1
· simp at h1
rw [tsum_eq_single x] at h1
. simp at h1
· simp at h1
trivial
. aesop
. aesop
· aesop
· aesop

theorem event_eq_singleton (m : Mechanism T U) (ε : ℝ) :
DP m ε ↔ DP_singleton m ε := by
constructor
. apply event_to_singleton
. apply singleton_to_event
· apply event_to_singleton
· apply singleton_to_event

lemma PureDP_mono {m : Mechanism T U} {ε₁ ε₂ : NNReal} (H : ε₁ ≤ ε₂) (Hε : PureDP m ε₁) : PureDP m ε₂ := by
rw [PureDP] at *
Expand Down
20 changes: 10 additions & 10 deletions SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ theorem privNoisedQueryPure_DP_bound (query : List T → ℤ) (Δ ε₁ ε₂ :
simp [DiscreteLaplaceGenSamplePMF]
simp [DFunLike.coe, PMF.instFunLike]
rw [← ENNReal.ofReal_div_of_pos]
. apply ofReal_le_ofReal
· apply ofReal_le_ofReal
rw [division_def]
rw [mul_inv]
rw [← mul_assoc]
Expand All @@ -75,7 +75,7 @@ theorem privNoisedQueryPure_DP_bound (query : List T → ℤ) (Δ ε₁ ε₂ :
rw [div_add_div_same]
rw [division_def]
apply (mul_inv_le_iff' _).mpr
. have B : (ε₁ : ℝ) / ε₂ * (Δ * ε₂ / ε₁) = Δ := by
· have B : (ε₁ : ℝ) / ε₂ * (Δ * ε₂ / ε₁) = Δ := by
ring_nf
simp
field_simp
Expand All @@ -96,23 +96,23 @@ theorem privNoisedQueryPure_DP_bound (query : List T → ℤ) (Δ ε₁ ε₂ :
rw [← natAbs_to_abs]
exact Nat.cast_le.mpr bounded_sensitivity

. simp
. rw [_root_.mul_pos_iff]
· simp
· rw [_root_.mul_pos_iff]
left
constructor
. rw [_root_.div_pos_iff]
· rw [_root_.div_pos_iff]
left
have A : 1 < rexp ((ε₁ : ℝ) / (Δ * ε₂)) := by
rw [← exp_zero]
apply exp_lt_exp.mpr
simp
constructor
. simp [A]
. apply @lt_trans _ _ _ 2 _
. simp
. rw [← one_add_one_eq_two]
· simp [A]
· apply @lt_trans _ _ _ 2 _
· simp
· rw [← one_add_one_eq_two]
exact (add_lt_add_iff_right 1).mpr A
. apply exp_pos
· apply exp_pos


/--
Expand Down
8 changes: 4 additions & 4 deletions SampCert/DifferentialPrivacy/Pure/Postprocessing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,14 +33,14 @@ lemma privPostProcess_DP_bound {nq : Mechanism T U} {ε : NNReal} (h : PureDP nq
apply tsum_le_tsum _ ENNReal.summable (by aesop)
intro i
split
. rename_i h
· rename_i h
subst h
refine (ENNReal.div_le_iff_le_mul ?inl.hb0 ?inl.hbt).mp (h i)
. aesop
. right
· aesop
· right
simp
exact Real.exp_pos ε
. simp
· simp

/--
``privPostProcess`` satisfies pure DP, for any surjective postprocessing function.
Expand Down
4 changes: 2 additions & 2 deletions SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ theorem privNoisedBoundedMean_DP (U : ℕ+) (ε₁ ε₂ : ℕ+) :
apply dps.postprocess_prop
rw [budget_split]
apply dps.compose_prop
. apply privNoisedBoundedSum_DP
. apply privNoisedCount_DP
· apply privNoisedBoundedSum_DP
· apply privNoisedCount_DP

end SLang
26 changes: 13 additions & 13 deletions SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,49 +34,49 @@ theorem exactBoundedSum_sensitivity (U : ℕ+) : sensitivity (exactBoundedSum U)
simp
exact Nat.le_total n ↑U
cases H
. rename_i l l' n h1 h2
· rename_i l l' n h1 h2
subst h1 h2
simp
cases A n
. rename_i h
· rename_i h
rw [h]
simp at *
trivial
. rename_i h
· rename_i h
rw [h]
simp
. rename_i l n l' h1 h2
· rename_i l n l' h1 h2
subst h1 h2
simp
cases A n
. rename_i h
· rename_i h
rw [h]
simp at *
trivial
. rename_i h
· rename_i h
rw [h]
simp
. rename_i l n l' m h1 h2
· rename_i l n l' m h1 h2
subst h1 h2
simp
cases A n
. rename_i h
· rename_i h
cases A m
. rename_i h'
· rename_i h'
rw [h, h']
simp at *
apply Int.natAbs_coe_sub_coe_le_of_le h h'
. rename_i h'
· rename_i h'
rw [h, h']
simp at *
apply Int.natAbs_coe_sub_coe_le_of_le h le_rfl
. rename_i h
· rename_i h
cases A m
. rename_i h'
· rename_i h'
rw [h, h']
simp at *
apply Int.natAbs_coe_sub_coe_le_of_le le_rfl h'
. rename_i h'
· rename_i h'
rw [h, h']
simp at *

Expand Down
6 changes: 3 additions & 3 deletions SampCert/DifferentialPrivacy/Queries/Count/Properties.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,13 +30,13 @@ theorem exactCount_1_sensitive :
simp [exactCount, sensitivity]
intros l₁ l₂ H
cases H
. rename_i a b n h1 h2
· rename_i a b n h1 h2
subst h1 h2
simp
. rename_i a b n h1 h2
· rename_i a b n h1 h2
subst h1 h2
simp
. rename_i a n b m h1 h2
· rename_i a n b m h1 h2
subst h1 h2
simp

Expand Down
Loading