From c0cae1a42544249f81c961fa4192ab5b92f73e84 Mon Sep 17 00:00:00 2001 From: Tristan Ravitch Date: Mon, 19 Aug 2024 17:48:55 -0600 Subject: [PATCH 1/2] Update to Lean 4.10 The update involved replacing a few deprecated theorems with other equivalents. The biggest change was that the `Complex.ext_iff` theorem became private in MathLib 4.10, which was required for one theorem. That is temporarily solved with a local copy of `ext_iff`. --- .../DifferentialPrivacy/RenyiDivergence.lean | 8 ++++---- SampCert/Util/Gaussian/GaussBound.lean | 17 ++++++++++++---- Tests/Load.py | 6 +++--- lake-manifest.json | 20 +++++++++---------- lakefile.lean | 2 +- lean-toolchain | 2 +- 6 files changed, 32 insertions(+), 23 deletions(-) diff --git a/SampCert/DifferentialPrivacy/RenyiDivergence.lean b/SampCert/DifferentialPrivacy/RenyiDivergence.lean index 2dcc4b3f..5c77c07e 100644 --- a/SampCert/DifferentialPrivacy/RenyiDivergence.lean +++ b/SampCert/DifferentialPrivacy/RenyiDivergence.lean @@ -572,11 +572,11 @@ lemma Renyi_Jensen_ENNReal_reduct [MeasurableSpace T] [MeasurableSingletonClass . apply measurable_discrete . apply Measurable.inv apply measurable_discrete - · simp [snorm] + · simp [eLpNorm] split · simp · rename_i Hα - simp [snorm'] + simp [eLpNorm'] rw [MeasureTheory.lintegral_countable'] rw [toReal_ofReal (le_of_lt (lt_trans zero_lt_one h))] apply rpow_lt_top_of_nonneg @@ -739,11 +739,11 @@ lemma Renyi_Jensen_ENNReal_converse_reduct [MeasurableSpace T] [MeasurableSingle . apply measurable_discrete . apply Measurable.inv apply measurable_discrete - · simp [snorm] + · simp [eLpNorm] split · simp · rename_i Hα - simp [snorm'] + simp [eLpNorm'] rw [MeasureTheory.lintegral_countable'] rw [toReal_ofReal (le_of_lt (lt_trans zero_lt_one h))] apply rpow_lt_top_of_nonneg diff --git a/SampCert/Util/Gaussian/GaussBound.lean b/SampCert/Util/Gaussian/GaussBound.lean index 917c1bea..63238a5a 100644 --- a/SampCert/Util/Gaussian/GaussBound.lean +++ b/SampCert/Util/Gaussian/GaussBound.lean @@ -25,6 +25,15 @@ open ContinuousMap Function attribute [local instance] Real.fact_zero_lt_one +/- +This is copied from MathLib; it was made private in the release of 4.10 with the suggestion that it would be +auto-generated in 4.11. It wasn't clear if it would become public again at that point. + +See: https://github.com/leanprover-community/mathlib4/pull/15340 +-/ +theorem local_ext_iff {z w : ℂ} : z = w ↔ z.re = w.re ∧ z.im = w.im := + ⟨fun H => by simp [H], fun h => Complex.ext h.1 h.2⟩ + /-- The sum of any gaussian function over ℤ is bounded above by the sum of the mean-zero gaussian function over ℤ. -/ @@ -94,13 +103,13 @@ theorem sum_gauss_term_bound {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) : rw [← Complex.ofReal_mul] rw [← Complex.ofReal_mul] rw [← Complex.ofReal_mul] - rw [ext_iff] + rw [local_ext_iff] constructor - . rw [rpow_def] + · rw [rpow_def] simp - . simp + · simp rw [cpow_inv_two_im_eq_sqrt] - . simp + · simp ring_nf simp rw [← Real.sqrt_zero] diff --git a/Tests/Load.py b/Tests/Load.py index dc2b7cda..8839dbae 100644 --- a/Tests/Load.py +++ b/Tests/Load.py @@ -4,15 +4,15 @@ home = expanduser("~") # Loading Lean's libraries -CDLL(home + "/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/lib/lean/libInit_shared.dylib", RTLD_GLOBAL) -lean = CDLL(home + "/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/lib/lean/libleanshared.dylib", RTLD_GLOBAL) +CDLL(home + "/.elan/toolchains/leanprover--lean4---v4.10.0/lib/lean/libInit_shared.dylib", RTLD_GLOBAL) +lean = CDLL(home + "/.elan/toolchains/leanprover--lean4---v4.10.0/lib/lean/libleanshared.dylib", RTLD_GLOBAL) # import-graph uses some Lake definitions that are available in the lake library, but # Lean does not produce a dynamic version # One needs to create the library # On Mac, it looks like: #clang++ -fpic -shared -Wl,-force_load libLake.a -o libLake_shared.dylib -L . -lleanshared # If you are in the lib/lean directory of your toolchain -CDLL(home + "/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/lib/lean/libLake_shared.dylib", RTLD_GLOBAL) +CDLL(home + "/.elan/toolchains/leanprover--lean4---v4.10.0/lib/lean/libLake_shared.dylib", RTLD_GLOBAL) # Loading Mathlib and its dependencies # To create the dynamic library, for each one of them, run lake build xxx:shared diff --git a/lake-manifest.json b/lake-manifest.json index c06ea209..74dd8bae 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239", + "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", + "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73", + "rev": "209712c78b16c795453b6da7f7adbda4589a8f21", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,27 +35,27 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d1b33202c3a29a079f292de65ea438648123b635", + "rev": "c87908619cccadda23f71262e6898b9893bffa36", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.39", + "inputRev": "v0.0.40", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7", + "rev": "543725b3bfed792097fc134adca628406f6145f5", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "984c68d7773ac133c74543b99b82c33e53baea6b", + "rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.10.0-rc2", + "inputRev": "v4.10.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "sampcert", diff --git a/lakefile.lean b/lakefile.lean index 47a381fa..f918d059 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,7 +5,7 @@ package «sampcert» where -- add any package configuration options here require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "v4.10.0-rc2" + "https://github.com/leanprover-community/mathlib4.git" @ "v4.10.0" @[default_target] lean_lib «SampCert» where diff --git a/lean-toolchain b/lean-toolchain index 6a4259fa..7f0ea50a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.10.0-rc2 +leanprover/lean4:v4.10.0 From 919bc6f7bc463b993e52ad34bc5a91129980249d Mon Sep 17 00:00:00 2001 From: Tristan Ravitch Date: Tue, 20 Aug 2024 12:08:45 -0600 Subject: [PATCH 2/2] Fix cdot lint warnings It seems that this lint check became a default with the release of 4.10. --- SampCert/DifferentialPrivacy/Generic.lean | 28 +- SampCert/DifferentialPrivacy/Pure/DP.lean | 18 +- .../Pure/Mechanism/Properties.lean | 20 +- .../Pure/Postprocessing.lean | 8 +- .../Queries/BoundedMean/Properties.lean | 4 +- .../Queries/BoundedSum/Properties.lean | 26 +- .../Queries/Count/Properties.lean | 6 +- .../DifferentialPrivacy/RenyiDivergence.lean | 72 ++-- .../ZeroConcentrated/ConcentratedBound.lean | 34 +- .../Mechanism/Properties.lean | 4 +- .../ZeroConcentrated/Postprocessing.lean | 18 +- SampCert/Foundations/UniformP2.lean | 8 +- SampCert/Foundations/Until.lean | 58 +-- SampCert/Foundations/While.lean | 12 +- SampCert/Samplers/Bernoulli/Properties.lean | 12 +- .../Properties.lean | 344 +++++++++--------- SampCert/Samplers/Gaussian/Properties.lean | 100 ++--- SampCert/Samplers/GaussianGen/Properties.lean | 12 +- SampCert/Samplers/Geometric/Properties.lean | 96 ++--- SampCert/Samplers/Laplace/Properties.lean | 208 +++++------ SampCert/Samplers/Uniform/Properties.lean | 58 +-- SampCert/Util/Gaussian/DiscreteGaussian.lean | 12 +- SampCert/Util/Gaussian/GaussBound.lean | 6 +- SampCert/Util/Gaussian/GaussPeriodicity.lean | 12 +- SampCert/Util/Log.lean | 2 +- SampCert/Util/Shift.lean | 30 +- SampCert/Util/Util.lean | 42 +-- 27 files changed, 625 insertions(+), 625 deletions(-) diff --git a/SampCert/DifferentialPrivacy/Generic.lean b/SampCert/DifferentialPrivacy/Generic.lean index eb64380f..be8e333c 100644 --- a/SampCert/DifferentialPrivacy/Generic.lean +++ b/SampCert/DifferentialPrivacy/Generic.lean @@ -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 @@ -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 @@ -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 @@ -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. @@ -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 diff --git a/SampCert/DifferentialPrivacy/Pure/DP.lean b/SampCert/DifferentialPrivacy/Pure/DP.lean index d7128a6e..40c33529 100644 --- a/SampCert/DifferentialPrivacy/Pure/DP.lean +++ b/SampCert/DifferentialPrivacy/Pure/DP.lean @@ -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 ε @@ -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 * diff --git a/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean index 32c96cb0..addf1b2f 100644 --- a/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean +++ b/SampCert/DifferentialPrivacy/Pure/Mechanism/Properties.lean @@ -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] @@ -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 @@ -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 /-- diff --git a/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean b/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean index 93817ff0..4e57529a 100644 --- a/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean +++ b/SampCert/DifferentialPrivacy/Pure/Postprocessing.lean @@ -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. diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean index de1567f9..775a6435 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedMean/Properties.lean @@ -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 diff --git a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean index 7f6fb4bc..70e72bfd 100644 --- a/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/BoundedSum/Properties.lean @@ -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 * diff --git a/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean b/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean index 08719827..8257d763 100644 --- a/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean +++ b/SampCert/DifferentialPrivacy/Queries/Count/Properties.lean @@ -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 diff --git a/SampCert/DifferentialPrivacy/RenyiDivergence.lean b/SampCert/DifferentialPrivacy/RenyiDivergence.lean index 5c77c07e..9ff28400 100644 --- a/SampCert/DifferentialPrivacy/RenyiDivergence.lean +++ b/SampCert/DifferentialPrivacy/RenyiDivergence.lean @@ -151,10 +151,10 @@ theorem RenyiDivergenceExpectation (p q : T → ENNReal) {α : ℝ} (h : 1 < α) · -- q x ∈ ℝ+, p x ∈ ℝ+ rename_i Hvp' rw [ENNReal.rpow_sub] - . rw [← ENNReal.mul_comm_div] + · rw [← ENNReal.mul_comm_div] rw [← ENNReal.div_rpow_of_nonneg] - . rw [ENNReal.rpow_one] - . apply le_of_lt (lt_trans Real.zero_lt_one h ) + · rw [ENNReal.rpow_one] + · apply le_of_lt (lt_trans Real.zero_lt_one h ) · simp_all only [some_eq_coe, not_false_eq_true, ne_eq, coe_eq_zero] · simp_all only [some_eq_coe, not_false_eq_true, ne_eq, coe_ne_top] @@ -238,7 +238,7 @@ lemma Integrable_rpow (f : T → ℝ) (nn : ∀ x : T, 0 ≤ f x) (μ : Measure intro X simp [Integrable] at * constructor - . cases X + · cases X rename_i left right rw [@aestronglyMeasurable_iff_aemeasurable] apply AEMeasurable.pow_const @@ -247,7 +247,7 @@ lemma Integrable_rpow (f : T → ℝ) (nn : ∀ x : T, 0 ≤ f x) (μ : Measure rename_i left' right' rw [aestronglyMeasurable_iff_aemeasurable] at left' simp [left'] - . rw [← hasFiniteIntegral_norm_iff] + · rw [← hasFiniteIntegral_norm_iff] simp [X] -- MARKUSDE: This lemma is derivable from ``Renyi_Jensen_strict_real``, however it requires a reduction @@ -271,17 +271,17 @@ theorem Renyi_Jensen_real (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 < α) (h have A := @convexOn_rpow α (le_of_lt h) have B : ContinuousOn (fun (x : ℝ) => x ^ α) (Set.Ici 0) := by apply ContinuousOn.rpow - . exact continuousOn_id' (Set.Ici 0) - . exact continuousOn_const - . intro x h' + · exact continuousOn_id' (Set.Ici 0) + · exact continuousOn_const + · intro x h' simp at h' have OR : x = 0 ∨ 0 < x := by exact LE.le.eq_or_gt h' cases OR - . rename_i h'' + · rename_i h'' subst h'' right apply lt_trans zero_lt_one h - . rename_i h'' + · rename_i h'' left by_contra rename_i h3 @@ -292,11 +292,11 @@ theorem Renyi_Jensen_real (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 < α) (h have D := @ConvexOn.map_integral_le T ℝ t1 _ _ _ (PMF.toMeasure q) (Set.Ici 0) f (fun (x : ℝ) => x ^ α) (PMF.toMeasure.isProbabilityMeasure q) A B C simp at D apply D - . exact MeasureTheory.ae_of_all (PMF.toMeasure q) h2 - . apply MeasureTheory.Memℒp.integrable _ mem + · exact MeasureTheory.ae_of_all (PMF.toMeasure q) h2 + · apply MeasureTheory.Memℒp.integrable _ mem rw [one_le_ofReal] apply le_of_lt h - . rw [Function.comp_def] + · rw [Function.comp_def] have X : ENNReal.ofReal α ≠ 0 := by simp apply lt_trans zero_lt_one h @@ -304,20 +304,20 @@ theorem Renyi_Jensen_real (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 < α) (h simp have Z := @Integrable_rpow T t1 f h2 (PMF.toMeasure q) (ENNReal.ofReal α) mem X Y rw [toReal_ofReal] at Z - . exact Z - . apply le_of_lt + · exact Z + · apply le_of_lt apply lt_trans zero_lt_one h - . have X : ENNReal.ofReal α ≠ 0 := by + · have X : ENNReal.ofReal α ≠ 0 := by simp apply lt_trans zero_lt_one h have Y : ENNReal.ofReal α ≠ ⊤ := by simp have Z := @Integrable_rpow T t1 f h2 (PMF.toMeasure q) (ENNReal.ofReal α) mem X Y rw [toReal_ofReal] at Z - . exact Z - . apply le_of_lt + · exact Z + · apply le_of_lt apply lt_trans zero_lt_one h - . apply MeasureTheory.Memℒp.integrable _ mem + · apply MeasureTheory.Memℒp.integrable _ mem rw [one_le_ofReal] apply le_of_lt h @@ -342,17 +342,17 @@ theorem Renyi_Jensen_strict_real (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 < have B : ContinuousOn (fun (x : ℝ) => x ^ α) (Set.Ici 0) := by apply ContinuousOn.rpow - . exact continuousOn_id' (Set.Ici 0) - . exact continuousOn_const - . intro x h' + · exact continuousOn_id' (Set.Ici 0) + · exact continuousOn_const + · intro x h' simp at h' have OR : x = 0 ∨ 0 < x := by exact LE.le.eq_or_gt h' cases OR - . rename_i h'' + · rename_i h'' subst h'' right apply lt_trans zero_lt_one h - . rename_i h'' + · rename_i h'' left by_contra rename_i h3 @@ -376,8 +376,8 @@ theorem Renyi_Jensen_strict_real (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 < simp have Z := @Integrable_rpow T t1 f h2 (PMF.toMeasure q) (ENNReal.ofReal α) mem X Y rw [toReal_ofReal] at Z - . exact Z - . apply le_of_lt + · exact Z + · apply le_of_lt apply lt_trans zero_lt_one h simp at D · cases D @@ -437,17 +437,17 @@ theorem Renyi_Jensen_strict_real (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 < rw [<- MeasureTheory.integral_average] simp apply HR - . have X : ENNReal.ofReal α ≠ 0 := by + · have X : ENNReal.ofReal α ≠ 0 := by simp apply lt_trans zero_lt_one h have Y : ENNReal.ofReal α ≠ ⊤ := by simp have Z := @Integrable_rpow T t1 f h2 (PMF.toMeasure q) (ENNReal.ofReal α) mem X Y rw [toReal_ofReal] at Z - . exact Z - . apply le_of_lt + · exact Z + · apply le_of_lt apply lt_trans zero_lt_one h - . apply MeasureTheory.Memℒp.integrable _ mem + · apply MeasureTheory.Memℒp.integrable _ mem rw [one_le_ofReal] apply le_of_lt h @@ -561,7 +561,7 @@ lemma Renyi_Jensen_ENNReal_reduct [MeasurableSpace T] [MeasurableSingletonClass · simp [Renyi_Jensen_f] · simp [Memℒp] constructor - . apply MeasureTheory.StronglyMeasurable.aestronglyMeasurable + · apply MeasureTheory.StronglyMeasurable.aestronglyMeasurable apply Measurable.stronglyMeasurable apply Measurable.ennreal_toReal conv => @@ -569,8 +569,8 @@ lemma Renyi_Jensen_ENNReal_reduct [MeasurableSpace T] [MeasurableSingletonClass intro x rw [division_def] apply Measurable.mul - . apply measurable_discrete - . apply Measurable.inv + · apply measurable_discrete + · apply Measurable.inv apply measurable_discrete · simp [eLpNorm] split @@ -728,7 +728,7 @@ lemma Renyi_Jensen_ENNReal_converse_reduct [MeasurableSpace T] [MeasurableSingle -- ℒp bound (same as forward proof) simp [Memℒp] constructor - . apply MeasureTheory.StronglyMeasurable.aestronglyMeasurable + · apply MeasureTheory.StronglyMeasurable.aestronglyMeasurable apply Measurable.stronglyMeasurable apply Measurable.ennreal_toReal conv => @@ -736,8 +736,8 @@ lemma Renyi_Jensen_ENNReal_converse_reduct [MeasurableSpace T] [MeasurableSingle intro x rw [division_def] apply Measurable.mul - . apply measurable_discrete - . apply Measurable.inv + · apply measurable_discrete + · apply Measurable.inv apply measurable_discrete · simp [eLpNorm] split diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean index bc851f9e..132b2efc 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean @@ -26,8 +26,8 @@ lemma sg_sum_pos' {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (α : ℝ) : rw [div_pos_iff] left constructor - . apply exp_pos - . apply sum_gauss_term_pos h + · apply exp_pos + · apply sum_gauss_term_pos h lemma SG_Renyi_simplify {σ : ℝ} (h : σ ≠ 0) (μ ν : ℤ) (α : ℝ) : (fun (x : ℤ) => (gauss_term_ℝ σ μ) x / ∑' (x : ℤ), (gauss_term_ℝ σ μ) x) x ^ α * @@ -128,7 +128,7 @@ theorem Renyi_divergence_bound {σ : ℝ} (h : σ ≠ 0) (μ : ℤ) (α : ℝ) ( rw [← Int.cast_zero] apply sum_gauss_term_pos h rw [exp_log] - . conv => + · conv => left ring_nf right @@ -225,8 +225,8 @@ theorem Renyi_divergence_bound {σ : ℝ} (h : σ ≠ 0) (μ : ℤ) (α : ℝ) ( rw [← mul_div_assoc] apply mul_le_of_le_one_right _ G apply exp_nonneg - . apply tsum_pos _ _ 0 _ - . simp -- some of this proof is similar to the one just above and needs to be hoisted + · apply tsum_pos _ _ 0 _ + · simp -- some of this proof is similar to the one just above and needs to be hoisted conv => right intro x @@ -275,18 +275,18 @@ theorem Renyi_divergence_bound {σ : ℝ} (h : σ ≠ 0) (μ : ℤ) (α : ℝ) ( rw [exp_add] apply Summable.mul_right apply summable_gauss_term' h - . intro i + · intro i apply le_of_lt rw [mul_pos_iff] left constructor - . apply sg_sum_pos' h - . apply sg_sum_pos' h - . rw [mul_pos_iff] + · apply sg_sum_pos' h + · apply sg_sum_pos' h + · rw [mul_pos_iff] left constructor - . apply sg_sum_pos' h - . apply sg_sum_pos' h + · apply sg_sum_pos' h + · apply sg_sum_pos' h lemma sg_mul_simplify (ss : ℝ) (x μ ν : ℤ) : rexp (-(x - μ) ^ 2 / (2 * ss)) ^ α * rexp (-(x - ν) ^ 2 / (2 * ss)) ^ (1 - α) @@ -357,14 +357,14 @@ lemma SG_Renyi_shift {σ : ℝ} (h : σ ≠ 0) (α : ℝ) (μ ν τ : ℤ) : rw [sg_mul_simplify] rw [← tsum_shift _ (-τ)] - . apply tsum_congr + · apply tsum_congr intro b congr 6 - . simp + · simp ring_nf - . simp + · simp ring_nf - . intro β + · intro β conv => right intro x @@ -434,8 +434,8 @@ theorem Renyi_sum_SG_nonneg {σ α : ℝ} (h : σ ≠ 0) (μ ν n : ℤ) : rw [mul_nonneg_iff] left constructor - . apply Real.rpow_nonneg A - . apply Real.rpow_nonneg B + · apply Real.rpow_nonneg A + · apply Real.rpow_nonneg B /-- Sum in Renyi divergence between discrete Gaussians is well-defined. diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean index 09c13880..d3653614 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean @@ -191,10 +191,10 @@ lemma discrete_gaussian_shift {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (τ x : ℤ) discrete_gaussian σ μ (x - τ) = discrete_gaussian σ (μ + τ) (x) := by simp [discrete_gaussian] congr 1 - . simp [gauss_term_ℝ] + · simp [gauss_term_ℝ] congr 3 ring_nf - . rw [shifted_gauss_sum h] + · rw [shifted_gauss_sum h] /-- privNoisedQuery preserves absolute continuity between neighbours diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean index ebb68722..6ebaacb2 100644 --- a/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean +++ b/SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean @@ -84,8 +84,8 @@ theorem norm_simplify (x : ENNReal) (h : x ≠ ⊤) : @nnnorm ℝ SeminormedAddGroup.toNNNorm x.toReal = x := by simp [nnnorm] cases x - . contradiction - . rename_i v + · contradiction + · rename_i v simp rfl @@ -95,12 +95,12 @@ theorem convergent_subset {p : T → ENNReal} (f : T → V) (conv : ∑' (x : T) rw [← condition_to_subset] have A : (∑' (y : T), if x = f y then p y else 0) ≤ ∑' (x : T), p x := by apply tsum_le_tsum - . intro i + · intro i split - . trivial - . simp only [_root_.zero_le] - . exact ENNReal.summable - . exact ENNReal.summable + · trivial + · simp only [_root_.zero_le] + · exact ENNReal.summable + · exact ENNReal.summable rw [← lt_top_iff_ne_top] apply lt_of_le_of_lt A rw [lt_top_iff_ne_top] @@ -208,8 +208,8 @@ theorem privPostPocess_DP_pre_reduct {U : Type} [m2 : MeasurableSpace U] [count rename_i z w exists z constructor - . trivial - . exact Hl z + · trivial + · exact Hl z simp let δF₁ := (δpmf (nq l₁) f i (nq_restriction_nzs l₁ Hnq2) nq_restriction_nts1) diff --git a/SampCert/Foundations/UniformP2.lean b/SampCert/Foundations/UniformP2.lean index ebe1424e..2bc7c194 100644 --- a/SampCert/Foundations/UniformP2.lean +++ b/SampCert/Foundations/UniformP2.lean @@ -46,9 +46,9 @@ theorem UniformPowerOfTwoSample_apply' (n : PNat) (x : Nat) (h : x ≥ 2 ^ (log lemma if_simpl_up2 (n : PNat) (x x_1: Fin (2 ^ log 2 ↑n)) : (@ite ENNReal (x_1 = x) (propDecidable (x_1 = x)) 0 (@ite ENNReal ((@Fin.val (2 ^ log 2 ↑n) x) = (@Fin.val (2 ^ log 2 ↑n) x_1)) (propDecidable ((@Fin.val (2 ^ log 2 ↑n) x) = (@Fin.val (2 ^ log 2 ↑n) x_1))) 1 0)) = 0 := by split - . simp - . split - . rename_i h1 h2 + · simp + · split + · rename_i h1 h2 cases x rename_i x p cases x_1 @@ -56,7 +56,7 @@ lemma if_simpl_up2 (n : PNat) (x x_1: Fin (2 ^ log 2 ↑n)) : simp at * subst h2 contradiction - . simp + · simp /-- The ``SLang`` term ``uniformPowerOfTwo`` is a proper distribution on ``ℕ``. diff --git a/SampCert/Foundations/Until.lean b/SampCert/Foundations/Until.lean index 17da4dde..72a5e532 100644 --- a/SampCert/Foundations/Until.lean +++ b/SampCert/Foundations/Until.lean @@ -43,20 +43,20 @@ theorem probUntilCut_apply_unsat (body : SLang T) (cond : T → Bool) (fuel : probWhileCut (fun v => decide (cond v = false)) (fun _ => body) fuel i x = 0 := by revert i induction fuel - . simp only [zero_eq, probUntilCut_zero, implies_true] - . rename_i fuel IH + · simp only [zero_eq, probUntilCut_zero, implies_true] + · rename_i fuel IH intro j simp only [probWhileCut, probWhileFunctional, decide_eq_true_eq, Bind.bind, Pure.pure, ite_apply, bind_apply, pure_apply] split - . simp only [IH, mul_zero, tsum_zero] - . rename_i h' + · simp only [IH, mul_zero, tsum_zero] + · rename_i h' split - . rename_i h' + · rename_i h' subst h' simp at h' simp [h'] at h - . simp + · simp /-- ``probUntil`` evaluates to zero at all values which do not satisfy ``cond``. @@ -74,14 +74,14 @@ theorem probUntil_apply_unsat (body : SLang T) (cond : T → Bool) (x : T) (h : lemma if_simpl (body : SLang T) (cond : T → Bool) (x_1 x : T) : (if x_1 = x then 0 else if cond x_1 = true then if x = x_1 then body x_1 else 0 else 0) = 0 := by split - . simp - . split - . split - . rename_i h1 h2 h3 + · simp + · split + · split + · rename_i h1 h2 h3 subst h3 contradiction - . simp - . simp + · simp + · simp -- Dead code theorem repeat_1 (body : SLang T) (cond : T → Bool) (x : T) (h : cond x) : @@ -113,14 +113,14 @@ lemma tsum_split_ite_exp (cond : T → Bool) (f g : T → ENNReal) : apply tsum_congr intro b split - . split - . rename_i h h' + · split + · rename_i h h' rw [h'] at h contradiction - . simp - . split - . simp - . rename_i h h' + · simp + · split + · simp + · rename_i h h' simp at h' rw [h'] at h contradiction @@ -129,8 +129,8 @@ theorem probUntilCut_closed_form (body : SLang T) (cond : T → Bool) (fuel : ∑' (i : T), body i * probWhileCut (fun v => decide (cond v = false)) (fun _ => body) fuel i x = ∑ i in range fuel, body x * (∑' x : T, if cond x then 0 else body x)^i := by induction fuel - . simp only [zero_eq, probUntilCut_zero, mul_zero, tsum_zero, range_zero, sum_empty] - . rename_i fuel IH + · simp only [zero_eq, probUntilCut_zero, mul_zero, tsum_zero, range_zero, sum_empty] + · rename_i fuel IH unfold probWhileCut unfold probWhileFunctional simp only [decide_eq_true_eq, Bind.bind, Pure.pure, ite_apply, bind_apply, pure_apply, mul_ite, @@ -173,8 +173,8 @@ theorem probUntilCut_closed_form (body : SLang T) (cond : T → Bool) (fuel : (body i) 0 * (body x * ∑ i in range fuel, (∑' (x : T), @ite ℝ≥0∞ (cond x = true) (instDecidableEqBool (cond x) true) 0 (body x)) ^ i) := by intro i split - . simp - . simp + · simp + · simp conv => left right @@ -190,9 +190,9 @@ theorem probUntilCut_closed_form (body : SLang T) (cond : T → Bool) (fuel : congr ext i split - . rename_i h + · rename_i h simp [h] - . rename_i h + · rename_i h simp [h] /-- @@ -241,7 +241,7 @@ theorem probUntil_apply_sat (body : SLang T) (cond : T → Bool) (x : T) (h : co right right intro s - rw [finset_sum_iSup_nat (probUntilCut_monotone body cond x)] + rw [finsetSum_iSup_of_monotone (probUntilCut_monotone body cond x)] rw [iSup_comm] conv => right @@ -260,9 +260,9 @@ theorem probUntil_apply (body : SLang T) (cond : T → Bool) (x : T) : probUntil (body : SLang T) (cond : T → Bool) x = (if cond x then body x else 0) * (1 - ∑' x : T, if cond x then 0 else body x)⁻¹ := by split - . rename_i h + · rename_i h simp [h, probUntil_apply_sat] - . rename_i h + · rename_i h simp [h, probUntil_apply_unsat] /-- @@ -280,8 +280,8 @@ theorem probUntil_apply_norm (body : SLang T) (cond : T → Bool) (x : T) (norm have A : ∀ x, body x = (if cond x then body x else 0) + (if cond x then 0 else body x) := by intro x split - . simp - . simp + · simp + · simp revert norm conv => left diff --git a/SampCert/Foundations/While.lean b/SampCert/Foundations/While.lean index 7bf6f1c6..380d0e0b 100644 --- a/SampCert/Foundations/While.lean +++ b/SampCert/Foundations/While.lean @@ -29,13 +29,13 @@ theorem probWhileCut_monotonic (cond : T → Bool) (body : T → SLang T) (init intro n revert init induction n - . intro init + · intro init simp [probWhileCut] - . rename_i n IH + · rename_i n IH intro init simp [probWhileCut,probWhileFunctional] split - . rename_i COND + · rename_i COND unfold probBind unfold SLang.probPure simp @@ -43,7 +43,7 @@ theorem probWhileCut_monotonic (cond : T → Bool) (body : T → SLang T) (init intro a apply mul_le_mul_left' exact IH a - . simp + · simp /-- The ``probWhile`` term evaluates to the pointwise limit of the ``probWhileCut`` term @@ -55,7 +55,7 @@ theorem probWhile_apply (cond : T → Bool) (body : T → SLang T) (init : T) (x intro H unfold probWhile apply iSup_eq_of_tendsto - . apply probWhileCut_monotonic - . apply H + · apply probWhileCut_monotonic + · apply H end SLang diff --git a/SampCert/Samplers/Bernoulli/Properties.lean b/SampCert/Samplers/Bernoulli/Properties.lean index 7d3c7820..22f9fc18 100644 --- a/SampCert/Samplers/Bernoulli/Properties.lean +++ b/SampCert/Samplers/Bernoulli/Properties.lean @@ -66,12 +66,12 @@ theorem BernoulliSample_apply_false (num : Nat) (den : PNat) (wf : num ≤ den) have A := BernoulliSample_normalizes num den wf rw [tsum_bool, BernoulliSample_apply_true] at A apply ENNReal.eq_sub_of_add_eq - . have B : ↑num / ↑↑den < (⊤ : ENNReal) := by + · have B : ↑num / ↑↑den < (⊤ : ENNReal) := by apply ENNReal.div_lt_top - . simp - . simp + · simp + · simp exact lt_top_iff_ne_top.mp B - . trivial + · trivial /-- Closed form for evaulation of Bernoulli distribution in terms of its paramater ``num/den``. @@ -80,8 +80,8 @@ Closed form for evaulation of Bernoulli distribution in terms of its paramater ` theorem BernoulliSample_apply (num : Nat) (den : PNat) (wf : num ≤ den) (b : Bool) : BernoulliSample num den wf b = if b then ((num : ENNReal) / (den : ENNReal)) else ((1 : ENNReal) - ((num : ENNReal) / (den : ENNReal))) := by cases b - . simp - . simp + · simp + · simp /-- ``SLang`` Bernoulli program is a proper distribution. diff --git a/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean b/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean index 7fd5e301..35efa4ac 100644 --- a/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean +++ b/SampCert/Samplers/BernoulliNegativeExponential/Properties.lean @@ -33,15 +33,15 @@ theorem BernoulliExpNegSampleUnitAux_returns_false (num : ℕ) (den : ℕ+) (fue probWhileCut (fun state => state.1) (BernoulliExpNegSampleUnitLoop num den wf) fuel st (true, r) = 0 := by revert st r induction fuel - . simp [probWhileCut] - . rename_i fuel IH + · simp [probWhileCut] + · rename_i fuel IH intro st r simp [probWhileCut, probWhileFunctional] unfold probBind unfold probPure simp [ite_apply] split - . rename_i h + · rename_i h cases st rename_i b n simp at h @@ -52,7 +52,7 @@ theorem BernoulliExpNegSampleUnitAux_returns_false (num : ℕ) (den : ℕ+) (fue intro a rw [IH a r] simp - . rename_i h + · rename_i h cases st rename_i b n simp at h @@ -64,8 +64,8 @@ theorem BernoulliExpNegSampleUnitAux_ite_simpl (x r : ℕ+) (k : ENNReal) : @ite ENNReal (x = r + 1) (Classical.propDecidable (x = r + 1)) 0 (@ite ENNReal (x = r + 1) (instPNatDecidableEq x (r + 1)) k 0) = 0 := by split - . simp - . simp + · simp + · simp @[simp] theorem BernoulliExpNegSampleUnitAux_succ_true (num : ℕ) (den : ℕ+) (fuel : ℕ) (st : Bool × ℕ+) (r : ℕ+) (wf : num ≤ den) : @@ -78,12 +78,12 @@ theorem BernoulliExpNegSampleUnitAux_succ_true (num : ℕ) (den : ℕ+) (fuel : conv => left congr - . rw [ENNReal.tsum_eq_add_tsum_ite (r + 1)] + · rw [ENNReal.tsum_eq_add_tsum_ite (r + 1)] right right intro x rw [BernoulliExpNegSampleUnitAux_ite_simpl] - . rw [ENNReal.tsum_eq_add_tsum_ite (r + 1)] + · rw [ENNReal.tsum_eq_add_tsum_ite (r + 1)] right right intro x @@ -104,25 +104,25 @@ theorem BernoulliExpNegSampleUnitAux_monotone_counter (num : ℕ) (den : ℕ+) ( probWhileCut (fun state => state.1) (BernoulliExpNegSampleUnitLoop num den wf) fuel st (false, n) = 0 := by revert st induction fuel - . simp - . rename_i fuel IH + · simp + · rename_i fuel IH intro st h1 h2 cases st rename_i stb stn simp at h1 simp at h2 cases stb - . simp + · simp exact Ne.symm (h1 rfl) - . simp [BernoulliExpNegSampleUnitAux_succ_true] + · simp [BernoulliExpNegSampleUnitAux_succ_true] have A : (false, stn + 1) ≠ (false, n) := by simp have OR : n = stn ∨ n < stn := by exact eq_or_lt_of_le h2 cases OR - . rename_i h + · rename_i h subst h exact _root_.ne_of_gt le.refl - . rename_i h + · rename_i h exact _root_.ne_of_gt (le.step h) have B : (true, stn + 1) ≠ (false, n) := by exact (bne_iff_ne (true, stn + 1) (false, n)).mp rfl @@ -171,25 +171,25 @@ theorem BernoulliExpNegSampleUnitAux_progress (num : ℕ) (den : ℕ+) (fuel k : probWhileCut (fun state => state.1) (BernoulliExpNegSampleUnitLoop num den wf) (fuel + 2) (true, plus_one k ) (false, plus_two k fuel ) = (∏ i in range fuel, (num : ENNReal) / ((k + 1 + i) * den)) * (1 - ((num : ENNReal) / ((fuel + k + 1) * den))) := by revert k induction fuel - . intro k + · intro k simp split - . rename_i h + · rename_i h rw [plus_one_prop] simp - . rename_i h + · rename_i h have A : ¬ k + 2 = k + 2 := by conv => right congr - . rw [← plus_two_zero_prop] - . change k + (1 + 1) + · rw [← plus_two_zero_prop] + · change k + (1 + 1) rw [← add_assoc] rw [← plus_one_prop] refine (Function.Injective.ne_iff ?hf).mpr h exact PNat.coe_injective contradiction - . rename_i fuel IH + · rename_i fuel IH intro k rw [BernoulliExpNegSampleUnitAux_succ_true] rw [BernoulliExpNegSampleUnitAux_succ_false] @@ -258,8 +258,8 @@ theorem BernoulliExpNegSampleUnitAux_progress (num : ℕ) (den : ℕ+) (fuel k : theorem adhoc (n : ℕ) (h : n > 1) : n - 2 + 1 = n - 1 := by rw [← tsub_tsub_assoc] - . exact h - . exact le.step le.refl + · exact h + · exact le.step le.refl theorem adhoc' (n : ℕ) (h : n > 1) : (n : ENNReal) - 2 + 1 = (n : ENNReal) - 1 := by @@ -291,7 +291,7 @@ theorem BernoulliExpNegSampleUnitAux_preservation (num : ℕ) (den : ℕ+) (fuel = probWhileCut (fun state => state.1) (BernoulliExpNegSampleUnitLoop num den wf) (fuel + 2) (true, plus_one k ) (false, plus_two k fuel') := by revert fuel' k induction fuel - . intro fuel' k h1 + · intro fuel' k h1 have A : fuel' = 0 := by exact le_zero.mp h1 subst A simp [BernoulliExpNegSampleUnitAux_succ_true] @@ -302,12 +302,12 @@ theorem BernoulliExpNegSampleUnitAux_preservation (num : ℕ) (den : ℕ+) (fuel rename_i h cases h -- similar proof in BernoulliExpNegSampleUnitAux_progress simp [B] - . rename_i fuel IH + · rename_i fuel IH intro fuel' k h1 conv => congr - . rw [BernoulliExpNegSampleUnitAux_succ_true] - . rw [BernoulliExpNegSampleUnitAux_succ_true] + · rw [BernoulliExpNegSampleUnitAux_succ_true] + · rw [BernoulliExpNegSampleUnitAux_succ_true] have A : succ fuel + 1 = fuel + 2 := by exact rfl rw [A] have B : 1 + succ fuel + 1 = 1 + fuel + 2 := by exact rfl @@ -316,14 +316,14 @@ theorem BernoulliExpNegSampleUnitAux_preservation (num : ℕ) (den : ℕ+) (fuel have IH' := IH (fuel' - 1) (k + 1) Pre clear IH cases fuel' - . rw [BernoulliExpNegSampleUnitAux_succ_false] + · rw [BernoulliExpNegSampleUnitAux_succ_false] rw [BernoulliExpNegSampleUnitAux_succ_false] have C : plus_two k Nat.zero = plus_one k + 1 := by -- Useful for cleanup simp [plus_two, plus_one] rfl rw [C] simp - . rename_i fuel' + · rename_i fuel' have C : succ fuel' - 1 = fuel' := by exact rfl rw [C] at IH' have D : plus_two (k + 1) fuel' = plus_two k (succ fuel') := by -- Important example for cleanup @@ -376,15 +376,15 @@ theorem BernoulliExpNegSampleUnitAux_characterization (num : ℕ) (den : ℕ+) ( = (∏ i in range (n - 2), (num : ENNReal) / ((1 + i) * den)) * (1 - ((num : ENNReal) / ((n - 1) * den))) := by revert n induction extra - . simp + · simp intro n h apply BernoulliExpNegSampleUnitAux_progress' num den n wf h - . rename_i extra IH + · rename_i extra IH intro n h have IH' := IH n h clear IH rw [← BernoulliExpNegSampleUnitAux_preservation'] at IH' - . have B : extra + n + 1 = succ extra + n := by + · have B : extra + n + 1 = succ extra + n := by clear IH' clear IH' conv => @@ -395,24 +395,24 @@ theorem BernoulliExpNegSampleUnitAux_characterization (num : ℕ) (den : ℕ+) ( exact one_add extra rw [← B] trivial - . trivial - . exact Nat.le_add_left n extra + · trivial + · exact Nat.le_add_left n extra theorem BernoulliExpNegSampleUnitAux_sup (num : ℕ) (den : ℕ+) (n : ℕ+) (wf : num ≤ den) : ⨆ i, probWhileCut (fun state => state.1) (BernoulliExpNegSampleUnitLoop num den wf) i (true, 1) (false, n) = if n = 1 then 0 else (∏ i in range (n - 2), (num : ENNReal) / ((1 + i) * den)) * (1 - ((num : ENNReal) / ((n - 1) * den))) := by apply iSup_eq_of_tendsto - . apply probWhileCut_monotonic - . rw [Iff.symm (Filter.tendsto_add_atTop_iff_nat n)] + · apply probWhileCut_monotonic + · rw [Iff.symm (Filter.tendsto_add_atTop_iff_nat n)] split - . rename_i h + · rename_i h subst h rw [ENNReal.tendsto_atTop_zero] intro ε _ existsi 0 intro n _ simp [BernoulliExpNegSampleUnitAux_monotone_counter] - . rename_i h + · rename_i h have h' : n > 1 := by by_contra rename_i h' @@ -443,7 +443,7 @@ theorem BernoulliExpNegSampleUnitAux_at_zero (num : ℕ) (den : ℕ+) (wf : num intro b right split - . rename_i h + · rename_i h cases b rename_i b pb subst h @@ -456,14 +456,14 @@ theorem if_simpl' (num : ℕ) (den : ℕ+) (x n : ℕ+) : (@ite ENNReal (x = 1) (instPNatDecidableEq x 1) 0 ((∏ i in range (↑x - 2), ↑num / (((1 : ENNReal) + ↑i) * ↑↑den)) * (1 - ↑num / ((↑↑x - 1) * ↑↑den)))) 0) = 0 := by split - . simp - . split - . split - . simp - . rename_i h1 h2 h3 + · simp + · split + · split + · simp + · rename_i h1 h2 h3 subst h2 contradiction - . simp + · simp theorem BernoulliExpNegSampleUnitAux_apply (num : ℕ) (den : ℕ+) (n : ℕ+) (wf : num ≤ den) : (BernoulliExpNegSampleUnitAux num den wf) n = @@ -536,15 +536,15 @@ theorem gamma_extract (num : Nat) (den : PNat) (n : ℕ) (h : n > 1) : simp clear X Y cases n - . contradiction - . rename_i n + · contradiction + · rename_i n cases n - . contradiction - . rename_i n + · contradiction + · rename_i n clear h induction n - . simp - . rename_i n IH + · simp + · rename_i n IH have A : succ (succ (succ n)) - 2 = succ n := rfl rw [A] rw [prod_range_succ] @@ -553,8 +553,8 @@ theorem gamma_extract (num : Nat) (den : PNat) (n : ℕ) (h : n > 1) : rw [B] at IH rw [IH] rw [ENNReal.mul_inv] - . simp - . simp + · simp + · simp noncomputable def mass (n : ℕ) (γ : ENNReal) := (γ^(n - 2) * (((n - 2)!) : ENNReal)⁻¹) * (1 - (γ * ((n : ENNReal) - 1)⁻¹)) @@ -562,30 +562,30 @@ theorem BernoulliExpNegSampleUnitAux_apply' (num : ℕ) (den : ℕ+) (n : ℕ) ( (BernoulliExpNegSampleUnitAux num den wf) n = mass n γ := by unfold mass cases n - . contradiction - . rename_i n + · contradiction + · rename_i n let m : ℕ+ := ⟨ succ n , by exact Fin.pos { val := n, isLt := le.refl } ⟩ have A : n + 1 = m := rfl rw [A] rw [BernoulliExpNegSampleUnitAux_apply num den m wf] split - . rename_i h' + · rename_i h' rw [h'] at A rw [A] at h contradiction - . rename_i h' + · rename_i h' cases n - . contradiction - . rename_i n + · contradiction + · rename_i n rw [gamma_extract] - . rw [← A] + · rw [← A] simp only [succ_sub_succ_eq_sub, add_tsub_cancel_right, cast_succ, cast_add, cast_one, ne_eq, ENNReal.one_ne_top, not_false_eq_true, ENNReal.add_sub_cancel_right] have B : (n : ENNReal) + 1 ≠ 0 := by exact cast_add_one_ne_zero n have C : (n : ENNReal) + 1 ≠ ⊤ := by simp rw [gamma_extract' num den (↑n + 1) B C] simp only [gam] - . rw [← A] + · rw [← A] simp only [gt_iff_lt, one_lt_succ_succ] noncomputable def mass' (n : ℕ) (γ : ENNReal) := (γ^n * (((n)!) : ENNReal)⁻¹) @@ -598,16 +598,16 @@ theorem mass'_neq_top (n : ℕ) (γ : ENNReal) (h : γ ≠ ⊤) : rw [ENNReal.mul_lt_top_iff] left constructor - . induction n - . simp - . rename_i n IH + · induction n + · simp + · rename_i n IH rw [_root_.pow_succ] rw [ENNReal.mul_lt_top_iff] left constructor - . trivial - . exact Ne.lt_top h - . have A : n ! > 0 := by exact factorial_pos n + · trivial + · exact Ne.lt_top h + · have A : n ! > 0 := by exact factorial_pos n rw [@ENNReal.inv_lt_iff_inv_lt] simp exact A @@ -616,7 +616,7 @@ theorem mass'_series_exp (γ : ENNReal) (h : γ ≠ ⊤) : (∑' (i : ℕ), mass' i γ).toReal = Real.exp (γ.toReal) := by unfold mass' rw [ENNReal.tsum_toReal_eq] - . conv => + · conv => left right intro a @@ -630,7 +630,7 @@ theorem mass'_series_exp (γ : ENNReal) (h : γ ≠ ⊤) : change ((λ x : ℝ => ∑' (a : ℕ), x ^ a / ↑a !) (ENNReal.toReal γ)) rw [← @NormedSpace.exp_eq_tsum_div ℝ ℝ] rw [← Real.exp_eq_exp_ℝ] - . intro a + · intro a apply mass'_neq_top _ _ h theorem mass'_series_converges (γ : ENNReal) (h : γ ≠ ⊤) : @@ -651,8 +651,8 @@ theorem mass'_series_converges' (γ : ENNReal) (h : γ ≠ ⊤) : have C : ∀ n, @ite ENNReal (n = 0) (instDecidableEqNat n 0) 0 (mass' n γ) = @ite ENNReal (n = 0) (Classical.propDecidable (n = 0)) 0 (mass' n γ) := by intro n split - . simp - . simp + · simp + · simp revert B conv => left @@ -671,28 +671,28 @@ theorem mass'_series_converges'_even (γ : ENNReal) (h : γ ≠ ⊤) : (∑' (i : ℕ), mass' (2 * i) γ) ≠ ⊤ := by have A := mass'_series_converges γ h rw [← tsum_even_add_odd] at A - . by_contra h' + · by_contra h' rw [h'] at A simp at A - . exact ENNReal.summable - . exact ENNReal.summable + · exact ENNReal.summable + · exact ENNReal.summable theorem mass'_series_converges'_odd (γ : ENNReal) (h : γ ≠ ⊤) : (∑' (i : ℕ), mass' (2 * i + 1) γ) ≠ ⊤ := by have A := mass'_series_converges γ h rw [← tsum_even_add_odd] at A - . by_contra h' + · by_contra h' rw [h'] at A simp at A - . exact ENNReal.summable - . exact ENNReal.summable + · exact ENNReal.summable + · exact ENNReal.summable theorem mass'_series_exp' (γ : ENNReal) (h : γ ≠ ⊤) : (∑' (i : ℕ), mass' i γ) = ENNReal.ofReal (Real.exp (γ.toReal)) := by rw [← @ENNReal.ofReal_toReal (∑' (i : ℕ), mass' i γ)] - . unfold mass' + · unfold mass' rw [ENNReal.tsum_toReal_eq] - . conv => + · conv => left right right @@ -708,16 +708,16 @@ theorem mass'_series_exp' (γ : ENNReal) (h : γ ≠ ⊤) : change ((λ x : ℝ => ∑' (a : ℕ), x ^ a / ↑a !) (ENNReal.toReal γ)) rw [← @NormedSpace.exp_eq_tsum_div ℝ ℝ] rw [← Real.exp_eq_exp_ℝ] - . intro a + · intro a apply mass'_neq_top _ _ h - . apply mass'_series_converges _ h + · apply mass'_series_converges _ h theorem mass_simpl (n : ℕ) (γ : ENNReal) (h : n ≥ 2) : mass n γ = mass' (n - 2) γ - mass' (n - 1) γ := by unfold mass unfold mass' rw [ENNReal.mul_sub] - . simp only [mul_one] + · simp only [mul_one] rw [mul_mul_mul_comm] conv => left @@ -728,7 +728,7 @@ theorem mass_simpl (n : ℕ) (γ : ENNReal) (h : n ≥ 2) : rw [adhoc n h] congr rw [← ENNReal.mul_inv] - . rw [inv_eq_iff_eq_inv] + · rw [inv_eq_iff_eq_inv] rw [inv_inv] rw [mul_comm] have A := @Nat.mul_factorial_pred (n - 1) (Nat.sub_pos_of_lt h) @@ -737,16 +737,16 @@ theorem mass_simpl (n : ℕ) (γ : ENNReal) (h : n ≥ 2) : clear B rw [← A] simp only [cast_mul, ENNReal.natCast_sub, cast_one] - . simp only [ne_eq, cast_eq_zero, ENNReal.sub_eq_top_iff, ENNReal.natCast_ne_top, + · simp only [ne_eq, cast_eq_zero, ENNReal.sub_eq_top_iff, ENNReal.natCast_ne_top, ENNReal.one_ne_top, not_false_eq_true, and_true, or_true] - . simp only [ne_eq, ENNReal.natCast_ne_top, not_false_eq_true, true_or] - . intro h1 h2 + · simp only [ne_eq, ENNReal.natCast_ne_top, not_false_eq_true, true_or] + · intro h1 h2 rw [ne_iff_lt_or_gt] -- Proof to simplify with mass'_neq_top left rw [ENNReal.mul_lt_top_iff] left constructor - . have X : γ ≠ ⊤ := by + · have X : γ ≠ ⊤ := by by_contra rename_i h subst h @@ -755,43 +755,43 @@ theorem mass_simpl (n : ℕ) (γ : ENNReal) (h : n ≥ 2) : ENNReal.zero_lt_top, not_top_lt] at * clear h1 h2 induction n - . simp only [zero_eq, ge_iff_le, _root_.zero_le, tsub_eq_zero_of_le, _root_.pow_zero, + · simp only [zero_eq, ge_iff_le, _root_.zero_le, tsub_eq_zero_of_le, _root_.pow_zero, ENNReal.one_lt_top] - . rename_i n IH + · rename_i n IH have OR : n = 1 ∨ n ≥ 2 := by clear IH γ X cases n - . simp at h - . rename_i n + · simp at h + · rename_i n cases n - . simp - . rename_i n + · simp + · rename_i n right exact AtLeastTwo.prop cases OR - . rename_i h' + · rename_i h' subst h' simp only [reduceSucc, ge_iff_le, le_refl, tsub_eq_zero_of_le, _root_.pow_zero, ENNReal.one_lt_top] - . rename_i h' + · rename_i h' have IH' := IH h' clear IH have A : succ n - 2 = succ (n - 2) := by cases n - . contradiction - . rename_i n + · contradiction + · rename_i n cases n - . contradiction - . rename_i n + · contradiction + · rename_i n rfl rw [A] rw [_root_.pow_succ] rw [ENNReal.mul_lt_top_iff] left constructor - . exact IH' - . exact Ne.lt_top X - . have A : (n - 2)! > 0 := by exact factorial_pos (n - 2) + · exact IH' + · exact Ne.lt_top X + · have A : (n - 2)! > 0 := by exact factorial_pos (n - 2) rw [@ENNReal.inv_lt_iff_inv_lt] simp only [ENNReal.inv_top, cast_pos] exact A @@ -801,22 +801,22 @@ theorem if_ge_2 (x : ℕ) (num : ℕ) (den : ℕ+) (wf : num ≤ den) (gam : γ (@ite ENNReal (x = 1) (Classical.propDecidable (x = 1)) 0 (BernoulliExpNegSampleUnitAux num den wf x))) = if x = 0 then 0 else if x = 1 then 0 else mass x γ := by split - . simp - . split - . simp - . rename_i h1 h2 + · simp + · split + · simp + · rename_i h1 h2 rw [BernoulliExpNegSampleUnitAux_apply'] - . exact one_lt_iff_ne_zero_and_ne_one.mpr { left := h1, right := h2 } - . exact gam + · exact one_lt_iff_ne_zero_and_ne_one.mpr { left := h1, right := h2 } + · exact gam theorem if_split_minus (x : ℕ) (γ : ENNReal) : (@ite ENNReal (x = 0) (instDecidableEqNat x 0) 0 (@ite ENNReal (x = 1) (instDecidableEqNat x 1) 0 (mass' (x - 2) γ - mass' (x - 1) γ))) = (@ite ENNReal (x = 0) (instDecidableEqNat x 0) 0 (@ite ENNReal (x = 1) (instDecidableEqNat x 1) 0 (mass' (x - 2) γ))) - (@ite ENNReal (x = 0) (instDecidableEqNat x 0) 0 (@ite ENNReal (x = 1) (instDecidableEqNat x 1) 0 (mass' (x - 1) γ))) := by split - . simp - . split - . simp - . simp + · simp + · split + · simp + · simp theorem mass'_antitone (n : ℕ) (γ : ENNReal) (h : γ ≤ 1) : mass' n γ ≥ mass' (n + 1) γ := by @@ -824,7 +824,7 @@ theorem mass'_antitone (n : ℕ) (γ : ENNReal) (h : γ ≤ 1) : rw [pow_add] simp [factorial] rw [ENNReal.mul_inv] - . have A : γ ^ n * γ * (((n : ENNReal) + 1)⁻¹ * (↑n !)⁻¹) = (γ ^ n * (↑n !)⁻¹) * (γ * ((n : ENNReal) + 1)⁻¹) := by + · have A : γ ^ n * γ * (((n : ENNReal) + 1)⁻¹ * (↑n !)⁻¹) = (γ ^ n * (↑n !)⁻¹) * (γ * ((n : ENNReal) + 1)⁻¹) := by rw [mul_assoc] rw [mul_assoc] congr 1 @@ -837,20 +837,20 @@ theorem mass'_antitone (n : ℕ) (γ : ENNReal) (h : γ ≤ 1) : have B := @mul_le_of_le_one_right ENNReal (γ ^ n * (↑n !)⁻¹) (γ * ((n : ENNReal) + 1)⁻¹) _ _ _ _ apply B clear B - . simp - . have C : ((n: ENNReal) + 1)⁻¹ ≤ 1 := by + · simp + · have C : ((n: ENNReal) + 1)⁻¹ ≤ 1 := by simp only [ENNReal.inv_le_one, self_le_add_left] exact mul_le_one' h C - . simp - . simp + · simp + · simp theorem mass'_series_converges'_sub (γ : ENNReal) (h1 : γ ≠ ⊤) (h2 : γ ≤ 1) : ∑' (n : ℕ), (mass' (2 * n) γ - mass' (2 * n + 1) γ) ≠ ⊤ := by rw [ENNReal.tsum_sub] - . have A := mass'_series_converges'_even _ h1 + · have A := mass'_series_converges'_even _ h1 apply ENNReal.sub_ne_top A - . apply mass'_series_converges'_odd _ h1 - . rw [Pi.le_def] + · apply mass'_series_converges'_odd _ h1 + · rw [Pi.le_def] intro i rw [← ge_iff_le] apply mass'_antitone _ _ h2 @@ -864,9 +864,9 @@ theorem γ_ne_top (num : ℕ) (den : ℕ+) (gam : γ = (num : ENNReal) / (den : rw [ENNReal.mul_lt_top_iff] left constructor - . rw [ENNReal.inv_lt_top] + · rw [ENNReal.inv_lt_top] apply NeZero.pos - . apply (cmp_eq_gt_iff _ _).mp + · apply (cmp_eq_gt_iff _ _).mp rfl theorem γ_le_1 (num : ℕ) (den : ℕ+) (wf : num ≤ den) (gam : γ = (num : ENNReal) / (den : ENNReal)) : @@ -886,9 +886,9 @@ theorem γ_le_1 (num : ℕ) (den : ℕ+) (wf : num ≤ den) (gam : γ = (num : E rw [ENNReal.toReal_nat] rw [inv_mul_eq_div] rw [div_le_one] - . rw [cast_le] + · rw [cast_le] exact wf - . simp only [cast_pos, PNat.pos] + · simp only [cast_pos, PNat.pos] theorem BernoulliExpNegSampleUnitAux_normalizes (num : ℕ) (den : ℕ+) (wf : num ≤ den) (gam : γ = (num : ENNReal) / (den : ENNReal)) : ∑' n : ℕ, (BernoulliExpNegSampleUnitAux num den wf) n = 1 := by @@ -909,13 +909,13 @@ theorem BernoulliExpNegSampleUnitAux_normalizes (num : ℕ) (den : ℕ+) (wf : n rw [mass_simpl _ _ (by simp)] simp rw [ENNReal.tsum_sub] - . rw [ENNReal.tsum_eq_add_tsum_ite 0] + · rw [ENNReal.tsum_eq_add_tsum_ite 0] have X := tsum_shift'_1 (fun n => mass' n γ) have A : ∀ n : ℕ, @ite ENNReal (n = 0) (instDecidableEqNat n 0) 0 (mass' n γ) = @ite ENNReal (n = 0) (Classical.propDecidable (n = 0)) 0 (mass' n γ) := by intro n split - . simp - . simp + · simp + · simp conv => left left @@ -925,14 +925,14 @@ theorem BernoulliExpNegSampleUnitAux_normalizes (num : ℕ) (den : ℕ+) (wf : n rw [← A] rw [X] rw [ENNReal.add_sub_cancel_right] - . simp [mass'] - . apply mass'_series_converges' _ (γ_ne_top num den gam) - . apply mass'_series_converges' _ (γ_ne_top num den gam) - . rw [@Pi.le_def] + · simp [mass'] + · apply mass'_series_converges' _ (γ_ne_top num den gam) + · apply mass'_series_converges' _ (γ_ne_top num den gam) + · rw [@Pi.le_def] intro i rw [← ge_iff_le] apply mass'_antitone - . -- γ ≤ 1 + · -- γ ≤ 1 rw [gam] apply γ_le_1 num den wf rfl @@ -940,7 +940,7 @@ theorem series_step_1 (num : Nat) (den : PNat) (wf : num ≤ den) (γ : ENNReal (∑' (a : ℕ), if a % 2 = 0 then BernoulliExpNegSampleUnitAux num den wf a else 0) = (∑' (n : ℕ), mass (2 * (n + 1)) γ) := by rw [← tsum_even_add_odd] - . conv => + · conv => left left right @@ -964,8 +964,8 @@ theorem series_step_1 (num : Nat) (den : PNat) (wf : num ≤ den) (γ : ENNReal have B : ∀ n, @ite ENNReal (n = 0) (instDecidableEqNat n 0) 0 (BernoulliExpNegSampleUnitAux num den wf (2 * n)) = @ite ENNReal (n = 0) (Classical.propDecidable (n = 0)) 0 (BernoulliExpNegSampleUnitAux num den wf (2 * n)) := by intro n split - . simp - . simp + · simp + · simp conv => left right @@ -980,8 +980,8 @@ theorem series_step_1 (num : Nat) (den : PNat) (wf : num ≤ den) (γ : ENNReal right intro k rw [BernoulliExpNegSampleUnitAux_apply' _ _ _ wf (C k) γ gam] - . exact ENNReal.summable - . exact ENNReal.summable + · exact ENNReal.summable + · exact ENNReal.summable theorem series_step_3 (γ : ENNReal) : (∑' n : ℕ, mass (2 * (n + 1)) γ) @@ -1002,12 +1002,12 @@ theorem series_step_4_pre (γ : ENNReal) (h : γ ≠ ⊤) (h' : γ ≤ 1) : (∑' n : ℕ, (mass' (2 * n) γ - mass' (2 * n + 1) γ)) = ENNReal.ofReal (∑' n : ℕ, mass'' n (- γ.toReal)) := by rw [← @ENNReal.ofReal_toReal (∑' (n : ℕ), (mass' (2 * n) γ - mass' (2 * n + 1) γ))] - . rw [ENNReal.tsum_sub] - . congr + · rw [ENNReal.tsum_sub] + · congr rw [ENNReal.toReal_sub_of_le] - . rw [ENNReal.tsum_toReal_eq] - . rw [ENNReal.tsum_toReal_eq] - . unfold mass' + · rw [ENNReal.tsum_toReal_eq] + · rw [ENNReal.tsum_toReal_eq] + · unfold mass' conv => left left @@ -1056,23 +1056,23 @@ theorem series_step_4_pre (γ : ENNReal) (h : γ ≠ ⊤) (h' : γ ≤ 1) : rw [A] rw [tsum_neg] rfl - . intro a + · intro a apply mass'_neq_top _ _ h - . intro a + · intro a apply mass'_neq_top _ _ h - . apply ENNReal.tsum_le_tsum + · apply ENNReal.tsum_le_tsum intro a rw [← ge_iff_le] apply mass'_antitone exact h' - . apply mass'_series_converges'_even _ h - . apply mass'_series_converges'_odd _ h - . rw [Pi.le_def] + · apply mass'_series_converges'_even _ h + · apply mass'_series_converges'_odd _ h + · rw [Pi.le_def] intro i rw [← ge_iff_le] apply mass'_antitone exact h' - . apply mass'_series_converges'_sub _ h + · apply mass'_series_converges'_sub _ h exact h' theorem series_step_4 (γ : ENNReal) (h : γ ≠ ⊤) (h' : γ ≤ 1) : @@ -1093,8 +1093,8 @@ theorem BernoulliExpNegSampleUnit_apply_true (num : Nat) (den : PNat) (wf : num rw [series_step_1 num den wf γ gam] rw [series_step_3 γ] rw [series_step_4 γ] - . apply γ_ne_top num den gam - . apply γ_le_1 num den wf gam + · apply γ_ne_top num den gam + · apply γ_le_1 num den wf gam theorem BernoulliExpNegSampleAux_split (num : Nat) (den : PNat) (wf : num ≤ den) : (∑' (a : ℕ), BernoulliExpNegSampleUnitAux num den wf a) @@ -1106,8 +1106,8 @@ theorem BernoulliExpNegSampleAux_split (num : Nat) (den : PNat) (wf : num ≤ d apply tsum_congr intro b split - . simp - . simp + · simp + · simp theorem BernoulliExpNegSampleUnit_normalizes (num : Nat) (den : PNat) (wf : num ≤ den) (γ : ENNReal) (gam : γ = (num : ENNReal) / (den : ENNReal)) : (∑' b : Bool, (BernoulliExpNegSampleUnit num den wf) b) = 1 := by @@ -1122,14 +1122,14 @@ theorem BernoulliExpNegSampleUnit_apply_false (num : Nat) (den : PNat) (wf : nu simp [tsum_bool] at A rw [BernoulliExpNegSampleUnit_apply_true num den wf γ gam] at A rw [← ENNReal.eq_sub_of_add_eq] - . exact ENNReal.ofReal_ne_top - . trivial + · exact ENNReal.ofReal_ne_top + · trivial theorem BernoulliExpNegSampleGenLoop_normalizes (iter : Nat) : (∑' b : Bool, (BernoulliExpNegSampleGenLoop iter) b) = 1 := by induction iter - . simp [BernoulliExpNegSampleGenLoop, tsum_bool] - . rename_i iter IH + · simp [BernoulliExpNegSampleGenLoop, tsum_bool] + · rename_i iter IH rw [BernoulliExpNegSampleGenLoop] simp [tsum_bool, ite_apply] rw [BernoulliExpNegSampleUnit_apply_true 1 1 le.refl ((1 : ENNReal) / (1 : ENNReal)) (by simp only [div_one, cast_one, PNat.one_coe] )] @@ -1146,12 +1146,12 @@ theorem BernoulliExpNegSampleGenLoop_normalizes (iter : Nat) : theorem BernoulliExpNegSampleGenLoop_apply_true (iter : Nat) : (BernoulliExpNegSampleGenLoop iter) true = ENNReal.ofReal (Real.exp (- iter)) := by induction iter - . simp [BernoulliExpNegSampleGenLoop] - . rename_i iter IH + · simp [BernoulliExpNegSampleGenLoop] + · rename_i iter IH unfold BernoulliExpNegSampleGenLoop split - . contradiction - . rename_i h + · contradiction + · rename_i h simp [h] simp [tsum_bool, IH] clear IH @@ -1160,8 +1160,8 @@ theorem BernoulliExpNegSampleGenLoop_apply_true (iter : Nat) : rw [BernoulliExpNegSampleUnit_apply_true 1 1 (le_refl 1) 1 A] rw [Real.exp_add] rw [ENNReal.ofReal_mul'] - . exact rfl - . apply Real.exp_nonneg (-↑iter) + · exact rfl + · apply Real.exp_nonneg (-↑iter) theorem BernoulliExpNegSampleGenLoop_apply_false (iter : Nat) : (BernoulliExpNegSampleGenLoop iter) false = 1 - ENNReal.ofReal (Real.exp (- iter)) := by @@ -1179,11 +1179,11 @@ theorem BernoulliExpNegSample_normalizes (num : Nat) (den : PNat) : (∑' b : Bool, (BernoulliExpNegSample num den) b) = 1 := by unfold BernoulliExpNegSample split - . rename_i h + · rename_i h have A := BernoulliExpNegSampleUnit_normalizes num den h ((num : NNReal) / (den : NNReal)) rfl simp [tsum_bool] at * rw [A] - . rename_i h + · rename_i h simp [tsum_bool] rw [add_assoc] rw [← mul_add] @@ -1218,17 +1218,17 @@ theorem BernoulliExpNegSample_apply_true (num : Nat) (den : PNat): (BernoulliExpNegSample num den) true = ENNReal.ofReal (Real.exp (- ((num : NNReal) / (den : NNReal)))) := by simp [BernoulliExpNegSample, ite_apply] split - . rename_i h + · rename_i h rw [BernoulliExpNegSampleUnit_apply_true num den h ((num : NNReal) / (den : NNReal)) rfl] congr rw [ENNReal.toReal_div] simp - . rename_i h + · rename_i h simp [tsum_bool] rw [BernoulliExpNegSampleGenLoop_apply_true] rw [BernoulliExpNegSampleUnit_apply_true (num % den) den _ (((num % (den : ℕ)) : NNReal) / (den : NNReal)) rfl] - . rw [← ENNReal.ofReal_mul'] - . rw [← Real.exp_add] + · rw [← ENNReal.ofReal_mul'] + · rw [← Real.exp_add] congr rw [← @neg_add_rev] congr @@ -1237,7 +1237,7 @@ theorem BernoulliExpNegSample_apply_true (num : Nat) (den : PNat): have C := A B rw [← C] rw [← ENNReal.toReal_add] - . clear A C + · clear A C have FOO := Nat.mod_add_div num den have BAR := Nat_eq_to_ENNReal_eq _ _ FOO have QUUX := ENNReal_eq_to_Real_eq _ _ BAR @@ -1260,7 +1260,7 @@ theorem BernoulliExpNegSample_apply_true (num : Nat) (den : PNat): have X : (den : ENNReal) ≠ 0 := NeZero.natCast_ne (↑den) ENNReal have Y : (den : ENNReal) ≠ ⊤ := ENNReal.natCast_ne_top ↑den rw [ENNReal.div_mul_cancel X Y] - . have X : (den : ENNReal) ≠ 0 := NeZero.natCast_ne (↑den) ENNReal + · have X : (den : ENNReal) ≠ 0 := NeZero.natCast_ne (↑den) ENNReal have Z : (den : ENNReal) ≠ ⊤ := ENNReal.natCast_ne_top ↑den clear A B C h rw [← lt_top_iff_ne_top] @@ -1269,8 +1269,8 @@ theorem BernoulliExpNegSample_apply_true (num : Nat) (den : PNat): rw [ENNReal.top_mul (by exact X)] rw [← lt_top_iff_ne_top] at Z exact (cmp_eq_gt_iff (⊤ : ENNReal) ↑(num % ↑den)).mp rfl - . exact ENNReal.ofReal_ne_top - . apply Real.exp_nonneg + · exact ENNReal.ofReal_ne_top + · apply Real.exp_nonneg /-- Evaluation of Bernoulli negative exponential sampler at ``false`` diff --git a/SampCert/Samplers/Gaussian/Properties.lean b/SampCert/Samplers/Gaussian/Properties.lean index 543903a0..f161646c 100644 --- a/SampCert/Samplers/Gaussian/Properties.lean +++ b/SampCert/Samplers/Gaussian/Properties.lean @@ -32,12 +32,12 @@ lemma ite_simpl_gaussian_1 (num den t: ℕ+) (x a : ℤ) : BernoulliExpNegSample (Int.natAbs (Int.sub (|x| * ↑↑t * ↑↑den) ↑↑num) ^ 2) (2 * num * t ^ 2 * den) false else 0) = 0 := by split - . simp - . split - . rename_i h1 h2 + · simp + · split + · rename_i h1 h2 subst h2 contradiction - . simp + · simp lemma ite_simpl_gaussian_2 (num den t: ℕ+) (x a : ℤ) : @ite ENNReal (x = a) (propDecidable (x = a)) 0 @@ -46,12 +46,12 @@ lemma ite_simpl_gaussian_2 (num den t: ℕ+) (x a : ℤ) : BernoulliExpNegSample (Int.natAbs (Int.sub (|x| * ↑↑t * ↑↑den) ↑↑num) ^ 2) (2 * num * t ^ 2 * den) true else 0) = 0 := by split - . simp - . split - . rename_i h1 h2 + · simp + · split + · rename_i h1 h2 subst h2 contradiction - . simp + · simp /-- Gaussian sampling attempt is a proper distribution. @@ -97,8 +97,8 @@ lemma ite_simpl_1' (num den t : PNat) (x : ℤ) (n : ℤ) : ENNReal.ofReal (-(((|x| * t * den).sub num).natAbs ^ 2 / ((2 : ℕ+) * num * (t : ℝ) ^ 2 * den))).exp) 0)) = 0 := by split - . simp - . rename_i h + · simp + · rename_i h simp [h] intro h subst h @@ -121,7 +121,7 @@ theorem DiscreteGaussianSampleLoop_apply_true (num den t : ℕ+) (n : ℤ) (mix simp (config := { contextual := true }) only [↓reduceIte, ite_simpl_1', tsum_zero, add_zero] rw [ENNReal.ofReal_mul] have A : 0 ≤ rexp (-(|↑n| / ↑↑t)) := by apply exp_nonneg - . conv => + · conv => left rw [mul_assoc] right @@ -129,22 +129,22 @@ theorem DiscreteGaussianSampleLoop_apply_true (num den t : ℕ+) (n : ℤ) (mix congr rw [cast_natAbs] simp only [Int.cast_abs] - . rw [div_nonneg_iff] -- always the same + · rw [div_nonneg_iff] -- always the same left simp only [sub_nonneg, one_le_exp_iff, inv_nonneg, cast_nonneg, true_and] apply Right.add_nonneg - . apply exp_nonneg - . simp only [zero_le_one] + · apply exp_nonneg + · simp only [zero_le_one] lemma if_simpl_2' (x_1 x : ℤ) (a : ENNReal) : @ite ENNReal (x_1 = x) (propDecidable (x_1 = x)) 0 (a * (@ite ENNReal (x = x_1) (propDecidable (x = (x_1, true).1))) 1 0) = 0 := by split - . simp - . split - . rename_i h1 h2 + · simp + · split + · rename_i h1 h2 subst h2 contradiction - . simp + · simp lemma alg_auto (num den : ℕ+) (x : ℤ) : ENNReal.ofReal ( @@ -163,7 +163,7 @@ lemma alg_auto (num den : ℕ+) (x : ℤ) : apply cast_add_one_pos rw [← ENNReal.ofReal_mul] - . congr 1 + · congr 1 simp [← exp_add] simp [division_def] rw [(neg_add _ _).symm] @@ -236,7 +236,7 @@ lemma alg_auto (num den : ℕ+) (x : ℤ) : ring - . simp [exp_nonneg] + · simp [exp_nonneg] lemma alg_auto' (num den : ℕ+) (x : ℤ) : -((x : ℝ) ^ 2 * (den : ℝ) ^ 2 / ((2 : ℝ) * (num : ℝ) ^ 2)) = -(x : ℝ) ^ 2 / ((2 : ℝ) * ((num : ℝ) ^ 2 / (den : ℝ) ^ 2)) := by @@ -280,7 +280,7 @@ theorem DiscreteGaussianSample_apply (num : PNat) (den : PNat) (mix : ℕ) (x : rw [ENNReal.tsum_mul_left] rw [ENNReal.mul_inv] - . rw [mul_assoc] + · rw [mul_assoc] conv => left right @@ -288,11 +288,11 @@ theorem DiscreteGaussianSample_apply (num : PNat) (den : PNat) (mix : ℕ) (x : rw [mul_assoc] rw [← mul_assoc] rw [ENNReal.mul_inv_cancel] - . simp only [one_mul] + · simp only [one_mul] rw [mul_comm] rw [← division_def] rw [ENNReal.ofReal_div_of_pos] - . simp only [alg_auto] + · simp only [alg_auto] rw [ENNReal.tsum_mul_left] rw [ENNReal.div_eq_inv_mul] rw [← mul_assoc] @@ -303,7 +303,7 @@ theorem DiscreteGaussianSample_apply (num : PNat) (den : PNat) (mix : ℕ) (x : simp only [exp_pos] have B : ENNReal.ofReal (rexp (-(↑↑num ^ 2 / (2 * ↑↑den ^ 2 * (↑(@HDiv.hDiv ℕ ℕ ℕ instHDiv ↑num ↑den) + 1) ^ 2)))) ≠ ⊤ := by exact ENNReal.ofReal_ne_top - . conv => + · conv => left left rw [mul_comm] @@ -314,60 +314,60 @@ theorem DiscreteGaussianSample_apply (num : PNat) (den : PNat) (mix : ℕ) (x : rw [mul_comm] rw [← division_def] congr - . simp only [alg_auto'] - . conv => + · simp only [alg_auto'] + · conv => left right intro i rw [alg_auto'] rw [← ENNReal.ofReal_tsum_of_nonneg] - . intro n + · intro n simp only [exp_nonneg] - . have A : ((num : ℝ) / (den : ℝ)) ≠ 0 := by + · have A : ((num : ℝ) / (den : ℝ)) ≠ 0 := by simp have Y := @summable_gauss_term' ((num : ℝ) / (den : ℝ)) A 0 unfold gauss_term_ℝ at Y simp at Y exact Y - . left + · left simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le] simp only [exp_pos] - . left + · left exact ENNReal.ofReal_ne_top - . apply tsum_pos - . have A : ((num : ℝ) / (den : ℝ)) ≠ 0 := by + · apply tsum_pos + · have A : ((num : ℝ) / (den : ℝ)) ≠ 0 := by simp have Y := @summable_gauss_term' ((num : ℝ) / (den : ℝ)) A 0 unfold gauss_term_ℝ at Y simp at Y exact Y - . intro i + · intro i simp only [exp_nonneg] - . simp only [exp_pos] - . exact 0 - . refine pos_iff_ne_zero.mp ?h0.a + · simp only [exp_pos] + · exact 0 + · refine pos_iff_ne_zero.mp ?h0.a simp only [ENNReal.ofReal_pos] rw [div_pos_iff] left simp only [sub_pos, one_lt_exp_iff, inv_pos] constructor - . apply cast_add_one_pos - . apply Right.add_pos_of_pos_of_nonneg - . simp only [exp_pos] - . simp only [zero_le_one] - . exact ENNReal.ofReal_ne_top - . left + · apply cast_add_one_pos + · apply Right.add_pos_of_pos_of_nonneg + · simp only [exp_pos] + · simp only [zero_le_one] + · exact ENNReal.ofReal_ne_top + · left apply zero_lt_iff.mp simp only [ENNReal.ofReal_pos] rw [div_pos_iff] left simp only [sub_pos, one_lt_exp_iff, inv_pos] constructor - . apply cast_add_one_pos - . apply Right.add_pos_of_pos_of_nonneg - . simp only [exp_pos] - . simp only [zero_le_one] - . left + · apply cast_add_one_pos + · apply Right.add_pos_of_pos_of_nonneg + · simp only [exp_pos] + · simp only [zero_le_one] + · left exact ENNReal.ofReal_ne_top /-- @@ -384,12 +384,12 @@ theorem DiscreteGaussianSample_normalizes (num : PNat) (den : PNat) (mix : ℕ) intro x rw [DiscreteGaussianSample_apply] rw [← ENNReal.ofReal_tsum_of_nonneg] - . rw [ENNReal.ofReal_one.symm] + · rw [ENNReal.ofReal_one.symm] congr 1 apply discrete_gaussian_normalizes A - . intro n + · intro n apply discrete_gaussian_nonneg A 0 n - . apply discrete_gaussian_summable A + · apply discrete_gaussian_summable A theorem DiscreteGaussianSample_HasSum1 (num : PNat) (den : PNat) (mix : ℕ) : HasSum (DiscreteGaussianSample num den mix) 1 := by diff --git a/SampCert/Samplers/GaussianGen/Properties.lean b/SampCert/Samplers/GaussianGen/Properties.lean index 9db662f5..ab23754f 100644 --- a/SampCert/Samplers/GaussianGen/Properties.lean +++ b/SampCert/Samplers/GaussianGen/Properties.lean @@ -24,12 +24,12 @@ lemma if_simple_GaussianGen (x_1 x μ : ℤ) : (@ite ENNReal (x = x_1 + μ) (x.instDecidableEq (x_1 + μ)) (ENNReal.ofReal (gauss_term_ℝ (↑↑num / ↑↑den) 0 ↑x_1 / ∑' (x : ℤ), gauss_term_ℝ (↑↑num / ↑↑den) 0 ↑x)) 0)) = 0 := by split - . simp - . split - . rename_i h1 h2 + · simp + · split + · rename_i h1 h2 subst h2 simp at h1 - . simp + · simp /-- ``SLang`` general discrete gaussian term evaluates according to the mathematical ``discrete_gaussian`` distribution. @@ -50,8 +50,8 @@ theorem DiscreteGaussianGenSample_apply (num : PNat) (den : PNat) (μ x : ℤ) : rw [if_simple_GaussianGen] simp only [tsum_zero, add_zero] congr 2 - . simp [gauss_term_ℝ] - . rw [shifted_gauss_sum_0 A] + · simp [gauss_term_ℝ] + · rw [shifted_gauss_sum_0 A] /-- DiscreteGaussianGen has sum 1 diff --git a/SampCert/Samplers/Geometric/Properties.lean b/SampCert/Samplers/Geometric/Properties.lean index ca31f6ef..623e009e 100644 --- a/SampCert/Samplers/Geometric/Properties.lean +++ b/SampCert/Samplers/Geometric/Properties.lean @@ -34,16 +34,16 @@ lemma trial_one_minus : by_contra h rw [← trial_spec] at h rw [ENNReal.add_sub_cancel_right] at h - . contradiction - . by_contra h' + · contradiction + · by_contra h' rw [h'] at trial_spec simp at trial_spec lemma trial_le_1 (i : ℕ) : trial true ^ i ≤ 1 := by induction i - . simp - . rename_i i IH + · simp + · rename_i i IH rw [_root_.pow_succ] have A : trial true ≤ 1 := by by_contra h @@ -89,8 +89,8 @@ theorem geometric_zero (st₁ st₂ : Bool × ℕ) : lemma ite_simpl (x a : ℕ) (v : ENNReal) : (@ite ENNReal (x = a) (propDecidable (x = a)) 0 (@ite ENNReal (x = a) (instDecidableEqNat x a) v 0)) = 0 := by split - . simp - . simp + · simp + · simp /-- Inductive formula for an unrolling of ``probGeometric`` starting in a ``(true, -)`` state. @@ -104,13 +104,13 @@ theorem geometric_succ_true (fuel n : ℕ) (st : Bool × ℕ) : simp [probWhileCut, probWhileFunctional, geoLoopCond, geoLoopBody, ite_apply, ENNReal.tsum_prod', tsum_bool] conv => left - . congr - . rw [ENNReal.tsum_eq_add_tsum_ite (n + 1)] + · congr + · rw [ENNReal.tsum_eq_add_tsum_ite (n + 1)] right right intro x rw [ite_simpl] - . rw [ENNReal.tsum_eq_add_tsum_ite (n + 1)] + · rw [ENNReal.tsum_eq_add_tsum_ite (n + 1)] right right intro x @@ -135,34 +135,34 @@ theorem geometric_monotone_counter (fuel n : ℕ) (st : Bool × ℕ) (h1 : st probWhileCut geoLoopCond (geoLoopBody trial) fuel st (false, n) = 0 := by revert st induction fuel - . simp - . rename_i fuel IH + · simp + · rename_i fuel IH intro st h1 h2 cases st rename_i stb stn simp at h1 simp at h2 cases stb - . simp + · simp exact Ne.symm (h1 rfl) - . simp [geometric_succ_true] + · simp [geometric_succ_true] have A : (false, stn + 1) ≠ (false, n) := by simp have OR : n = stn ∨ n < stn := by exact Nat.eq_or_lt_of_le h2 cases OR - . rename_i h + · rename_i h subst h exact Nat.ne_of_gt le.refl - . rename_i h + · rename_i h exact Nat.ne_of_gt (le.step h) have B : (true, stn + 1) ≠ (false, n) := by exact (bne_iff_ne (true, stn + 1) (false, n)).mp rfl rw [IH _ A] rw [IH _ B] - . simp - . simp + · simp + · simp exact le.step h2 - . simp + · simp exact le.step h2 /-- @@ -173,9 +173,9 @@ theorem geometric_progress (fuel n : ℕ) : probWhileCut geoLoopCond (geoLoopBody trial) (fuel + 2) (true,n) (false,n + fuel + 1) = (trial true)^fuel * (trial false) := by revert n induction fuel - . intro n + · intro n simp [geometric_succ_true] - . rename_i fuel IH + · rename_i fuel IH intro n rw [geometric_succ_true] have A : succ fuel + 1 = fuel + 2 := by exact rfl @@ -212,16 +212,16 @@ theorem geometric_preservation (fuel fuel' n : ℕ) (h1 : fuel ≥ fuel') : probWhileCut geoLoopCond (geoLoopBody trial) (fuel + 2) (true,n) (false,n + fuel' + 1) := by revert fuel' n induction fuel - . intro fuel' n h1 + · intro fuel' n h1 have A : fuel' = 0 := by exact le_zero.mp h1 subst A simp [geometric_succ_true] - . rename_i fuel IH + · rename_i fuel IH intro fuel' n h1 conv => congr - . rw [geometric_succ_true] - . rw [geometric_succ_true] + · rw [geometric_succ_true] + · rw [geometric_succ_true] have A : succ fuel + 1 = fuel + 2 := by exact rfl rw [A] have B : 1 + succ fuel + 1 = 1 + fuel + 2 := by exact rfl @@ -229,8 +229,8 @@ theorem geometric_preservation (fuel fuel' n : ℕ) (h1 : fuel ≥ fuel') : have Pre : fuel ≥ fuel' - 1 := by exact sub_le_of_le_add h1 have IH' := IH (fuel' - 1) (n + 1) Pre cases fuel' - . simp at * - . rename_i fuel' + · simp at * + · rename_i fuel' have C : succ fuel' - 1 = fuel' := by exact rfl rw [C] at IH' have D : n + 1 + fuel' + 1 = n + succ fuel' + 1 := by exact @@ -284,21 +284,21 @@ theorem geometric_characterization (n extra : ℕ) (h : ¬ n = 0) : probWhileCut geoLoopCond (geoLoopBody trial) (extra + (n + 1)) (true,0) (false,n) = (trial true)^(n-1) * (trial false) := by revert n induction extra - . simp + · simp intro n h apply geometric_progress' trial _ h - . rename_i extra IH + · rename_i extra IH intro n h have IH' := IH n h clear IH have A : extra + (n + 1) = (extra + n) + 1 := by exact rfl rw [A] at IH' rw [← geometric_preservation'] at IH' - . have B : succ extra + (n + 1) = extra + n + 2 := by exact succ_add_eq_add_succ extra (n + 1) + · have B : succ extra + (n + 1) = extra + n + 2 := by exact succ_add_eq_add_succ extra (n + 1) rw [B] trivial - . trivial - . exact Nat.le_add_left n extra + · trivial + · exact Nat.le_add_left n extra /-- Closed form for the limit of terminiating executions of truncated ``probGeometric``. @@ -306,17 +306,17 @@ Closed form for the limit of terminiating executions of truncated ``probGeometri theorem geometric_pwc_sup (n : ℕ) : ⨆ i, probWhileCut geoLoopCond (geoLoopBody trial) i (true, 0) (false, n) = if n = 0 then 0 else (trial true)^(n-1) * (trial false) := by refine iSup_eq_of_tendsto ?hf ?_ - . apply probWhileCut_monotonic - . rw [Iff.symm (Filter.tendsto_add_atTop_iff_nat (n + 1))] + · apply probWhileCut_monotonic + · rw [Iff.symm (Filter.tendsto_add_atTop_iff_nat (n + 1))] split - . rename_i h + · rename_i h subst h rw [ENNReal.tendsto_atTop_zero] intro ε _ existsi 0 intro n _ simp [geometric_monotone_counter] - . rename_i h + · rename_i h conv => congr intro E @@ -331,19 +331,19 @@ theorem geometric_returns_false (n fuel k : ℕ) (b : Bool) : probWhileCut geoLoopCond (geoLoopBody trial) fuel (b, k) (true,n) = 0 := by revert n b k induction fuel - . intro n + · intro n simp - . rename_i fuel IH + · rename_i fuel IH intro n k b simp [probWhileCut,probWhileFunctional,geoLoopBody,geoLoopCond] unfold probBind unfold probPure simp [ite_apply] split - . rename_i h + · rename_i h subst h simp [IH] - . rename_i h + · rename_i h simp at h subst h simp [IH] @@ -351,14 +351,14 @@ theorem geometric_returns_false (n fuel k : ℕ) (b : Bool) : lemma if_simpl_geo (x n : ℕ) : (@ite ENNReal (x = n) (propDecidable (x = n)) 0 (@ite ENNReal (x = 0) (instDecidableEqNat x 0) 0 ((trial true ^ (x - 1) * trial false) * (@ite ENNReal (n = x) (propDecidable (n = (false, x).2)) 1 0)))) = 0 := by split - . simp - . split - . simp - . split - . rename_i h + · simp + · split + · simp + · split + · rename_i h subst h contradiction - . simp + · simp /-- Closed form for evaluation of ``probGeometric``. @@ -407,13 +407,13 @@ theorem probGeometric_normalizes : clear A simp only [mul_one] rw [ENNReal.tsum_sub] - . rw [ENNReal.tsum_eq_add_tsum_ite 0] + · rw [ENNReal.tsum_eq_add_tsum_ite 0] simp only [_root_.pow_zero, ite_test, tsum_shift'_1] simp only [pow_add, pow_one] rw [ENNReal.add_sub_cancel_right] apply trial_sum_ne_top' trial trial_spec' - . apply trial_sum_ne_top' trial trial_spec' - . rw [Pi.le_def] + · apply trial_sum_ne_top' trial trial_spec' + · rw [Pi.le_def] intro i have A : 0 ≤ trial true ^ i := by exact _root_.zero_le (trial true ^ i) have B := trial_le_1 trial trial_spec 1 diff --git a/SampCert/Samplers/Laplace/Properties.lean b/SampCert/Samplers/Laplace/Properties.lean index 767a9409..c903dd17 100644 --- a/SampCert/Samplers/Laplace/Properties.lean +++ b/SampCert/Samplers/Laplace/Properties.lean @@ -36,39 +36,39 @@ theorem DiscreteLaplaceSampleLoopIn1Aux_normalizes (t : PNat) : right intro a congr - . rw [ENNReal.tsum_eq_add_tsum_ite a] - . rw [ENNReal.tsum_eq_add_tsum_ite a] + · rw [ENNReal.tsum_eq_add_tsum_ite a] + · rw [ENNReal.tsum_eq_add_tsum_ite a] simp only [↓reduceIte, NNReal.coe_natCast] have A : forall x a, (@ite ENNReal (x = a) (Classical.propDecidable (x = a)) 0 (if a = x then UniformSample t x * BernoulliExpNegSample x t false else 0)) = 0 := by intro x a split - . simp - . split - . rename_i h1 h2 + · simp + · split + · rename_i h1 h2 subst h2 contradiction - . simp + · simp have B : forall x a, (@ite ENNReal (x = a) (Classical.propDecidable (x = a)) 0 (if a = x then UniformSample t x * BernoulliExpNegSample x t true else 0)) = 0 := by intro x a split - . simp - . split - . rename_i h1 h2 + · simp + · split + · rename_i h1 h2 subst h2 contradiction - . simp + · simp conv => left right intro a congr - . right + · right right intro x rw [A] - . right + · right right intro x rw [B] @@ -108,12 +108,12 @@ theorem DiscreteLaplaceSampleLoopIn1Aux_apply_true (t : PNat) (n : ℕ) : (@ite ENNReal (n = x) (instDecidableEqNat n x) (UniformSample t x * BernoulliExpNegSample x t true) 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 @@ -143,12 +143,12 @@ theorem DiscreteLaplaceSampleLoopIn1Aux_apply_false (t : PNat) (n : ℕ) : (@ite ENNReal (n = x) (instDecidableEqNat n x) (UniformSample t x * BernoulliExpNegSample x t false) 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 @@ -182,12 +182,12 @@ theorem DiscreteLaplaceSampleLoopIn1_apply_pre (t : PNat) (n : ℕ) : @ite ENNReal (n = x) (Classical.propDecidable (n = (x, true).1)) 1 0)) = 0 := by intro x split - . simp only - . split - . rename_i h1 h2 + · simp only + · split + · rename_i h1 h2 subst h2 contradiction - . simp only [mul_zero] + · simp only [mul_zero] conv => left right @@ -214,9 +214,9 @@ theorem DiscreteLaplaceSampleLoopIn1_apply (t : PNat) (n : ℕ) (support : n < t have B : ∀ i : ℕ, (@ite ENNReal (i + ↑t < ↑t) (decLt (i + ↑t) ↑t) ((ENNReal.ofReal (rexp (- (↑(i + ↑t) / ↑↑t)))) / ↑↑t) 0) = 0 := by intro i split - . rename_i h + · rename_i h simp only [add_lt_iff_neg_right, not_lt_zero'] at h - . simp only + · simp only conv => left right @@ -249,10 +249,10 @@ theorem DiscreteLaplaceSampleLoopIn1_apply (t : PNat) (n : ℕ) (support : n < t rw [mul_assoc] congr - . rw [ENNReal.toReal_div] + · rw [ENNReal.toReal_div] simp only [ENNReal.toReal_nat] - . have A : ∀ i ∈ range t, 0 ≤ rexp (- (i / t)) := by + · have A : ∀ i ∈ range t, 0 ≤ rexp (- (i / t)) := by intro i _ apply exp_nonneg (-(↑i / ↑↑t)) @@ -286,27 +286,27 @@ theorem DiscreteLaplaceSampleLoopIn1_apply (t : PNat) (n : ℕ) (support : n < t rw [X] clear X rw [ENNReal.mul_inv] - . rw [mul_comm] + · rw [mul_comm] rw [mul_assoc] rw [ENNReal.inv_mul_cancel] - . rw [← ENNReal.ofReal_inv_of_pos] - . rw [inv_div] + · rw [← ENNReal.ofReal_inv_of_pos] + · rw [inv_div] simp only [mul_one] - . apply div_pos - . rw [Real.exp_neg] + · apply div_pos + · rw [Real.exp_neg] simp only [sub_pos] rw [inv_lt_one_iff] right rw [one_lt_exp_iff] simp only [zero_lt_one] - . simp only [sub_pos, exp_lt_one_iff] + · simp only [sub_pos, exp_lt_one_iff] rw [← neg_div'] simp only [one_div, Left.neg_neg_iff, inv_pos, cast_pos, PNat.pos] - . simp only [ne_eq, ENNReal.inv_eq_zero, ENNReal.natCast_ne_top, not_false_eq_true] - . simp only [ne_eq, ENNReal.inv_eq_top, cast_eq_zero, PNat.ne_zero, not_false_eq_true] - . simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le, ENNReal.inv_eq_top, cast_eq_zero, + · simp only [ne_eq, ENNReal.inv_eq_zero, ENNReal.natCast_ne_top, not_false_eq_true] + · simp only [ne_eq, ENNReal.inv_eq_top, cast_eq_zero, PNat.ne_zero, not_false_eq_true] + · simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le, ENNReal.inv_eq_top, cast_eq_zero, PNat.ne_zero, not_false_eq_true, or_true] - . simp only [ne_eq, ENNReal.ofReal_ne_top, not_false_eq_true, ENNReal.inv_eq_zero, + · simp only [ne_eq, ENNReal.ofReal_ne_top, not_false_eq_true, ENNReal.inv_eq_zero, ENNReal.natCast_ne_top, or_self] @[simp] @@ -335,18 +335,18 @@ theorem DiscreteLaplaceSampleLoop_apply (num : PNat) (den : PNat) (n : ℕ) (b : ((@ite ENNReal (b = false ∧ n = x - 1) instDecidableAnd 2⁻¹ 0 : ENNReal) + @ite ENNReal (b = true ∧ n = x - 1) instDecidableAnd 2⁻¹ 0 : ENNReal))) ) = 0 := by intro x split - . simp only - . split - . simp only - . split - . split - . rename_i h1 h2 h3 h4 + · simp only + · split + · simp only + · split + · split + · rename_i h1 h2 h3 h4 cases h3 cases h4 rename_i h5 h6 h7 h8 subst h7 contradiction - . rename_i h1 h2 h3 h4 + · rename_i h1 h2 h3 h4 cases h3 simp only [not_and] at h4 rename_i h5 h6 @@ -354,15 +354,15 @@ theorem DiscreteLaplaceSampleLoop_apply (num : PNat) (den : PNat) (n : ℕ) (b : have B : x = x - 1 + 1 := by exact (succ_pred h2).symm contradiction - . split - . rename_i h1 h2 h3 h4 + · split + · rename_i h1 h2 h3 h4 cases h4 rename_i h5 h6 subst h6 have B : x = x - 1 + 1 := by exact (succ_pred h2).symm contradiction - . rename_i h1 h2 h3 h4 + · rename_i h1 h2 h3 h4 simp only [not_and, add_zero, mul_zero] at * conv => @@ -376,9 +376,9 @@ theorem DiscreteLaplaceSampleLoop_apply (num : PNat) (den : PNat) (n : ℕ) (b : simp only [tsum_zero, add_zero] congr split - . rename_i h + · rename_i h simp only [h, ↓reduceIte, add_zero] - . simp only [zero_add, ite_eq_left_iff, Bool.not_eq_true] + · simp only [zero_add, ite_eq_left_iff, Bool.not_eq_true] rename_i h1 intro h2 contradiction @@ -386,8 +386,8 @@ theorem DiscreteLaplaceSampleLoop_apply (num : PNat) (den : PNat) (n : ℕ) (b : @[simp] theorem ite_simpl_1 (x y : ℕ) (a : ENNReal) : ite (x = y) 0 (ite (y = x) a 0) = 0 := by split - . simp - . rename_i h + · simp + · rename_i h simp [h] intro h subst h @@ -396,57 +396,57 @@ theorem ite_simpl_1 (x y : ℕ) (a : ENNReal) : ite (x = y) 0 (ite (y = x) a 0) @[simp] theorem ite_simpl_2 (x y : ℕ) (a : ENNReal) : ite (x = 0) 0 (ite ((y : ℤ) = -(x : ℤ)) a 0) = 0 := by split - . simp - . split - . rename_i h1 h2 + · simp + · split + · rename_i h1 h2 have A : (y : ℤ) ≥ 0 := Int.NonNeg.mk (y + 0) rw [h2] at A simp at * subst A contradiction - . simp + · simp @[simp] theorem ite_simpl_3 (x y : ℕ) (a : ENNReal) : ite (x = y + 1) 0 (ite (x = 0) 0 (ite (y = x - 1) a 0)) = 0 := by split - . simp - . split - . simp - . split - . rename_i h1 h2 h3 + · simp + · split + · simp + · split + · rename_i h1 h2 h3 subst h3 cases x - . contradiction - . simp at h1 - . simp + · contradiction + · simp at h1 + · simp @[simp] theorem ite_simpl_4 (x y : ℕ) (a : ENNReal) : ite ((x : ℤ) = - (y : ℤ)) (ite (y = 0) 0 a) 0 = 0 := by split - . split - . simp - . rename_i h1 h2 + · split + · simp + · rename_i h1 h2 have B : (y : ℤ) ≥ 0 := by exact Int.NonNeg.mk (y + 0) have C : -(y : ℤ) ≥ 0 := by exact le_iff_exists_sup.mpr (Exists.intro (Int.ofNat x) (id h1.symm)) cases y - . contradiction - . rename_i n + · contradiction + · rename_i n simp at C contradiction - . simp + · simp @[simp] theorem ite_simpl_5 (n c : ℕ) (a : ENNReal) (h : n ≠ 0) : ite (- (n : ℤ) = (c : ℤ)) a 0 = 0 := by split - . rename_i h' + · rename_i h' have A : (n : ℤ) ≥ 0 := by exact Int.NonNeg.mk (n + 0) have B : -(n : ℤ) ≥ 0 := by exact le_iff_exists_sup.mpr (Exists.intro (Int.ofNat c) h') cases n - . contradiction - . rename_i n + · contradiction + · rename_i n simp at B contradiction - . simp + · simp @[simp] theorem DiscreteLaplaceSampleLoop_normalizes (num : PNat) (den : PNat) : @@ -501,10 +501,10 @@ theorem DiscreteLaplaceSampleLoop_normalizes (num : PNat) (den : PNat) : clear A rw [mul_one] apply probGeometric_normalizes' - . have A := BernoulliExpNegSample_normalizes den num + · have A := BernoulliExpNegSample_normalizes den num rw [tsum_bool] at A trivial - . simp + · simp theorem avoid_double_counting (num den : PNat) : (∑' (x : Bool × ℕ), if x.1 = true → ¬x.2 = 0 then DiscreteLaplaceSampleLoop num den x else 0) @@ -623,7 +623,7 @@ theorem DiscreteLaplaceSample_apply (num den : PNat) (x : ℤ) : have OR : x ≥ 0 ∨ x < 0 := by exact le_or_gt 0 x cases OR - . rename_i h1 + · rename_i h1 lift x to ℕ using h1 conv => left @@ -647,7 +647,7 @@ theorem DiscreteLaplaceSample_apply (num den : PNat) (x : ℤ) : rw [division_def] rw [avoid_double_counting] rw [ENNReal.mul_inv] - . simp only [inv_inv] + · simp only [inv_inv] have A : 0 ≤ rexp (-(↑↑den / ↑↑num)) := by apply exp_nonneg (-(↑↑den / ↑↑num)) have B : 0 ≤ rexp ((↑↑den / ↑↑num)) := by apply exp_nonneg ((↑↑den / ↑↑num)) @@ -708,17 +708,17 @@ theorem DiscreteLaplaceSample_apply (num den : PNat) (x : ℤ) : -- end of 3rd rewrite rw [laplace_normalizer_swap] - . simp only [sub_nonneg, exp_le_one_iff, Left.neg_nonpos_iff] + · simp only [sub_nonneg, exp_le_one_iff, Left.neg_nonpos_iff] rw [div_nonneg_iff] left simp only [cast_nonneg, and_self] - . refine Right.add_pos_of_pos_of_nonneg ?inl.intro.e_a.ha A + · refine Right.add_pos_of_pos_of_nonneg ?inl.intro.e_a.ha A simp only [zero_lt_one] -- 0 < 1 + rexp (-(↑↑den / ↑↑num)) - . exact A - . simp only [zero_le_one] -- 0 ≤ 1 - . exact A - . exact A - . have X : 0 ≤ (rexp (↑↑den / ↑↑num) - 1) := by + · exact A + · simp only [zero_le_one] -- 0 ≤ 1 + · exact A + · exact A + · have X : 0 ≤ (rexp (↑↑den / ↑↑num) - 1) := by simp only [sub_nonneg, one_le_exp_iff] rw [div_nonneg_iff] left @@ -728,16 +728,16 @@ theorem DiscreteLaplaceSample_apply (num den : PNat) (x : ℤ) : refine Right.add_nonneg B ?hb simp only [zero_le_one] exact mul_nonneg X Y - . left + · left simp only [PNat.val_ofNat, reduceSucc, cast_ofNat, ne_eq, ENNReal.inv_eq_zero, ENNReal.two_ne_top, not_false_eq_true] - . left + · left simp only [ne_eq, ENNReal.inv_eq_top, cast_eq_zero, PNat.ne_zero, not_false_eq_true] - . rename_i h1 + · rename_i h1 have A : ∃ n : ℕ, - n = x := by cases x - . contradiction - . rename_i a + · contradiction + · rename_i a exists (a + 1) cases A rename_i n h2 @@ -769,7 +769,7 @@ theorem DiscreteLaplaceSample_apply (num den : PNat) (x : ℤ) : rw [division_def] rw [avoid_double_counting] rw [ENNReal.mul_inv] - . simp only [inv_inv] + · simp only [inv_inv] have A : 0 ≤ rexp (-(↑↑den / ↑↑num)) := by apply exp_nonneg (-(↑↑den / ↑↑num)) have B : 0 ≤ rexp ((↑↑den / ↑↑num)) := by apply exp_nonneg ((↑↑den / ↑↑num)) @@ -828,18 +828,18 @@ theorem DiscreteLaplaceSample_apply (num den : PNat) (x : ℤ) : congr 1 rw [laplace_normalizer_swap] - . simp only [sub_nonneg, exp_le_one_iff, Left.neg_nonpos_iff] + · simp only [sub_nonneg, exp_le_one_iff, Left.neg_nonpos_iff] rw [div_nonneg_iff] left simp only [cast_nonneg, and_self] - . apply Right.add_pos_of_pos_of_nonneg + · apply Right.add_pos_of_pos_of_nonneg simp only [zero_lt_one] exact A - . exact A - . simp only [zero_le_one] -- 0 ≤ 1 - . exact A - . exact A - . have X : 0 ≤ (rexp (↑↑den / ↑↑num) - 1) := by + · exact A + · simp only [zero_le_one] -- 0 ≤ 1 + · exact A + · exact A + · have X : 0 ≤ (rexp (↑↑den / ↑↑num) - 1) := by simp only [sub_nonneg, one_le_exp_iff] rw [div_nonneg_iff] left @@ -850,10 +850,10 @@ theorem DiscreteLaplaceSample_apply (num den : PNat) (x : ℤ) : simp only [zero_le_one] exact mul_nonneg X Y - . left + · left simp only [PNat.val_ofNat, reduceSucc, cast_ofNat, ne_eq, ENNReal.inv_eq_zero, ENNReal.two_ne_top, not_false_eq_true] - . left + · left simp only [ne_eq, ENNReal.inv_eq_top, cast_eq_zero, PNat.ne_zero, not_false_eq_true] /-- @@ -907,7 +907,7 @@ theorem DiscreteLaplaceSample_normalizes (num den : PNat) : rw [← add_mul] rw [ENNReal.mul_inv_cancel] - . simp only [DiscreteLaplaceSampleLoop_apply, ne_eq, add_eq_zero, ENNReal.tsum_eq_zero, + · simp only [DiscreteLaplaceSampleLoop_apply, ne_eq, add_eq_zero, ENNReal.tsum_eq_zero, _root_.mul_eq_zero, pow_eq_zero_iff', ENNReal.ofReal_eq_zero, tsub_eq_zero_iff_le, ENNReal.one_le_ofReal, one_le_exp_iff, Left.nonneg_neg_iff, ENNReal.inv_eq_zero, ENNReal.natCast_ne_top, or_false, ite_eq_left_iff, not_and, not_forall, exists_prop] @@ -915,7 +915,7 @@ theorem DiscreteLaplaceSample_normalizes (num den : PNat) : existsi 1 simp apply exp_pos (-(↑↑den / ↑↑num)) - . rw [← @ENNReal.tsum_add] + · rw [← @ENNReal.tsum_add] rw [ne_iff_lt_or_gt] left have B : (∑' (a : ℕ), (DiscreteLaplaceSampleLoop num den (false, a) + if a = 0 then 0 else DiscreteLaplaceSampleLoop num den (true, a))) ≤ (∑' (x : Bool × ℕ), DiscreteLaplaceSampleLoop num den x) := by @@ -929,8 +929,8 @@ theorem DiscreteLaplaceSample_normalizes (num den : PNat) : apply ENNReal.tsum_le_tsum intro a split - . simp - . simp + · simp + · simp have E : (∑' (x : Bool × ℕ), DiscreteLaplaceSampleLoop num den x) < ⊤ := by simp diff --git a/SampCert/Samplers/Uniform/Properties.lean b/SampCert/Samplers/Uniform/Properties.lean index c108628c..fd7539bf 100644 --- a/SampCert/Samplers/Uniform/Properties.lean +++ b/SampCert/Samplers/Uniform/Properties.lean @@ -38,11 +38,11 @@ theorem rw1 (n : PNat) : congr rw [mul_comm] rw [ENNReal.mul_inv] - . simp only [inv_inv] - . simp only [ne_eq, cast_eq_zero, PNat.ne_zero, not_false_eq_true, inv_eq_top, log_eq_zero_iff, + · simp only [inv_inv] + · simp only [ne_eq, cast_eq_zero, PNat.ne_zero, not_false_eq_true, inv_eq_top, log_eq_zero_iff, gt_iff_lt, ofNat_pos, mul_lt_iff_lt_one_right, lt_one_iff, not_ofNat_le_one, or_self, pow_eq_zero_iff, OfNat.ofNat_ne_zero] - . simp only [ne_eq, natCast_ne_top, not_false_eq_true, ENNReal.inv_eq_zero, pow_eq_top_iff, + · simp only [ne_eq, natCast_ne_top, not_false_eq_true, ENNReal.inv_eq_zero, pow_eq_top_iff, two_ne_top, log_eq_zero_iff, gt_iff_lt, ofNat_pos, mul_lt_iff_lt_one_right, lt_one_iff, PNat.ne_zero, not_ofNat_le_one, or_self, and_true] @@ -59,8 +59,8 @@ lemma double_large_enough (n : PNat) (x : Nat) (support : x < n) : have A : ∀ m : ℕ, m < 2 ^ (log 2 ↑(2 * m)) := by intro m cases m - . simp - . rename_i m + · simp + · rename_i m have H1 := @Nat.lt_pow_succ_log_self 2 le.refl (succ m) have H2 := @Nat.log_mul_base 2 (succ m) le.refl (succ_ne_zero m) rw [Nat.mul_comm] @@ -113,7 +113,7 @@ lemma uniformPowerOfTwoSample_autopilot (n : PNat) : clear D trivial apply ENNReal.sub_eq_of_eq_add_rev - . have Y := tsum_split_less (fun i => ↑n ≤ i) (fun i => UniformPowerOfTwoSample (2 * n) i) + · have Y := tsum_split_less (fun i => ↑n ≤ i) (fun i => UniformPowerOfTwoSample (2 * n) i) rw [UniformPowerOfTwoSample_normalizes (2 * n)] at Y simp at Y clear X @@ -121,7 +121,7 @@ lemma uniformPowerOfTwoSample_autopilot (n : PNat) : rename_i h rw [h] at Y contradiction - . simp only [decide_eq_true_eq, decide_eq_false_iff_not, not_le, one_div] at X + · simp only [decide_eq_true_eq, decide_eq_false_iff_not, not_le, one_div] at X rw [X] /-- @@ -141,14 +141,14 @@ theorem UniformSample_apply (n : PNat) (x : Nat) (support : x < n) : 0) = 0 := by intro x1 split - . simp only - . split - . split - . rename_i h1 h2 h3 + · simp only + · split + · split + · rename_i h1 h2 h3 subst h3 contradiction - . simp only [mul_zero] - . simp only + · simp only [mul_zero] + · simp only conv => left right @@ -162,15 +162,15 @@ theorem UniformSample_apply (n : PNat) (x : Nat) (support : x < n) : (@ite ℝ≥0∞ (↑n ≤ x) (decLe ↑n x) (UniformPowerOfTwoSample (2 * n) x) 0) := by intro x split - . split - . rename_i h1 h2 + · split + · rename_i h1 h2 rw [← not_lt] at h2 contradiction - . simp only - . split - . rename_i h1 h2 + · simp only + · split + · rename_i h1 h2 simp only - . rename_i h1 h2 + · rename_i h1 h2 simp only [not_lt] at h1 contradiction conv => @@ -205,8 +205,8 @@ Sum of the ``UniformSample`` distribution over a subset of its support. lemma UniformSample_support_Sum (n : PNat) (m : ℕ) (h : m ≤ n) : (Finset.sum (range m) fun i => UniformSample n i) = m / n := by induction m - . simp - . rename_i m IH + · simp + · rename_i m IH simp at * have A : m ≤ ↑n := by exact lt_succ.mp (le.step h) have IH' := IH A @@ -223,8 +223,8 @@ lemma UniformSample_support_Sum' (n : PNat) : (Finset.sum (range n) fun i => UniformSample n i) = 1 := by rw [UniformSample_support_Sum n n le.refl] apply ENNReal.div_self - . simp - . simp + · simp + · simp /-- Sum over the whole space of ``UniformSample`` is ``1``. @@ -233,8 +233,8 @@ Sum over the whole space of ``UniformSample`` is ``1``. theorem UniformSample_normalizes (n : PNat) : ∑' a : ℕ, UniformSample n a = 1 := by rw [← @sum_add_tsum_nat_add' _ _ _ _ _ _ n] - . simp [UniformSample_support_Sum'] - . exact ENNReal.summable + · simp [UniformSample_support_Sum'] + · exact ENNReal.summable /-- ``UniformSample`` is a proper distribution @@ -259,8 +259,8 @@ theorem UniformSample_apply_ite (a b : ℕ) (c : PNat) (i1 : b ≤ c) : split rename_i i2 rw [UniformSample_apply] - . exact Nat.lt_of_lt_of_le i2 i1 - . trivial + · exact Nat.lt_of_lt_of_le i2 i1 + · trivial /-- Evaluation of ``UniformSample`` on ``ℕ`` guarded by its support, when outside the support. @@ -268,9 +268,9 @@ Evaluation of ``UniformSample`` on ``ℕ`` guarded by its support, when outside theorem UniformSample_apply' (n : PNat) (x : Nat) : (UniformSample n) x = if x < n then (1 : ENNReal) / n else 0 := by split - . rename_i h + · rename_i h simp [h] - . rename_i h + · rename_i h apply UniformSample_apply_out exact Nat.not_lt.mp h diff --git a/SampCert/Util/Gaussian/DiscreteGaussian.lean b/SampCert/Util/Gaussian/DiscreteGaussian.lean index 33623a93..93ac2a6a 100644 --- a/SampCert/Util/Gaussian/DiscreteGaussian.lean +++ b/SampCert/Util/Gaussian/DiscreteGaussian.lean @@ -43,8 +43,8 @@ instance gauss_term_ℂ (σ μ : ℝ) : C(ℝ,ℂ) where apply Continuous.neg apply Continuous.pow apply Continuous.sub - . apply continuous_ofReal - . apply continuous_const + · apply continuous_ofReal + · apply continuous_const /-- Agreement between the ℂ-valued and ℝ-valued gaussian formulas over ℝ @@ -271,8 +271,8 @@ The sum of ``gauss_term_ℝ`` is positive. theorem sum_gauss_term_pos {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) : 0 < (∑' (x : ℤ), (gauss_term_ℝ σ μ) x) := by apply tsum_pos (summable_gauss_term' h μ) _ 0 - . apply gauss_term_pos - . intro i + · apply gauss_term_pos + · intro i apply gauss_term_noneg /-- @@ -298,8 +298,8 @@ theorem discrete_gaussian_pos {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (n : ℤ) : rw [div_pos_iff] left constructor - . apply gauss_term_pos - . apply sum_gauss_term_pos h μ + · apply gauss_term_pos + · apply sum_gauss_term_pos h μ /-- The discrete gaussian is nonnegative. diff --git a/SampCert/Util/Gaussian/GaussBound.lean b/SampCert/Util/Gaussian/GaussBound.lean index 63238a5a..2dddaffe 100644 --- a/SampCert/Util/Gaussian/GaussBound.lean +++ b/SampCert/Util/Gaussian/GaussBound.lean @@ -83,9 +83,9 @@ theorem sum_gauss_term_bound {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) : unfold fourier_gauss_term simp [sq] congr 1 - . rw [Complex.abs_exp] + · rw [Complex.abs_exp] simp [sq] - . have A : 0 ≤ (2⁻¹ * ((↑σ)⁻¹ * (↑σ)⁻¹ * (↑π)⁻¹)) ^ (2 : ℝ)⁻¹ := by + · have A : 0 ≤ (2⁻¹ * ((↑σ)⁻¹ * (↑σ)⁻¹ * (↑π)⁻¹)) ^ (2 : ℝ)⁻¹ := by apply rpow_nonneg rw [mul_nonneg_iff] left @@ -124,7 +124,7 @@ theorem sum_gauss_term_bound {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) : simp right ring_nf - . simp + · simp rw [← X] rw [H] diff --git a/SampCert/Util/Gaussian/GaussPeriodicity.lean b/SampCert/Util/Gaussian/GaussPeriodicity.lean index fb4e9896..0a257747 100644 --- a/SampCert/Util/Gaussian/GaussPeriodicity.lean +++ b/SampCert/Util/Gaussian/GaussPeriodicity.lean @@ -174,8 +174,8 @@ theorem shifted_gauss_sum_pos {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (k : ℕ) : (∑' (n : ℤ), (gauss_term_ℝ σ μ) n) = ∑' (n : ℤ), (gauss_term_ℝ σ (μ + k)) n := by revert μ induction k - . simp - . intro μ + · simp + · intro μ rename_i n IH simp rw [← add_assoc] @@ -189,8 +189,8 @@ theorem shifted_gauss_sum_neg {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (k : ℕ) : (∑' (n : ℤ), (gauss_term_ℝ σ μ) n) = ∑' (n : ℤ), (gauss_term_ℝ σ (μ - k)) n := by revert μ induction k - . simp - . intro μ + · simp + · intro μ rename_i n IH simp rw [sub_add_eq_sub_sub] @@ -207,8 +207,8 @@ The sum of ``gauss_term_ℝ`` does not change when the mean shifts by any intege theorem shifted_gauss_sum {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (k : ℤ) : (∑' (n : ℤ), (gauss_term_ℝ σ μ) n) = ∑' (n : ℤ), (gauss_term_ℝ σ (μ + k)) n := by cases k - . apply shifted_gauss_sum_pos h - . simp + · apply shifted_gauss_sum_pos h + · simp have X : ∀ a : ℕ, -(1: ℝ) + -a = - (((1 + a) : ℕ)) := by intro a simp diff --git a/SampCert/Util/Log.lean b/SampCert/Util/Log.lean index 0739ce47..c3498da4 100644 --- a/SampCert/Util/Log.lean +++ b/SampCert/Util/Log.lean @@ -106,7 +106,7 @@ lemma ENNReal_isReal_cases (x : ENNReal) : x = ⊤ ∨ (∃ v : ℝ, x = ENNReal cases x · left simp - . right + · right rename_i v rcases v with ⟨ r, Hr ⟩ exists r diff --git a/SampCert/Util/Shift.lean b/SampCert/Util/Shift.lean index 57c2aa2c..356c3e51 100644 --- a/SampCert/Util/Shift.lean +++ b/SampCert/Util/Shift.lean @@ -27,7 +27,7 @@ theorem tsum_shift₁ (f : ℤ → ℝ) (μ : ℕ) have h4 : Summable fun x : ℕ => f (- (x + 1)) := by apply h3 0 rw [tsum_of_nat_of_neg_add_one h1] - . rw [← sum_add_tsum_nat_add μ h1] + · rw [← sum_add_tsum_nat_add μ h1] rw [add_rotate] conv => left @@ -53,8 +53,8 @@ theorem tsum_shift₁ (f : ℤ → ℝ) (μ : ℕ) rw [add_comm] congr 1 induction μ - . simp - . rename_i n IH + · simp + · rename_i n IH rw [Finset.sum_range_succ] rw [IH] clear IH @@ -64,7 +64,7 @@ theorem tsum_shift₁ (f : ℤ → ℝ) (μ : ℕ) intro x _ congr 1 ring_nf - . exact h4 + · exact h4 /-- @@ -79,7 +79,7 @@ theorem tsum_shift₂ (f : ℤ → ℝ) (μ : ℕ) have h4 : Summable fun x : ℕ => f (- (x + 1)) := by apply h3 0 rw [tsum_of_nat_of_neg_add_one] - . rw [← sum_add_tsum_nat_add μ (h2 μ)] + · rw [← sum_add_tsum_nat_add μ (h2 μ)] rw [add_rotate] conv => left @@ -90,28 +90,28 @@ theorem tsum_shift₂ (f : ℤ → ℝ) (μ : ℕ) right rw [tsum_of_nat_of_neg_add_one h1 h4] congr 1 - . apply tsum_congr + · apply tsum_congr intro b congr 1 simp - . conv => + · conv => right rw [← sum_add_tsum_nat_add μ h4] congr 1 - . induction μ - . simp - . rename_i μ IH + · induction μ + · simp + · rename_i μ IH rw [Finset.sum_range_succ'] rw [Finset.sum_range_succ] rw [← IH] simp - . apply tsum_congr + · apply tsum_congr intro b congr 1 simp ring_nf - . exact (h2 μ) - . exact (h3 μ) + · exact (h2 μ) + · exact (h3 μ) /-- A series is invariant under integer shifts provided its shifted positive and negative parts are summable. @@ -146,10 +146,10 @@ theorem tsum_shift (f : ℤ → ℝ) (μ : ℤ) intro μ apply h' cases μ - . rename_i μ + · rename_i μ rw [tsum_shift₁ f μ h1 h2] simp - . rename_i μ + · rename_i μ rw [← tsum_shift₂ f (μ + 1) h3 h4] apply tsum_congr intro b diff --git a/SampCert/Util/Util.lean b/SampCert/Util/Util.lean index 936e3630..7f9e3d76 100644 --- a/SampCert/Util/Util.lean +++ b/SampCert/Util/Util.lean @@ -33,9 +33,9 @@ theorem sum_simple (bound : ℕ) (k : ENNReal) : rw [(tsum_eq_zero_iff A).mpr] · rw [← @Finset.sum_filter] rw [Finset.filter_true_of_mem] - . simp + · simp rw [mul_comm] - . intro _ + · intro _ exact List.mem_range.mp · intro x simp @@ -50,8 +50,8 @@ theorem tsum_simpl_ite_left (cond : T → Bool) (f g : T → ENNReal) : apply tsum_congr intro b split - . simp - . rename_i h + · simp + · rename_i h cases b rename_i b P simp at * @@ -67,13 +67,13 @@ theorem tsum_simpl_ite_right (cond : T → Bool) (f g : T → ENNReal) : apply tsum_congr intro b split - . rename_i h + · rename_i h cases b rename_i b P simp at * have A : ¬ cond b = true := by exact P simp [A] at h - . simp + · simp /-- Partition series indices based on conditional guard @@ -98,13 +98,13 @@ theorem tsum_simpl_ite_left' (cond : T → Bool) (f g : T → ENNReal) : apply tsum_congr intro b split - . rename_i h + · rename_i h cases b rename_i b P simp at * have A : cond b = true := by exact P simp [A] at h - . simp + · simp /-- Simplify guarded series based on index type @@ -115,8 +115,8 @@ theorem tsum_simpl_ite_right' (cond : T → Bool) (f g : T → ENNReal) : apply tsum_congr intro b split - . simp - . rename_i h + · simp + · rename_i h cases b rename_i b P simp at * @@ -184,8 +184,8 @@ theorem tsum_shift_1 (f : ℕ → ENNReal) : rw [iSup_congr] intro i induction i - . simp - . rename_i i IH + · simp + · rename_i i IH rw [sum_range_succ] simp conv => @@ -210,8 +210,8 @@ theorem tsum_shift'_1 (f : ℕ → ENNReal) : rw [iSup_congr] intro i induction i - . simp - . rename_i i IH + · simp + · rename_i i IH rw [sum_range_succ] simp conv => @@ -236,16 +236,16 @@ theorem tsum_shift'_2 (f : ℕ → ENNReal) : rw [iSup_congr] intro i induction i - . simp + · simp intro x h1 h2 h3 cases x - . contradiction - . rename_i x - . cases x - . contradiction - . rename_i x + · contradiction + · rename_i x + · cases x + · contradiction + · rename_i x contradiction - . rename_i i IH + · rename_i i IH rw [sum_range_succ] simp conv =>