From 888918d31bf556a04215a38559542b30a557bc44 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 15:10:19 -0400 Subject: [PATCH 1/5] chore(deps): track CSLib main and Lean rc2 Advance CSLib to 8a8ad748 and synchronize Mathlib, the documentation generator, Verso, and all three lockfiles with Lean v4.36.0-rc2. Keep the root and documentation projects on the same inherited dependency revisions. --- docbuild/lake-manifest.json | 34 +++++++++++++++++----------------- docbuild/lakefile.toml | 2 +- guide/lake-manifest.json | 30 +++++++++++++++--------------- guide/lakefile.toml | 2 +- lake-manifest.json | 26 +++++++++++++------------- lakefile.toml | 2 +- lean-toolchain | 2 +- 7 files changed, 49 insertions(+), 49 deletions(-) diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json index 3609d26b5..a1f5e4692 100644 --- a/docbuild/lake-manifest.json +++ b/docbuild/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "0656b7ebd305f089c8d6bd8684a0797f19414cc2", + "rev": "20afd4ddabd2ef38ffb1a8b930ee0f375e3f75e8", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.36.0-rc1", + "inputRev": "v4.36.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"type": "path", @@ -23,7 +23,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e1faac1842cb10b3a68c644643b6e3568766343c", + "rev": "f582e4bc64d6f43e6e711f89b09567d2088fab8d", "name": "leansqlite", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -33,7 +33,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49", + "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -43,7 +43,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a24bcde05a7971144ba0c0b5b1d60c3a0f0bc4af", + "rev": "91ece4f8d8f93aac566e247874f6b27b57249f1b", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -53,7 +53,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "78f28e27259a4b2f5a8199800334cebd92730f3d", + "rev": "cdf8963f8b4c9a5593c5aaa9fa4f2759f8dec1c1", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -73,27 +73,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "f4a472560f78c59bbedd795fe041ec507f7d0582", + "rev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "f4a472560f78c59bbedd795fe041ec507f7d0582", + "inputRev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "625d8914199bc567cca9b91f90e8e5afafa5ae51", + "rev": "9d581dfff2e41de989072ea63abf3daf69311520", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.36.0-rc1", + "inputRev": "v4.36.0-rc2", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c2d7840c65673533e15b499f25beecdc6227f7d8", + "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -103,7 +103,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9d39f9bb0c30aa2f6200808805ff16e6ce950890", + "rev": "c61286b7b63cbfd563b28e11e81d0a18233a044a", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -113,7 +113,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b3cc36c295aa5e3e3c0197b09a6556298e710447", + "rev": "b8cc5dd0a36233b88a6ed5a7dbf1207d09338c60", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -123,7 +123,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "17137fad38a2cc782ff00b323a13c3a991d085ab", + "rev": "16259c0d07d61ee37d999d05b5cf96338b8daa11", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -133,7 +133,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cbdde3aa2665915fb286c48bcd4cdf885c629511", + "rev": "7d11bfa88558f8d3d90afdf6bd877ed70001498d", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -143,7 +143,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6d26f8bb4b2bb78f929ad160feac508866821316", + "rev": "b0256621cb88178e9ad932a53633077b3029e621", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -153,7 +153,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4453b52d2468f4c346a8711d728c0742e7483c9b", + "rev": "d4c39b228d4a06f3b00748c2c445a7b9f056a6e3", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml index ed4689727..b9c4092df 100644 --- a/docbuild/lakefile.toml +++ b/docbuild/lakefile.toml @@ -12,4 +12,4 @@ path = ".." [[require]] scope = "leanprover" name = "doc-gen4" -rev = "v4.36.0-rc1" +rev = "v4.36.0-rc2" diff --git a/guide/lake-manifest.json b/guide/lake-manifest.json index b8da10f21..3f19786a0 100644 --- a/guide/lake-manifest.json +++ b/guide/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "f7a4dc6867f8df27778b2b320763ec9e3b7be070", + "rev": "71a2035b44e7f54a797ce799fd1b03cdd3a44684", "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": "v4.36.0-rc1", + "inputRev": "v4.36.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"type": "path", @@ -23,7 +23,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49", + "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -33,7 +33,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d22e76ef3d2a925132315af902ea432233b4a44a", + "rev": "758bff3509b8e90ca82e37aa5de81de3c9e70fc0", "name": "illuminate", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -43,7 +43,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c2d7840c65673533e15b499f25beecdc6227f7d8", + "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -73,27 +73,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "f4a472560f78c59bbedd795fe041ec507f7d0582", + "rev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "f4a472560f78c59bbedd795fe041ec507f7d0582", + "inputRev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "625d8914199bc567cca9b91f90e8e5afafa5ae51", + "rev": "9d581dfff2e41de989072ea63abf3daf69311520", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.36.0-rc1", + "inputRev": "v4.36.0-rc2", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9d39f9bb0c30aa2f6200808805ff16e6ce950890", + "rev": "c61286b7b63cbfd563b28e11e81d0a18233a044a", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -103,7 +103,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b3cc36c295aa5e3e3c0197b09a6556298e710447", + "rev": "b8cc5dd0a36233b88a6ed5a7dbf1207d09338c60", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -113,7 +113,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "17137fad38a2cc782ff00b323a13c3a991d085ab", + "rev": "16259c0d07d61ee37d999d05b5cf96338b8daa11", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -123,7 +123,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cbdde3aa2665915fb286c48bcd4cdf885c629511", + "rev": "7d11bfa88558f8d3d90afdf6bd877ed70001498d", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -133,7 +133,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6d26f8bb4b2bb78f929ad160feac508866821316", + "rev": "b0256621cb88178e9ad932a53633077b3029e621", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -143,7 +143,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4453b52d2468f4c346a8711d728c0742e7483c9b", + "rev": "d4c39b228d4a06f3b00748c2c445a7b9f056a6e3", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/guide/lakefile.toml b/guide/lakefile.toml index fb7601692..f62d2a91a 100644 --- a/guide/lakefile.toml +++ b/guide/lakefile.toml @@ -21,7 +21,7 @@ path = ".." [[require]] name = "verso" git = "https://github.com/leanprover/verso" -rev = "v4.36.0-rc1" +rev = "v4.36.0-rc2" [[lean_lib]] name = "ComplexityGuide" diff --git a/lake-manifest.json b/lake-manifest.json index a4892b4fc..a2c1eaffd 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,27 +5,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "f4a472560f78c59bbedd795fe041ec507f7d0582", + "rev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "f4a472560f78c59bbedd795fe041ec507f7d0582", + "inputRev": "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "625d8914199bc567cca9b91f90e8e5afafa5ae51", + "rev": "9d581dfff2e41de989072ea63abf3daf69311520", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.36.0-rc1", + "inputRev": "v4.36.0-rc2", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c2d7840c65673533e15b499f25beecdc6227f7d8", + "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9d39f9bb0c30aa2f6200808805ff16e6ce950890", + "rev": "c61286b7b63cbfd563b28e11e81d0a18233a044a", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b3cc36c295aa5e3e3c0197b09a6556298e710447", + "rev": "b8cc5dd0a36233b88a6ed5a7dbf1207d09338c60", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "17137fad38a2cc782ff00b323a13c3a991d085ab", + "rev": "16259c0d07d61ee37d999d05b5cf96338b8daa11", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cbdde3aa2665915fb286c48bcd4cdf885c629511", + "rev": "7d11bfa88558f8d3d90afdf6bd877ed70001498d", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6d26f8bb4b2bb78f929ad160feac508866821316", + "rev": "b0256621cb88178e9ad932a53633077b3029e621", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4453b52d2468f4c346a8711d728c0742e7483c9b", + "rev": "d4c39b228d4a06f3b00748c2c445a7b9f056a6e3", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49", + "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.36.0-rc1", + "inputRev": "v4.36.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "complexitylib", diff --git a/lakefile.toml b/lakefile.toml index ce7b8cd77..00f09a874 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -33,7 +33,7 @@ autoImplicit = false [[require]] name = "cslib" git = "https://github.com/leanprover/cslib" -rev = "f4a472560f78c59bbedd795fe041ec507f7d0582" +rev = "8a8ad7489cdccb007ad7279bfb9d03bbda2229ad" [[lean_lib]] name = "Complexity" diff --git a/lean-toolchain b/lean-toolchain index 2afd38716..0fc433692 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.36.0-rc1 +leanprover/lean4:v4.36.0-rc2 From 9a1b75416b7723a073411f0ee9a7d2ccfdd49ec9 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 15:10:24 -0400 Subject: [PATCH 2/5] refactor(probability): use generic infinite-sum lemmas Replace 187 deprecated ENNReal wrapper uses across 55 proof files with their generic counterparts. The exact mapping is: - ENNReal.tsum_le_tsum -> tsum_le_tsum (94) - ENNReal.tsum_add -> tsum_add (54) - ENNReal.tsum_eq_zero -> tsum_eq_zero_iff (14) - ENNReal.summable -> CompleteLattice.summable (6) - ENNReal.tsum_comm -> tsum_comm (6) - ENNReal.tsum_prod' -> tsum_prod' (5) - ENNReal.le_tsum -> le_tsum (5) - ENNReal.tsum_eq_add_tsum_ite -> tsum_eq_add_tsum_ite (2) - ENNReal.tsum_sigma -> tsum_sigma (1) The old wrappers invoke these same theorems specialized to ENNReal. All five le_tsum calls already pass the function by name. No statements or definitions change. --- .../Algorithms/WordRAM/Karger/FastCut.lean | 2 +- .../Algorithms/WordRAM/Karger/Graph.lean | 6 +-- .../Algorithms/WordRAM/KargerMinCut.lean | 2 +- .../Algorithms/WordRAM/KargerStein.lean | 6 +-- .../Computability/Complexity/Classes/IP.lean | 2 +- .../Classes/IP/GraphNonIsomorphism.lean | 2 +- .../Complexity/Classes/IP/Guessing.lean | 6 +-- .../Complexity/Classes/IP/OptimalProver.lean | 8 ++-- .../Complexity/Classes/IP/Repetition.lean | 6 +-- .../LogSpace/Randomized/Amplification.lean | 2 +- .../Complexity/Classes/MIP/OptimalProver.lean | 4 +- .../Complexity/FineGrained/PPSZ/Basic.lean | 2 +- .../Complexity/FineGrained/PPZ.lean | 2 +- .../Computability/Interactive/Plain.lean | 4 +- .../Computability/Kolmogorov/AverageCase.lean | 4 +- .../Computability/PCP/TwoProverGame.lean | 2 +- .../WordRAM/Randomized/Expected.lean | 12 ++--- .../CramerShoup/ProjectiveHash.lean | 4 +- .../Computational/CramerShoup/Scheme.lean | 2 +- .../Crypto/Computational/DiffieHellman.lean | 16 +++---- .../Computational/DiffieHellman/Order.lean | 4 +- .../Encryption/Authenticated.lean | 14 +++--- .../Encryption/EncryptThenMAC.lean | 8 ++-- .../Crypto/Computational/GMW/Soundness.lean | 6 +-- Complexity/Crypto/Computational/MAC.lean | 8 ++-- .../Computational/NaorReingold/Security.lean | 10 ++-- .../Computational/OneWay/LiuPassConverse.lean | 2 +- .../Computational/OneWayToSignature.lean | 6 +-- .../Crypto/Computational/PRGToOneWay.lean | 2 +- .../Computational/PedersenCommitment.lean | 8 ++-- .../Pseudoentropy/MaskedExtraction.lean | 2 +- Complexity/Crypto/Game.lean | 20 ++++---- Complexity/Crypto/Game/UntilBad.lean | 16 +++---- Complexity/Crypto/Primitives/PRG/NextBit.lean | 4 +- .../Crypto/Protocols/Cipher/EvenMansour.lean | 6 +-- .../Crypto/Protocols/Cipher/LubyRackoff.lean | 48 +++++++++---------- .../Crypto/Protocols/MAC/CarterWegman.lean | 16 +++---- .../Protocols/SigmaProtocol/FiatShamir.lean | 6 +-- .../Probabilistic/BoundedUniform.lean | 6 +-- .../Languages/Probabilistic/Expect.lean | 8 ++-- .../Probabilistic/Oracle/Interaction.lean | 2 +- .../Probabilistic/RandomPermutation.lean | 8 ++-- .../Languages/Probabilistic/UntilBad.lean | 10 ++-- .../Languages/Probabilistic/Vector.lean | 2 +- Complexity/Probability/Conditioning.lean | 6 +-- .../Probability/CorrelatedSampling.lean | 2 +- Complexity/Probability/Forking.lean | 2 +- Complexity/Probability/IID.lean | 2 +- Complexity/Probability/MinEntropy.lean | 2 +- Complexity/Probability/Minimax.lean | 4 +- Complexity/Probability/PMF/Bind.lean | 14 +++--- Complexity/Probability/PMF/Event.lean | 16 +++---- Complexity/Probability/PMF/Map.lean | 2 +- .../ProductConditioning/SideInformation.lean | 2 +- Complexity/Probability/RejectionSampling.lean | 4 +- 55 files changed, 186 insertions(+), 186 deletions(-) diff --git a/Complexity/Algorithms/WordRAM/Karger/FastCut.lean b/Complexity/Algorithms/WordRAM/Karger/FastCut.lean index a216c2ae8..30a2afa92 100644 --- a/Complexity/Algorithms/WordRAM/Karger/FastCut.lean +++ b/Complexity/Algorithms/WordRAM/Karger/FastCut.lean @@ -658,7 +658,7 @@ theorem two_branch_hit_prob_ge {α β γ : Type} (m₁ : ProbComp α) (m₂ : α have ha : a ∈ m₁.support := (ProbComp.support_eval m₁) ▸ ha_eval have ha_hit : a ∈ hit₁ := not_not.mp ha_not_miss rw [PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply] - refine ENNReal.tsum_eq_zero.mpr fun b => ?_ + refine tsum_eq_zero_iff.mpr fun b => ?_ by_cases hb_eval : b ∈ (m₂ a).eval.support · have hb : b ∈ (m₂ a).support := (ProbComp.support_eval (m₂ a)) ▸ hb_eval have hmem : f a b ∈ hit := hprop₁ a ha ha_hit b hb diff --git a/Complexity/Algorithms/WordRAM/Karger/Graph.lean b/Complexity/Algorithms/WordRAM/Karger/Graph.lean index 9afa1d805..c03da4013 100644 --- a/Complexity/Algorithms/WordRAM/Karger/Graph.lean +++ b/Complexity/Algorithms/WordRAM/Karger/Graph.lean @@ -1107,7 +1107,7 @@ theorem toOuterMeasure_bind_ge_mul_ennreal {α β : Type*} (p : PMF α) (kernel s₁ * s₂ ≤ p.toOuterMeasure pre * s₂ := mul_le_mul_of_nonneg_right hp zero_le _ ≤ (p.bind kernel).toOuterMeasure event := by rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_mul_right] - refine ENNReal.tsum_le_tsum fun a => ?_ + refine tsum_le_tsum fun a => ?_ by_cases ha : a ∈ pre · simp only [Set.indicator_of_mem ha] by_cases hs : a ∈ p.support @@ -1131,7 +1131,7 @@ theorem toOuterMeasure_bind_le_mul_ennreal {α β : Type*} (p : PMF α) (kernel (p.bind kernel).toOuterMeasure failure ≤ p.toOuterMeasure stillFailing * q₂ := by rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_mul_right] - refine ENNReal.tsum_le_tsum fun a => ?_ + refine tsum_le_tsum fun a => ?_ by_cases hs : a ∈ p.support · by_cases ha : a ∈ stillFailing · simp only [Set.indicator_of_mem ha] @@ -1146,7 +1146,7 @@ valid on arbitrary types without measurability hypotheses. -/ theorem toOuterMeasure_add_compl_ennreal {α : Type*} (p : PMF α) (s : Set α) : p.toOuterMeasure s + p.toOuterMeasure sᶜ = 1 := by classical - rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add] + rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add] have hpt : (fun x => s.indicator p x + sᶜ.indicator p x) = p := by ext x by_cases hx : x ∈ s <;> simp [hx] diff --git a/Complexity/Algorithms/WordRAM/KargerMinCut.lean b/Complexity/Algorithms/WordRAM/KargerMinCut.lean index b3ef003a5..c07c84a3c 100644 --- a/Complexity/Algorithms/WordRAM/KargerMinCut.lean +++ b/Complexity/Algorithms/WordRAM/KargerMinCut.lean @@ -1181,7 +1181,7 @@ theorem ampLoop_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : obtain ⟨m_r, hm_r, _, hsup_r, _⟩ := hnext z₁ hz₁ rw [hml_def, hm_r.codeComp_eq, PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply] - convert ENNReal.tsum_eq_zero.mpr _ + convert tsum_eq_zero_iff.mpr _ intro z₂ by_cases hz₂_eval : z₂ ∈ m_r.eval.support · have hz₂ : z₂ ∈ m_r.support := (ProbComp.support_eval m_r) ▸ hz₂_eval diff --git a/Complexity/Algorithms/WordRAM/KargerStein.lean b/Complexity/Algorithms/WordRAM/KargerStein.lean index 92368fc36..5a2a42a1a 100644 --- a/Complexity/Algorithms/WordRAM/KargerStein.lean +++ b/Complexity/Algorithms/WordRAM/KargerStein.lean @@ -168,7 +168,7 @@ private theorem toOuterMeasure_mono_support {α : Type} (m : ProbComp α) {S T : m.eval.toOuterMeasure S ≤ m.eval.toOuterMeasure T := by classical rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply] - refine ENNReal.tsum_le_tsum fun a => ?_ + refine tsum_le_tsum fun a => ?_ by_cases ha : a ∈ S · simp only [Set.indicator_of_mem ha] by_cases hs : a ∈ m.support @@ -2684,7 +2684,7 @@ theorem fastCutNode_spec {n w : ℕ} {W₀ : Fin n → Fin n → ℕ} have hcompl0 : (ms2_fn z₂.1).eval.toOuterMeasure {zs | zs.1.regs retVal = minCut W₀}ᶜ = 0 := by rw [PMF.toOuterMeasure_apply] - refine ENNReal.tsum_eq_zero.mpr fun zs => ?_ + refine tsum_eq_zero_iff.mpr fun zs => ?_ by_cases hzs_ev : zs ∈ (ms2_fn z₂.1).eval.support · have hzs : zs ∈ (ms2_fn z₂.1).support := (ProbComp.support_eval (ms2_fn z₂.1)) ▸ hzs_ev @@ -3679,7 +3679,7 @@ theorem fastCutAmpLoop_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {mem have hbv₁ : z₁.1.regs bestVal = minCut W := not_not.mp hhit obtain ⟨m_r, hm_r, _, hsup_r, _⟩ := hnext z₁ hz₁ rw [hml_def, hm_r.codeComp_eq, PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply] - refine ENNReal.tsum_eq_zero.mpr fun z₂ => ?_ + refine tsum_eq_zero_iff.mpr fun z₂ => ?_ by_cases hz₂_eval : z₂ ∈ m_r.eval.support · have hz₂ : z₂ ∈ m_r.support := (ProbComp.support_eval m_r) ▸ hz₂_eval have hbv₂ : z₂.1.regs bestVal = minCut W := diff --git a/Complexity/Computability/Complexity/Classes/IP.lean b/Complexity/Computability/Complexity/Classes/IP.lean index d2c73a5bc..d583e0f90 100644 --- a/Complexity/Computability/Complexity/Classes/IP.lean +++ b/Complexity/Computability/Complexity/Classes/IP.lean @@ -148,7 +148,7 @@ theorem acceptProb_eq_acceptProbWith (verifier : WordOracleComp Operation Bool) /-- The acceptance probability sums the masses of the accepting outcomes over final states. -/ theorem acceptProb_eq_tsum (verifier : WordOracleComp Operation Bool) (P : Prover Operation) : acceptProb verifier P = ∑' s, P.run verifier P.init (true, s) := by - rw [acceptProb, PMF.map_apply, ENNReal.tsum_prod', tsum_bool] + rw [acceptProb, PMF.map_apply, tsum_prod', tsum_bool] simp /-- Private coins drawn before any message average the acceptance probabilities of the diff --git a/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean b/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean index dfce7de33..659f372bf 100644 --- a/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean +++ b/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean @@ -413,7 +413,7 @@ private theorem card_filter_not_injective_div_le (n : ℕ) : private theorem tsum_map_mul {β γ : Type*} (μ : PMF β) (m : β → γ) (f : γ → ENNReal) : ∑' c, μ.map m c * f c = ∑' b, μ b * f (m b) := by simp only [PMF.map_apply, ENNReal.tsum_mul_right.symm] - rw [ENNReal.tsum_comm] + rw [tsum_comm] refine tsum_congr fun b => ?_ rw [tsum_eq_single (m b)] · simp diff --git a/Complexity/Computability/Complexity/Classes/IP/Guessing.lean b/Complexity/Computability/Complexity/Classes/IP/Guessing.lean index 6eaedc8da..02e8929d3 100644 --- a/Complexity/Computability/Complexity/Classes/IP/Guessing.lean +++ b/Complexity/Computability/Complexity/Classes/IP/Guessing.lean @@ -77,8 +77,8 @@ noncomputable def Prover.guessProb (P : Prover Unit) (s : P.State) (m : List Boo theorem Prover.guessProb_add_le_one (P : Prover Unit) (s : P.State) (m : List Bool) : P.guessProb s m false + P.guessProb s m true ≤ 1 := by simp only [Prover.guessProb, PMF.map_apply] - rw [← ENNReal.tsum_add, ← PMF.tsum_coe ((P.respond ((), m)).run s)] - refine ENNReal.tsum_le_tsum fun y => ?_ + rw [← tsum_add, ← PMF.tsum_coe ((P.respond ((), m)).run s)] + refine tsum_le_tsum fun y => ?_ by_cases h : List.take 1 y.1 = [false] · simp [h] · by_cases h' : List.take 1 y.1 = [true] <;> simp [h, h'] @@ -120,7 +120,7 @@ theorem acceptProb_guessingRound_le {message : Bool → ProbComp (List Bool)} { exact hclose _ fun m => PMF.coe_le_one _ _ _ = ∑' m, ProbComp.eval (message false) m * (P.guessProb P.init m false + P.guessProb P.init m true) + δ := by - rw [← add_assoc, ← ENNReal.tsum_add] + rw [← add_assoc, ← tsum_add] simp only [mul_add] _ ≤ 1 + δ := by gcongr diff --git a/Complexity/Computability/Complexity/Classes/IP/OptimalProver.lean b/Complexity/Computability/Complexity/Classes/IP/OptimalProver.lean index 3ad366c14..7fd4eec66 100644 --- a/Complexity/Computability/Complexity/Classes/IP/OptimalProver.lean +++ b/Complexity/Computability/Complexity/Classes/IP/OptimalProver.lean @@ -304,7 +304,7 @@ private theorem sum_acceptFrom_after_le (hF : IsBounded F D L) (P : Prover Unit) lia rw [Finset.sum_eq_zero fun m _ => ?_, add_zero] · split_ifs <;> simp - · refine ENNReal.tsum_eq_zero.mpr fun ys => ?_ + · refine tsum_eq_zero_iff.mpr fun ys => ?_ rw [after_append] unfold outcome at hnil rcases hah : after (F r) h with _ | ⟨b⟩ | ⟨q, next⟩ @@ -320,12 +320,12 @@ private theorem sum_acceptFrom_after_le (hF : IsBounded F D L) (P : Prover Unit) exact (Finset.sum_congr rfl fun r _ => by split_ifs <;> simp).le rw [Finset.sum_comm] refine Finset.sum_le_sum fun m _ => ?_ - rw [← Summable.tsum_finsetSum fun r _ => ENNReal.summable] + rw [← Summable.tsum_finsetSum fun r _ => CompleteLattice.summable] calc ∑' ys : List Bool × P.State, ∑ r, (P.respond ((), m)).run s ys * acceptFrom P ys.2 (after (F r) (h ++ [(m, ys.1)])) ≤ ∑' ys : List Bool × P.State, (P.respond ((), m)).run s ys * ((BitString.shortWords L).sup fun y => value F L n (h ++ [(m, y)]) : ℕ) := by - refine ENNReal.tsum_le_tsum fun ys => ?_ + refine tsum_le_tsum fun ys => ?_ rw [← Finset.mul_sum] refine mul_le_mul_right ?_ _ refine (ih (h ++ [(m, ys.1)]) (by @@ -395,7 +395,7 @@ private theorem sum_acceptFrom_optimalProver_after (hF : IsBounded F D L) (n : lia rw [Finset.sum_eq_zero fun m _ => ?_, add_zero] · split_ifs <;> simp - · refine ENNReal.tsum_eq_zero.mpr fun ys => ?_ + · refine tsum_eq_zero_iff.mpr fun ys => ?_ rw [after_append] unfold outcome at hnil rcases hah : after (F r) h with _ | ⟨b⟩ | ⟨q, next⟩ diff --git a/Complexity/Computability/Complexity/Classes/IP/Repetition.lean b/Complexity/Computability/Complexity/Classes/IP/Repetition.lean index 66023d528..77f8fb503 100644 --- a/Complexity/Computability/Complexity/Classes/IP/Repetition.lean +++ b/Complexity/Computability/Complexity/Classes/IP/Repetition.lean @@ -64,7 +64,7 @@ private theorem acceptProb_bind_ite (P : Prover Operation) acceptProb (do let ok ← round; if ok then rest else pure false) P = ∑' s, P.run round P.init (true, s) * acceptProb rest { P with init := s } := by simp only [acceptProb, Prover.run_bind, PMF.map_bind] - rw [PMF.bind_apply, ENNReal.tsum_prod', tsum_bool] + rw [PMF.bind_apply, tsum_prod', tsum_bool] simp only [Bool.false_eq_true, Bool.true_eq_false, ↓reduceIte, Prover.run_pure, PMF.pure_map, PMF.pure_apply, mul_zero, tsum_zero, zero_add] rfl @@ -81,7 +81,7 @@ theorem acceptProb_sequentialRepeat_le {round : WordOracleComp Operation Bool} { calc ∑' s, P.run round P.init (true, s) * acceptProb (sequentialRepeat k round) { P with init := s } ≤ ∑' s, P.run round P.init (true, s) * ε ^ k := - ENNReal.tsum_le_tsum fun s => mul_le_mul' le_rfl (ih _) + tsum_le_tsum fun s => mul_le_mul' le_rfl (ih _) _ = (∑' s, P.run round P.init (true, s)) * ε ^ k := ENNReal.tsum_mul_right _ ≤ ε * ε ^ k := by gcongr @@ -103,7 +103,7 @@ theorem le_acceptProb_sequentialRepeat {round : WordOracleComp Operation Bool} { gcongr exact (h s).trans_eq (acceptProb_eq_tsum round _) _ = ∑' s', P.run round s (true, s') * c ^ k := ENNReal.tsum_mul_right.symm - _ ≤ _ := ENNReal.tsum_le_tsum fun s' => mul_le_mul' le_rfl (ih s') + _ ≤ _ := tsum_le_tsum fun s' => mul_le_mul' le_rfl (ih s') /-- A constant number of sequential runs of a strict oracle PPT verifier is strict oracle PPT. -/ theorem isOraclePPTOn_sequentialRepeat [DecidableEq Operation] [Finite Operation] diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/Amplification.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/Amplification.lean index 1c3606355..56fd01273 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/Amplification.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/Amplification.lean @@ -126,7 +126,7 @@ theorem eval_runClosed_orElse_apply (h₁ : first.toNTM.RunsInTime input t₁) exact congrArg _ (PMF.pure_apply_self _) · rw [add_zero] _ = q + ProbComp.eval (first.runClosed t₁ input) [true] * (1 - q) := by - rw [ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, tsum_ite_eq] + rw [tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, tsum_ite_eq] /-- **Rejections multiply under `orElse`.** Counted on coin strings, the probability that `first.orElse second` does not accept is the product of the probabilities that `first` and diff --git a/Complexity/Computability/Complexity/Classes/MIP/OptimalProver.lean b/Complexity/Computability/Complexity/Classes/MIP/OptimalProver.lean index ebf6834a9..0f1a57869 100644 --- a/Complexity/Computability/Complexity/Classes/MIP/OptimalProver.lean +++ b/Complexity/Computability/Complexity/Classes/MIP/OptimalProver.lean @@ -581,7 +581,7 @@ private theorem tsum_mul_le_bestOfList (μ : PMF α) (g : α → ℝ≥0∞) (de ∑' x, μ x * g x ≤ g (bestOfList g default l) := by calc ∑' x, μ x * g x ≤ ∑' x, μ x * g (bestOfList g default l) := by - refine ENNReal.tsum_le_tsum fun x => ?_ + refine tsum_le_tsum fun x => ?_ by_cases hx : x ∈ μ.support · exact mul_le_mul_right (le_bestOfList g default l (hsupp x hx)) (μ x) · rw [PMF.mem_support_iff, not_not] at hx @@ -618,7 +618,7 @@ theorem exists_deterministic_prover_family [Finite ι] [DecidableEq ι] {γ : Ty rw [run_eq_bind_piPresample (hF c) P (fun _ => d) (fun _ => le_rfl) (Prover.independent P).init, PMF.bind_apply] simp only [hc, ← ENNReal.tsum_mul_left] - rw [← Summable.tsum_finsetSum fun _ _ => ENNReal.summable] + rw [← Summable.tsum_finsetSum fun _ _ => CompleteLattice.summable] refine tsum_congr fun f => ?_ rw [Finset.mul_sum] exact Finset.sum_congr rfl fun c _ => by rw [mul_left_comm] diff --git a/Complexity/Computability/Complexity/FineGrained/PPSZ/Basic.lean b/Complexity/Computability/Complexity/FineGrained/PPSZ/Basic.lean index e47a1f654..a73035873 100644 --- a/Complexity/Computability/Complexity/FineGrained/PPSZ/Basic.lean +++ b/Complexity/Computability/Complexity/FineGrained/PPSZ/Basic.lean @@ -276,7 +276,7 @@ theorem ppz_round_apply_le {φ : CNF (Fin n)} {w : ℕ} (hw : 1 ≤ w) {σ : Fin (hσ : φ.eval σ = true) : PPZ.round φ (fun x => some (σ x)) ≤ round φ w (fun x => some (σ x)) := by rw [PPZ.round, round, PPZ.roundWith, PPZ.roundWith, PMF.bind_apply, PMF.bind_apply] - refine ENNReal.tsum_le_tsum fun π => mul_le_mul_right ?_ _ + refine tsum_le_tsum fun π => mul_le_mul_right ?_ _ rw [← PPZ.restrict_prefixSet_self σ π] rw [PPZ.runWith_apply_restrict (O := PPZ.forced φ) (fun _ hτ _ _ h => PPZ.forced_eq hσ hτ h) π le_rfl, PPZ.runWith_apply_restrict (O := implied φ w) (fun _ hτ _ _ h => implied_eq hσ hτ h) π diff --git a/Complexity/Computability/Complexity/FineGrained/PPZ.lean b/Complexity/Computability/Complexity/FineGrained/PPZ.lean index 29084952a..a7c4fa2c3 100644 --- a/Complexity/Computability/Complexity/FineGrained/PPZ.lean +++ b/Complexity/Computability/Complexity/FineGrained/PPZ.lean @@ -458,7 +458,7 @@ theorem runWith_apply_restrict {O : (Fin n → Option Bool) → Fin n → Option by_cases hsupp : τ ∈ (runWith O π i).support · rw [PMF.map_apply] convert mul_zero _ - refine ENNReal.tsum_eq_zero.mpr fun b => ite_eq_right fun e => hτ ?_ + refine tsum_eq_zero_iff.mpr fun b => ite_eq_right fun e => hτ ?_ funext y by_cases hy : y = x · subst hy diff --git a/Complexity/Computability/Interactive/Plain.lean b/Complexity/Computability/Interactive/Plain.lean index 23a157b84..822083780 100644 --- a/Complexity/Computability/Interactive/Plain.lean +++ b/Complexity/Computability/Interactive/Plain.lean @@ -201,9 +201,9 @@ private theorem rbrFrom_le : ∀ (s : Spec) (smp : PerChallenge ProbComp s) st' calc ∑' c, ProbComp.eval smp.1 c * _ ≤ ∑' c, ProbComp.eval smp.1 c * (A.indicator 1 c + PerChallenge.sum s ε.2) := - ENNReal.tsum_le_tsum fun c => by gcongr; exact hinner c + tsum_le_tsum fun c => by gcongr; exact hinner c _ = (ProbComp.eval smp.1).toOuterMeasure A + PerChallenge.sum s ε.2 := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, PMF.toOuterMeasure_apply] congr 1 refine tsum_congr fun c => ?_ diff --git a/Complexity/Computability/Kolmogorov/AverageCase.lean b/Complexity/Computability/Kolmogorov/AverageCase.lean index 0ead74cf0..86083ba86 100644 --- a/Complexity/Computability/Kolmogorov/AverageCase.lean +++ b/Complexity/Computability/Kolmogorov/AverageCase.lean @@ -277,7 +277,7 @@ private theorem pmf_map_true_le_one_sub_of_imp_false {α : Type*} (q : PMF α) ( ((q.map P) true).toReal ≤ 1 - ((q.map Q) true).toReal := by have hle : (q.map P) true ≤ (q.map Q) false := by rw [PMF.map_apply, PMF.map_apply] - refine ENNReal.tsum_le_tsum fun v => ?_ + refine tsum_le_tsum fun v => ?_ by_cases hp : P v = true · have hq : Q v = false := hdisj v hp simp [hp, hq] @@ -292,7 +292,7 @@ private theorem pmf_map_true_le_of_imp_true {α : Type*} (q : PMF α) (P Q : α ((q.map P) true).toReal ≤ ((q.map Q) true).toReal := by apply ENNReal.toReal_mono (PMF.apply_ne_top _ _) rw [PMF.map_apply, PMF.map_apply] - refine ENNReal.tsum_le_tsum fun v => ?_ + refine tsum_le_tsum fun v => ?_ by_cases hp : P v = true · have hq : Q v = true := himp v hp simp [hp, hq] diff --git a/Complexity/Computability/PCP/TwoProverGame.lean b/Complexity/Computability/PCP/TwoProverGame.lean index d918d1eba..e742d8fc8 100644 --- a/Complexity/Computability/PCP/TwoProverGame.lean +++ b/Complexity/Computability/PCP/TwoProverGame.lean @@ -117,7 +117,7 @@ theorem winProb_shared_le_value [Nonempty A] [Nonempty B] {R : Type*} (ρ : PMF exact ENNReal.ofReal_le_ofReal (G.winProb_le_value (fun x => ha x r) (fun y => hb y r)) calc ∑' r, ρ r * (G.questions.map fun q => (q, ha q.1 r, hb q.2 r)).toOuterMeasure {z | G.accepts z.1.1 z.1.2 z.2.1 z.2.2} - ≤ ∑' r, ρ r * ENNReal.ofReal G.value := ENNReal.tsum_le_tsum fun r => by gcongr; exact hr r + ≤ ∑' r, ρ r * ENNReal.ofReal G.value := tsum_le_tsum fun r => by gcongr; exact hr r _ = ENNReal.ofReal G.value := by rw [ENNReal.tsum_mul_right, ρ.tsum_coe, one_mul] end Finite diff --git a/Complexity/Computability/WordRAM/Randomized/Expected.lean b/Complexity/Computability/WordRAM/Randomized/Expected.lean index 7d9e1844a..4f1881163 100644 --- a/Complexity/Computability/WordRAM/Randomized/Expected.lean +++ b/Complexity/Computability/WordRAM/Randomized/Expected.lean @@ -117,7 +117,7 @@ theorem evalRand_haltedSet_mono (w : ℕ) (p : Program B r) (s : State r) : rw [evalRand, runRand_add w p T 1, ProbComp.eval_bind] simp only [evalRand, runRand_succ, runRand_zero, bind_pure] rw [hstep, PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply] - refine ENNReal.tsum_le_tsum fun cfg => ?_ + refine tsum_le_tsum fun cfg => ?_ by_cases hcfg : cfg ∈ RandCfg.haltedSet r · have hmem := hcfg obtain ⟨v, d, rfl⟩ := hcfg @@ -139,7 +139,7 @@ theorem RandHaltsWithin.almostSurelyHalts {w T : ℕ} {p : Program B r} {s : Sta exact hnot (h cfg hmem) have hsum : (evalRand w p T s).toOuterMeasure (RandCfg.haltedSet r) + (evalRand w p T s).toOuterMeasure (RandCfg.haltedSet r)ᶜ = 1 := by - rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add] + rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add] convert (evalRand w p T s).tsum_coe using 1 congr 1 funext cfg @@ -172,7 +172,7 @@ theorem expectedStepsFrom_faulted (w : ℕ) (p : Program B r) : private theorem tsum_nat_eq_zero_add (g : ℕ → ℝ≥0∞) : ∑' t : ℕ, g t = g 0 + ∑' t : ℕ, g (t + 1) := by - rw [ENNReal.tsum_eq_add_tsum_ite (f := g) 0] + rw [tsum_eq_add_tsum_ite (f := g) 0] congr 1 have hsh := Function.Injective.tsum_eq Nat.succ_injective (f := fun t => if t = 0 then 0 else g t) fun t ht => by @@ -199,7 +199,7 @@ theorem expectedStepsFrom_running (w : ℕ) (p : Program B r) (s : State r) : intro t rw [runRand_succ, ProbComp.eval_bind, PMF.toOuterMeasure_bind_apply] simp only [hsucc] - rw [ENNReal.tsum_comm] + rw [tsum_comm] simp only [ProbComp.expect, expectedStepsFrom, ENNReal.tsum_mul_left] /-- Under `RandFaultFree`, every horizon partitions probability `1` between `.running` and @@ -208,7 +208,7 @@ theorem RandFaultFree.running_add_halted_eq_one {w : ℕ} {p : Program B r} {s : (hf : RandFaultFree w p s) (t : ℕ) : (evalRand w p t s).toOuterMeasure {cfg | ∃ u, cfg = .running u} + (evalRand w p t s).toOuterMeasure (RandCfg.haltedSet r) = 1 := by - rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add] + rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add] convert (evalRand w p t s).tsum_coe using 1 congr 1 funext cfg @@ -242,7 +242,7 @@ theorem AlmostSurelyHalts.of_expectedTime_ne_top {w : ℕ} {p : Program B r} {s have hinf : (⊤ : ℝ≥0∞) ≤ expectedTime w p s := by calc (⊤ : ℝ≥0∞) = ∑' _ : ℕ, (1 - supH) := (ENNReal.tsum_const_eq_top_of_ne_zero hpos.ne').symm - _ ≤ expectedTime w p s := ENNReal.tsum_le_tsum hle_run + _ ≤ expectedTime w p s := tsum_le_tsum hle_run exact htop (top_unique hinf) /-- Under `RandHaltsWithin w p s T`, the active-configuration tail sum vanishes from `T` onward and diff --git a/Complexity/Crypto/Computational/CramerShoup/ProjectiveHash.lean b/Complexity/Crypto/Computational/CramerShoup/ProjectiveHash.lean index 09e298a66..c52fe95e6 100644 --- a/Complexity/Crypto/Computational/CramerShoup/ProjectiveHash.lean +++ b/Complexity/Crypto/Computational/CramerShoup/ProjectiveHash.lean @@ -555,8 +555,8 @@ theorem uniform_projHash2_fiber_any_le (d : F.Desc) [DecidableEq (F.Carrier d)] have hor : (μ.map (fun τ₂ => (q :: qs).any (fun q' => hit q' τ₂))) true ≤ (μ.map (hit q)) true + (μ.map (fun τ₂ => qs.any (fun q' => hit q' τ₂))) true := by - simp only [List.any_cons, PMF.map_apply, ← ENNReal.tsum_add] - refine ENNReal.tsum_le_tsum fun τ₂ => ?_ + simp only [List.any_cons, PMF.map_apply, ← tsum_add] + refine tsum_le_tsum fun τ₂ => ?_ cases hit q τ₂ <;> cases qs.any (fun q' => hit q' τ₂) <;> simp have hsingle : (μ.map (hit q)) true = (F.order d : ℝ≥0∞)⁻¹ := by have heq : diff --git a/Complexity/Crypto/Computational/CramerShoup/Scheme.lean b/Complexity/Crypto/Computational/CramerShoup/Scheme.lean index 58a4a0937..0e6744c8c 100644 --- a/Complexity/Crypto/Computational/CramerShoup/Scheme.lean +++ b/Complexity/Crypto/Computational/CramerShoup/Scheme.lean @@ -1008,7 +1008,7 @@ private theorem tsum_and_isCramerShoupBadDH_le rw [hpre, Bool.true_and, ← hvElem, ← hwElem, encodeProjHash2_encode, he_equiv τ] rw [hbad_eq] cases cond <;> cases F.encode d (e_equiv τ • F.generator d) == parts.2.2.2 <;> simp - exact (ENNReal.tsum_le_tsum fun τ => + exact (tsum_le_tsum fun τ => mul_le_mul_of_nonneg_left (hle τ) zero_le).trans (F.tsum_uniform_smul_generator_eq e_equiv parts.2.2.2) · simp only [Bool.not_eq_true] at hpre diff --git a/Complexity/Crypto/Computational/DiffieHellman.lean b/Complexity/Crypto/Computational/DiffieHellman.lean index 00a002fc8..2f8a35c45 100644 --- a/Complexity/Crypto/Computational/DiffieHellman.lean +++ b/Complexity/Crypto/Computational/DiffieHellman.lean @@ -173,14 +173,14 @@ theorem succProbability_discreteLogGame_le_cdhGame (setup : ℕ → PMF F.Desc) simp only [discreteLogGame, cdhGame, dlToCDHAdversary, ProbComp.eval_bind, ProbComp.eval_pure, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] rw [PMF.bind_apply, PMF.bind_apply] - refine ENNReal.tsum_le_tsum fun d => mul_le_mul_of_nonneg_left ?_ zero_le + refine tsum_le_tsum fun d => mul_le_mul_of_nonneg_left ?_ zero_le rw [PMF.bind_apply, PMF.bind_apply] - refine ENNReal.tsum_le_tsum fun α => mul_le_mul_of_nonneg_left ?_ zero_le + refine tsum_le_tsum fun α => mul_le_mul_of_nonneg_left ?_ zero_le rw [← PMF.bind_const (PMF.uniformOfFintype (ZMod (F.order d))) ((ProbComp.eval (adversary n (d, F.encode d (α • F.generator d)))).bind _)] rw [PMF.bind_apply, PMF.bind_apply] - refine ENNReal.tsum_le_tsum fun β => mul_le_mul_of_nonneg_left ?_ zero_le - refine ENNReal.tsum_le_tsum fun guess => mul_le_mul_of_nonneg_left ?_ zero_le + refine tsum_le_tsum fun β => mul_le_mul_of_nonneg_left ?_ zero_le + refine tsum_le_tsum fun guess => mul_le_mul_of_nonneg_left ?_ zero_le by_cases hα : (ofBits guess : ZMod (F.order d)) = α · simp only [hα, F.smul_encode, smul_smul, decide_true, le_rfl] · simp only [hα, decide_false, PMF.pure_apply, Bool.true_eq_false, ↓reduceIte, zero_le] @@ -301,7 +301,7 @@ theorem ddhIdealGame_cdhToDDHDistinguisher_true_le (setup : ℕ → PMF F.Desc) fun guess => PMF.pure (decide (guess = F.encode d (γ • F.generator d)))) true ≤ ∑' d, setup n d * (m : ℝ≥0∞)⁻¹ := by - refine ENNReal.tsum_le_tsum fun d => ?_ + refine tsum_le_tsum fun d => ?_ by_cases hd : d ∈ (setup n).support · refine mul_le_mul_of_nonneg_left ?_ zero_le have hord : (F.order d : ℝ≥0∞)⁻¹ ≤ (m : ℝ≥0∞)⁻¹ := @@ -315,8 +315,8 @@ theorem ddhIdealGame_cdhToDDHDistinguisher_true_le (setup : ℕ → PMF F.Desc) PMF.pure (decide (guess = F.encode d (γ • F.generator d)))) true ≤ ∑' α, PMF.uniformOfFintype (ZMod (F.order d)) α * ∑' β, PMF.uniformOfFintype (ZMod (F.order d)) β * (m : ℝ≥0∞)⁻¹ := by - refine ENNReal.tsum_le_tsum fun α => mul_le_mul_of_nonneg_left ?_ zero_le - refine ENNReal.tsum_le_tsum fun β => mul_le_mul_of_nonneg_left ?_ zero_le + refine tsum_le_tsum fun α => mul_le_mul_of_nonneg_left ?_ zero_le + refine tsum_le_tsum fun β => mul_le_mul_of_nonneg_left ?_ zero_le rw [PMF.bind_comm, PMF.bind_apply] calc ∑' guess, ProbComp.eval (adversary n (d, F.encode d (α • F.generator d), F.encode d (β • F.generator d))) guess * @@ -325,7 +325,7 @@ theorem ddhIdealGame_cdhToDDHDistinguisher_true_le (setup : ℕ → PMF F.Desc) ≤ ∑' guess, ProbComp.eval (adversary n (d, F.encode d (α • F.generator d), F.encode d (β • F.generator d))) guess * (m : ℝ≥0∞)⁻¹ := by - refine ENNReal.tsum_le_tsum fun guess => + refine tsum_le_tsum fun guess => mul_le_mul_of_nonneg_left ((F.uniform_decide_eq_encode_le d guess).trans hord) zero_le _ = (m : ℝ≥0∞)⁻¹ := by rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] diff --git a/Complexity/Crypto/Computational/DiffieHellman/Order.lean b/Complexity/Crypto/Computational/DiffieHellman/Order.lean index b0a3dbafa..478cd484b 100644 --- a/Complexity/Crypto/Computational/DiffieHellman/Order.lean +++ b/Complexity/Crypto/Computational/DiffieHellman/Order.lean @@ -138,7 +138,7 @@ private theorem expected_inv_order_le_two_mul_advantage_ddh (F : PrimeOrderGroup (((F.order d - 1 : ℕ) : ℝ≥0∞) * ((F.order d : ℝ≥0∞)⁻¹ * (F.order d : ℝ≥0∞)⁻¹))) := by dsimp only [ddhRealGame, ddhZeroDistinguisher] simp only [ProbComp.eval_pure, PMF.monad_bind_eq_bind, PMF.bind_apply] - rw [← ENNReal.tsum_add] + rw [← tsum_add] refine tsum_congr fun d => ?_ have hstep : (∑' α, PMF.uniformOfFintype (ZMod (F.order d)) α * @@ -164,7 +164,7 @@ private theorem expected_inv_order_le_two_mul_advantage_ddh (F : PrimeOrderGroup 2 * ∑' d, setup n d * (((F.order d - 1 : ℕ) : ℝ≥0∞) * ((F.order d : ℝ≥0∞)⁻¹ * (F.order d : ℝ≥0∞)⁻¹)) := by rw [← ENNReal.tsum_mul_left] - refine ENNReal.tsum_le_tsum fun d => ?_ + refine tsum_le_tsum fun d => ?_ rw [← mul_assoc, mul_comm (2 : ℝ≥0∞) (setup n d), mul_assoc] refine mul_le_mul_of_nonneg_left ?_ zero_le have hq2 : 2 ≤ F.order d := (F.prime_order d).two_le diff --git a/Complexity/Crypto/Computational/Encryption/Authenticated.lean b/Complexity/Crypto/Computational/Encryption/Authenticated.lean index a177011ae..951e29dce 100644 --- a/Complexity/Crypto/Computational/Encryption/Authenticated.lean +++ b/Complexity/Crypto/Computational/Encryption/Authenticated.lean @@ -1662,7 +1662,7 @@ private theorem ennreal_tsum_finsetSum {α β : Type*} induction s using Finset.induction_on with | empty => simp | insert b s hb ih => - simp only [Finset.sum_insert hb, ENNReal.tsum_add, ih] + simp only [Finset.sum_insert hb, tsum_add, ih] private theorem eval_ccaRejectWithBadOracle_false (E : SymmetricCipher) (n : ℕ) (k : List Bool) (bit : Bool) (request : Bool × List Bool) (queried : List (List Bool)) : @@ -1761,7 +1761,7 @@ private theorem bad_ccaRejectWithBad_le_sum_ciCombined {α : Type} (E : Symmetri (fun x => PMF.pure (!x.2.2.contains x.2.1.2.2 && (E.decrypt n k x.2.1.2.2).isSome)) true := - ENNReal.tsum_le_tsum fun a => mul_le_mul_of_nonneg_left (ih a queried) zero_le + tsum_le_tsum fun a => mul_le_mul_of_nonneg_left (ih a queried) zero_le _ = _ := by simp only [Finset.mul_sum] rw [ennreal_tsum_finsetSum] @@ -1818,7 +1818,7 @@ private theorem bad_ccaRejectWithBad_le_sum_ciCombined {α : Type} (E : Symmetri PMF.pure (!x.2.2.contains x.2.1.2.2 && (E.decrypt n k x.2.1.2.2).isSome)) true := - ENNReal.tsum_le_tsum fun ct => + tsum_le_tsum fun ct => mul_le_mul_of_nonneg_left (ih ct (ct :: queried)) zero_le _ = _ := by simp only [Finset.mul_sum] @@ -1993,8 +1993,8 @@ private theorem advantage_ccaGame_ccaRejectGame_le_sum (E : SymmetricCipher) (ct ProbOracleComp.eval_run_interpret, hrejEq] exact PMF.bind_apply _ _ _ have hle1 : pCCA ≤ pRej + pSum := by - rw [hCCA_eq, hRej_eq, hsum_eq, ← ENNReal.tsum_add] - refine ENNReal.tsum_le_tsum fun k => ?_ + rw [hCCA_eq, hRej_eq, hsum_eq, ← tsum_add] + refine tsum_le_tsum fun k => ?_ rw [← mul_add] by_cases hk : k ∈ (ProbComp.eval (E.keyGen n)).support · refine mul_le_mul_of_nonneg_left ?_ zero_le @@ -2007,8 +2007,8 @@ private theorem advantage_ccaGame_ccaRejectGame_le_sum (E : SymmetricCipher) (ct rw [eval_ciGame_ccaToCIAtIndexAdversary_key E ctBound j bit adversary n k hk hctBound] · rw [(PMF.apply_eq_zero_iff _ _).mpr hk, zero_mul, zero_mul] have hle2 : pRej ≤ pCCA + pSum := by - rw [hCCA_eq, hRej_eq, hsum_eq, ← ENNReal.tsum_add] - refine ENNReal.tsum_le_tsum fun k => ?_ + rw [hCCA_eq, hRej_eq, hsum_eq, ← tsum_add] + refine tsum_le_tsum fun k => ?_ rw [← mul_add] by_cases hk : k ∈ (ProbComp.eval (E.keyGen n)).support · refine mul_le_mul_of_nonneg_left ?_ zero_le diff --git a/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean b/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean index d8d240fb8..e33925650 100644 --- a/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean +++ b/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean @@ -1629,7 +1629,7 @@ private theorem step_bad_prfCipherForgetfulWithBadOracle_le (n : ℕ) (bit : Boo {x | x.2.2 = true} ≤ ∑' r, (BitString.uniformList n) r * {r : List Bool | (cache.lookup r).isSome}.indicator 1 r := by - refine ENNReal.tsum_le_tsum fun r => mul_le_mul_of_nonneg_left ?_ zero_le + refine tsum_le_tsum fun r => mul_le_mul_of_nonneg_left ?_ zero_le by_cases hr : (cache.lookup r).isSome = true · rw [Set.indicator_of_mem (show r ∈ {r : List Bool | (cache.lookup r).isSome} from hr), Pi.one_apply] @@ -1697,7 +1697,7 @@ private theorem bad_prfCipherForgetfulWithBadOracle_le {α : Type} (n : ℕ) (bi (cont y.1)).run y.2).toOuterMeasure {x | x.2.2 = true} ≤ ∑' y, ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit) (Sum.inl m) (cache, false) y * B := by - refine ENNReal.tsum_le_tsum fun y => ?_ + refine tsum_le_tsum fun y => ?_ by_cases hy : y ∈ (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit) (Sum.inl m) (cache, false)).support @@ -1749,10 +1749,10 @@ private theorem bad_prfCipherForgetfulWithBadOracle_le {α : Type} (n : ℕ) (bi ≤ ∑' y, prfCipherForgetfulWithBadOracle n bit request (cache, false) y * ({x : List Bool × (List (List Bool × List Bool) × Bool) | x.2.2 = true}.indicator 1 y + K) := - ENNReal.tsum_le_tsum hterm + tsum_le_tsum hterm _ = (prfCipherForgetfulWithBadOracle n bit request (cache, false)).toOuterMeasure {x | x.2.2 = true} + K := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, PMF.toOuterMeasure_apply] congr 1 refine tsum_congr fun y => ?_ diff --git a/Complexity/Crypto/Computational/GMW/Soundness.lean b/Complexity/Crypto/Computational/GMW/Soundness.lean index 7841dd8ec..99dcd2c2f 100644 --- a/Complexity/Crypto/Computational/GMW/Soundness.lean +++ b/Complexity/Crypto/Computational/GMW/Soundness.lean @@ -562,7 +562,7 @@ theorem acceptProb_gmwVerifier_le {α : Type} {generator : List Bool → List Bo P.init x * ProbOracleComp.acceptProbWith P.respond (step2 r x.1) x.2 ≤ ∑' x, ProbOracleComp.runWith P.respond (List.take (K * m) <$> ProbOracleComp.query ((), r)) P.init x * (1 / 8) := - ENNReal.tsum_le_tsum fun x => mul_le_mul_right (hstep2_le r x.1 x.2 hbind) _ + tsum_le_tsum fun x => mul_le_mul_right (hstep2_le r x.1 x.2 hbind) _ _ = (∑' x, ProbOracleComp.runWith P.respond (List.take (K * m) <$> ProbOracleComp.query ((), r)) P.init x) * (1 / 8) := ENNReal.tsum_mul_right @@ -591,9 +591,9 @@ theorem acceptProb_gmwVerifier_le {α : Type} {generator : List Bool → List Bo calc ∑' r, BitString.uniformList m r * acceptProb (step1 r) P ≤ ∑' r, (({r | ¬ NaorBinding generator s r}.indicator (BitString.uniformList m) r) + - BitString.uniformList m r * (1 / 8)) := ENNReal.tsum_le_tsum hterm_le + BitString.uniformList m r * (1 / 8)) := tsum_le_tsum hterm_le _ = (∑' r, {r | ¬ NaorBinding generator s r}.indicator (BitString.uniformList m) r) + - ∑' r, BitString.uniformList m r * (1 / 8) := ENNReal.tsum_add + ∑' r, BitString.uniformList m r * (1 / 8) := tsum_add _ = naorBindingProb generator length s + 1 / 8 := by rw [← PMF.toOuterMeasure_apply, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] rfl diff --git a/Complexity/Crypto/Computational/MAC.lean b/Complexity/Crypto/Computational/MAC.lean index 5b35fad27..5d8f4e36f 100644 --- a/Complexity/Crypto/Computational/MAC.lean +++ b/Complexity/Crypto/Computational/MAC.lean @@ -797,7 +797,7 @@ private theorem pmf_bind_pure_bool_le {α : Type} (p : PMF α) (f g : α → Boo (p.bind (fun a => PMF.pure (f a))) true ≤ (p.bind (fun a => PMF.pure (g a))) true := by rw [PMF.bind_apply, PMF.bind_apply] - refine ENNReal.tsum_le_tsum fun a => ?_ + refine tsum_le_tsum fun a => ?_ by_cases ha : a ∈ p.support · refine mul_le_mul_of_nonneg_left ?_ zero_le cases hf : f a @@ -816,7 +816,7 @@ theorem succProbability_eufCmaGame_le_sufCmaGame (M : MACScheme) simp only [Game.succProbability, sufCmaGame, ProbComp.eval_bind, ProbComp.eval_pure] refine ENNReal.toNNReal_mono (PMF.apply_ne_top _ true) ?_ rw [PMF.bind_apply, PMF.bind_apply] - refine ENNReal.tsum_le_tsum fun sk => ?_ + refine tsum_le_tsum fun sk => ?_ refine mul_le_mul_of_nonneg_left (pmf_bind_pure_bool_le _ _ _ fun out _ hout => ?_) zero_le simp only [Bool.and_eq_true, Bool.not_eq_true'] at hout ⊢ refine ⟨⟨hout.1.1, ?_⟩, hout.2⟩ @@ -1450,7 +1450,7 @@ theorem succProbability_prfIdealGame_macToPrfDistinguisher_le (adversary : Forge zero_le] have htotal : (phase1.bind phase2) true ≤ (1 : ℝ≥0∞) / 2 ^ n := by rw [PMF.bind_apply] - refine (ENNReal.tsum_le_tsum fun a => ?_).trans + refine (tsum_le_tsum fun a => ?_).trans (PMF.tsum_mul_le_of_forall_le phase1 fun _ => le_rfl) by_cases ha : a ∈ phase1.support · exact mul_le_mul_right (hstep_bound a ha) _ @@ -2012,7 +2012,7 @@ theorem succProbability_eufCmaGame_le_sufCmaGame (M : NonceMACScheme) simp only [Game.succProbability, eufCmaGame, sufCmaGame, ProbComp.eval_bind, ProbComp.eval_pure] refine ENNReal.toNNReal_mono (PMF.apply_ne_top _ true) ?_ rw [PMF.bind_apply, PMF.bind_apply] - refine ENNReal.tsum_le_tsum fun sk => ?_ + refine tsum_le_tsum fun sk => ?_ refine mul_le_mul_of_nonneg_left (MACScheme.pmf_bind_pure_bool_le _ _ _ fun out _ hout => ?_) zero_le simp only [Bool.and_eq_true, Bool.not_eq_true'] at hout ⊢ diff --git a/Complexity/Crypto/Computational/NaorReingold/Security.lean b/Complexity/Crypto/Computational/NaorReingold/Security.lean index ad05595ed..bcc1e4022 100644 --- a/Complexity/Crypto/Computational/NaorReingold/Security.lean +++ b/Complexity/Crypto/Computational/NaorReingold/Security.lean @@ -2995,7 +2995,7 @@ theorem DDH.negligible_naorReingoldHashedGame_const {F : PrimeOrderGroupFamily} refine ne_of_lt (lt_of_le_of_lt ?_ ENNReal.one_lt_top) calc (∑' d, setup n d * (F.order d : ℝ≥0∞)⁻¹) ≤ ∑' d, setup n d * 1 := by - refine ENNReal.tsum_le_tsum fun d => mul_le_mul_of_nonneg_left ?_ (by positivity) + refine tsum_le_tsum fun d => mul_le_mul_of_nonneg_left ?_ (by positivity) exact ENNReal.inv_le_one.mpr (by exact_mod_cast (F.prime_order d).pos) _ = 1 := by simp [(setup n).tsum_coe] have hε_pos : 0 < ε n := by @@ -3007,7 +3007,7 @@ theorem DDH.negligible_naorReingoldHashedGame_const {F : PrimeOrderGroupFamily} ENNReal.mul_pos hd₀_ne hord_ne exact ENNReal.toNNReal_pos (ne_of_gt (lt_of_lt_of_le hterm_pos - (ENNReal.le_tsum (f := fun d => setup n d * (F.order d : ℝ≥0∞)⁻¹) d₀))) + (le_tsum (f := fun d => setup n d * (F.order d : ℝ≥0∞)⁻¹) d₀))) hexp_top let τ : ℝ≥0 := NNReal.sqrt (ε n) have hτ_pos : 0 < τ := NNReal.sqrt_pos.mpr hε_pos @@ -3079,7 +3079,7 @@ theorem DDH.negligible_naorReingoldHashedGame_const {F : PrimeOrderGroupFamily} have hsum_err : (∑' d, setup n d * errTerm d) = ((lhlBound n : ℝ≥0) : ℝ≥0∞) := by dsimp only [errTerm, lhlBound] - simp_rw [mul_add, ENNReal.tsum_add, ← mul_assoc] + simp_rw [mul_add, tsum_add, ← mul_assoc] rw [ENNReal.tsum_mul_right, ENNReal.tsum_mul_right, (setup n).tsum_coe, one_mul, ENNReal.coe_add] congr 1 @@ -3095,8 +3095,8 @@ theorem DDH.negligible_naorReingoldHashedGame_const {F : PrimeOrderGroupFamily} (hfg : ∀ d ∈ (setup n).support, f d true ≤ g d true + ((Game.advantage (g1 d) (g2 d) : ℝ≥0) : ℝ≥0∞)) : ((setup n).bind f) true ≤ ((setup n).bind g) true + ((lhlBound n : ℝ≥0) : ℝ≥0∞) := by - rw [← hsum_err, PMF.bind_apply, PMF.bind_apply, ← ENNReal.tsum_add] - refine ENNReal.tsum_le_tsum fun d => ?_ + rw [← hsum_err, PMF.bind_apply, PMF.bind_apply, ← tsum_add] + refine tsum_le_tsum fun d => ?_ by_cases hd : d ∈ (setup n).support · rw [← mul_add] exact mul_le_mul_of_nonneg_left ((hfg d hd).trans (add_le_add le_rfl (hpoint d hd))) diff --git a/Complexity/Crypto/Computational/OneWay/LiuPassConverse.lean b/Complexity/Crypto/Computational/OneWay/LiuPassConverse.lean index 3c997b6a5..2350d6382 100644 --- a/Complexity/Crypto/Computational/OneWay/LiuPassConverse.lean +++ b/Complexity/Crypto/Computational/OneWay/LiuPassConverse.lean @@ -610,7 +610,7 @@ private theorem heuristic_fail_mul_le_family_fail {t : ℕ → ℕ} (ht : ∀ n, rw [hfailA_eq] dsimp only [failH] rw [PMF.map_apply, PMF.map_apply] - refine ENNReal.tsum_le_tsum fun coins => ?_ + refine tsum_le_tsum fun coins => ?_ split_ifs with h1 h2 · rfl · exfalso diff --git a/Complexity/Crypto/Computational/OneWayToSignature.lean b/Complexity/Crypto/Computational/OneWayToSignature.lean index ce784ba7d..a3cc11acb 100644 --- a/Complexity/Crypto/Computational/OneWayToSignature.lean +++ b/Complexity/Crypto/Computational/OneWayToSignature.lean @@ -663,7 +663,7 @@ private theorem map_bool_apply_true {α : Type*} (p : PMF α) (P : α → Bool) private theorem ennreal_tsum_finsetSum {α ι : Type*} (s : Finset ι) (g : ι → α → ℝ≥0∞) : (∑' a, ∑ i ∈ s, g i a) = ∑ i ∈ s, ∑' a, g i a := - Summable.tsum_finsetSum fun _ _ => ENNReal.summable + Summable.tsum_finsetSum fun _ _ => CompleteLattice.summable /-- **Lamport's one-time signature theorem**: for any one-way function `f`, `lamportScheme f` is existentially unforgeable under one-time adaptive chosen-message attack (`OneTimeEUFCMA`). -/ @@ -817,7 +817,7 @@ theorem OneWay.oneTimeEUFCMA_lamport {f : List Bool → List Bool} (hf : OneWay ≤ ∑' out, ∑ j : Fin (dyadicSize (2 * n)), if j.val < 2 * n then runWith (pkOf w) (dummySkOf w j.val) out * (if invWin w j.val out then 1 else 0) - else 0 := ENNReal.tsum_le_tsum (hpointwise w hw) + else 0 := tsum_le_tsum (hpointwise w hw) _ = ∑ j : Fin (dyadicSize (2 * n)), ∑' out, if j.val < 2 * n then runWith (pkOf w) (dummySkOf w j.val) out * (if invWin w j.val out then 1 else 0) @@ -845,7 +845,7 @@ theorem OneWay.oneTimeEUFCMA_lamport {f : List Bool → List Bool} (hf : OneWay if j.val < 2 * n then ((runWith (pkOf w) (dummySkOf w j.val)).map (invWin w j.val)) true else 0 := by - refine ENNReal.tsum_le_tsum fun w => ?_ + refine tsum_le_tsum fun w => ?_ by_cases hw : w ∈ μ.support · exact mul_le_mul_right (hw_sum w hw) (μ w) · simp [(PMF.apply_eq_zero_iff μ w).mpr hw] diff --git a/Complexity/Crypto/Computational/PRGToOneWay.lean b/Complexity/Crypto/Computational/PRGToOneWay.lean index 1fb8c7c47..70e7f7aea 100644 --- a/Complexity/Crypto/Computational/PRGToOneWay.lean +++ b/Complexity/Crypto/Computational/PRGToOneWay.lean @@ -107,7 +107,7 @@ theorem succProbability_uniformList_test_le {generator : List Bool → List Bool split_ifs with hr · exact PMF.coe_le_one _ _ simp only [test, ProbComp.eval_bind, ProbComp.eval_pure, PMF.bind_apply, PMF.pure_apply] - refine le_of_eq (ENNReal.tsum_eq_zero.2 fun x => ?_) + refine le_of_eq (tsum_eq_zero_iff.2 fun x => ?_) have hne : generator x ≠ List.ofFn r := fun hx => hr <| mem_image.2 ⟨x, hP x (by rw [← hlen x, hx, List.length_ofFn]), hx⟩ simp [hne] diff --git a/Complexity/Crypto/Computational/PedersenCommitment.lean b/Complexity/Crypto/Computational/PedersenCommitment.lean index e77853f5a..09842b79b 100644 --- a/Complexity/Crypto/Computational/PedersenCommitment.lean +++ b/Complexity/Crypto/Computational/PedersenCommitment.lean @@ -405,11 +405,11 @@ theorem pedersenHidingGame_apply_true_le (setup : ℕ → PMF F.Desc) ≤ ∑' α, (PMF.uniformOfFintype (ZMod (F.order d)) α * F.pedersenScheme.hidingForKey ⟨d, α • F.generator d⟩ adversary b₂ n true + if α = 0 then (F.order d : ℝ≥0∞)⁻¹ else 0) := - ENNReal.tsum_le_tsum hα + tsum_le_tsum hα _ = (∑' α, PMF.uniformOfFintype (ZMod (F.order d)) α * F.pedersenScheme.hidingForKey ⟨d, α • F.generator d⟩ adversary b₂ n true) + (F.order d : ℝ≥0∞)⁻¹ := by - rw [ENNReal.tsum_add, tsum_ite_eq] + rw [tsum_add, tsum_ite_eq] _ ≤ (∑' α, PMF.uniformOfFintype (ZMod (F.order d)) α * F.pedersenScheme.hidingForKey ⟨d, α • F.generator d⟩ adversary b₂ n true) + (m : ℝ≥0∞)⁻¹ := add_le_add le_rfl hord @@ -423,7 +423,7 @@ theorem pedersenHidingGame_apply_true_le (setup : ℕ → PMF F.Desc) (((PMF.uniformOfFintype (ZMod (F.order d))).bind fun α => F.pedersenScheme.hidingForKey ⟨d, α • F.generator d⟩ adversary b₂ n) true + (m : ℝ≥0∞)⁻¹) := by - refine ENNReal.tsum_le_tsum fun d => ?_ + refine tsum_le_tsum fun d => ?_ by_cases hd : d ∈ (setup n).support · exact mul_le_mul_of_nonneg_left (hd_bound d hd) zero_le · have hd0 : setup n d = 0 := by rwa [PMF.mem_support_iff, not_not] at hd @@ -432,7 +432,7 @@ theorem pedersenHidingGame_apply_true_le (setup : ℕ → PMF F.Desc) ((PMF.uniformOfFintype (ZMod (F.order d))).bind fun α => F.pedersenScheme.hidingForKey ⟨d, α • F.generator d⟩ adversary b₂ n) true) + (m : ℝ≥0∞)⁻¹ := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, (setup n).tsum_coe, one_mul] + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, (setup n).tsum_coe, one_mul] /-- **Unconditional hiding bound for Pedersen commitments**: when every supported group at parameter `n` has order at least `m > 0`, any (even computationally unbounded) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean b/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean index 9a46827f4..ffd5f9b0b 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/MaskedExtraction.lean @@ -109,7 +109,7 @@ theorem maskedSample_mass_ge {α β : Type} (source : ProbComp α) rw [← ENNReal.toReal_mul] apply ENNReal.toReal_mono (PMF.apply_ne_top _ _) rw [PMF.bind_apply] - exact ENNReal.le_tsum (f := fun x => ProbComp.eval source x * + exact le_tsum (f := fun x => ProbComp.eval source x * ((ProbComp.eval (maskBit (mask x) (truth x))).map (observe x, ·)) (observe value, bit)) value exact (mul_le_mul (hsource value hvalue) (hbitMass.trans hmap) diff --git a/Complexity/Crypto/Game.lean b/Complexity/Crypto/Game.lean index e289aabc6..4f37d2714 100644 --- a/Complexity/Crypto/Game.lean +++ b/Complexity/Crypto/Game.lean @@ -295,16 +295,16 @@ theorem advantage_bind_le {α : Type*} (d : PMF α) (game1 game2 : α → Game) rw [PMF.bind_apply, PMF.bind_apply] calc ∑' a, d a * game1 a true ≤ ∑' a, d a * (game2 a true + ENNReal.ofReal ε) := - ENNReal.tsum_le_tsum fun a => mul_le_mul_of_nonneg_left (h1 a) zero_le + tsum_le_tsum fun a => mul_le_mul_of_nonneg_left (h1 a) zero_le _ = (∑' a, d a * game2 a true) + ENNReal.ofReal ε := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, d.tsum_coe, one_mul] + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, d.tsum_coe, one_mul] have hsum2 : (d.bind game2) true ≤ (d.bind game1) true + ENNReal.ofReal ε := by rw [PMF.bind_apply, PMF.bind_apply] calc ∑' a, d a * game2 a true ≤ ∑' a, d a * (game1 a true + ENNReal.ofReal ε) := - ENNReal.tsum_le_tsum fun a => mul_le_mul_of_nonneg_left (h2 a) zero_le + tsum_le_tsum fun a => mul_le_mul_of_nonneg_left (h2 a) zero_le _ = (∑' a, d a * game1 a true) + ENNReal.ofReal ε := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, d.tsum_coe, one_mul] + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, d.tsum_coe, one_mul] have hadv := advantage_le_of_apply_le ENNReal.ofReal_ne_top hsum1 hsum2 rwa [ENNReal.toReal_ofReal hε0] at hadv @@ -324,8 +324,8 @@ theorem advantage_bind_uniformOfFintype_of_ne_le {α : Type*} [Fintype α] [None have hle₁ : ((PMF.uniformOfFintype α).bind g) true ≤ p true + (Fintype.card α : ℝ≥0∞)⁻¹ := by rw [← PMF.bind_const (PMF.uniformOfFintype α) p, ← hsingle, PMF.bind_apply, PMF.bind_apply, - PMF.bind_apply, ← ENNReal.tsum_add] - refine ENNReal.tsum_le_tsum fun a => ?_ + PMF.bind_apply, ← tsum_add] + refine tsum_le_tsum fun a => ?_ rw [← mul_add] refine mul_le_mul_of_nonneg_left ?_ zero_le by_cases ha : a = a₀ @@ -335,8 +335,8 @@ theorem advantage_bind_uniformOfFintype_of_ne_le {α : Type*} [Fintype α] [None have hle₂ : p true ≤ ((PMF.uniformOfFintype α).bind g) true + (Fintype.card α : ℝ≥0∞)⁻¹ := by nth_rw 1 [← PMF.bind_const (PMF.uniformOfFintype α) p] - rw [← hsingle, PMF.bind_apply, PMF.bind_apply, PMF.bind_apply, ← ENNReal.tsum_add] - refine ENNReal.tsum_le_tsum fun a => ?_ + rw [← hsingle, PMF.bind_apply, PMF.bind_apply, PMF.bind_apply, ← tsum_add] + refine tsum_le_tsum fun a => ?_ rw [← mul_add] refine mul_le_mul_of_nonneg_left ?_ zero_le by_cases ha : a = a₀ @@ -363,8 +363,8 @@ theorem bind_apply_le_add_bind_apply {β : Type*} (μ : PMF β) (μ.bind game2) b ≤ (μ.bind game1) b + (μ.bind err) b := by have h1 (f g : β → Game) (hle : ∀ x, f x b ≤ g x b + err x b) : (μ.bind f) b ≤ (μ.bind g) b + (μ.bind err) b := by - simp only [PMF.bind_apply, ← ENNReal.tsum_add, ← mul_add] - exact ENNReal.tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (hle x) zero_le + simp only [PMF.bind_apply, ← tsum_add, ← mul_add] + exact tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (hle x) zero_le exact ⟨h1 game1 game2 fun x => (h x).1, h1 game2 game1 fun x => (h x).2⟩ /-- Averaging pointwise acceptance-probability bounds `game1 x true ≤ game2 x true + err x true` diff --git a/Complexity/Crypto/Game/UntilBad.lean b/Complexity/Crypto/Game/UntilBad.lean index 52f3c2892..f80d1e46d 100644 --- a/Complexity/Crypto/Game/UntilBad.lean +++ b/Complexity/Crypto/Game/UntilBad.lean @@ -164,9 +164,9 @@ theorem runStatelessOracle_bind_le {T α : Type} (μ : PMF T) (∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * g x) + (Q : ℝ≥0∞) * δ := by calc ∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * f x ≤ ∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * (g x + (Q : ℝ≥0∞) * δ) := - ENNReal.tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (hle x) zero_le + tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (hle x) zero_le _ = (∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * g x) + (Q : ℝ≥0∞) * δ := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] exact ⟨hsum _ _ (fun x => (ih x).1), hsum _ _ (fun x => (ih x).2)⟩ · simp only [Sum.elim_inr] have hinr₁ : @@ -184,13 +184,13 @@ theorem runStatelessOracle_bind_le {T α : Type} (μ : PMF T) simp only [PMF.bind_apply] calc ∑' τ, μ τ * f τ b ≤ ∑' τ, (μ τ * g τ b + μ τ * if isBad τ req.2 then 1 else 0) := by - refine ENNReal.tsum_le_tsum fun τ => ?_ + refine tsum_le_tsum fun τ => ?_ by_cases hb : isBad τ req.2 = true · simp only [hb, ↓reduceIte, mul_one] exact le_add_of_le_right (mul_le_of_le_one_right zero_le (PMF.coe_le_one _ _)) · simp only [Bool.not_eq_true] at hb rw [hfg τ hb]; simp [hb] - _ = (∑' τ, μ τ * g τ b) + ∑' τ, μ τ * if isBad τ req.2 then 1 else 0 := ENNReal.tsum_add + _ = (∑' τ, μ τ * g τ b) + ∑' τ, μ τ * if isBad τ req.2 then 1 else 0 := tsum_add _ ≤ (∑' τ, μ τ * g τ b) + δ := add_le_add le_rfl (hbad req.2) have hstep1 := hstep (fun τ => runStatelessOracle (o₁ τ) (k (o₁ τ req.2)) (next τ)) @@ -372,20 +372,20 @@ theorem runStatelessOracle_le_runFinderOracle {α : Type} ≤ ∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * (runStatelessOracle o₂ (k x) next b + runFinderOracle o₂ isBad extract (k x) none isGood true) := - ENNReal.tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (ih x).1 zero_le + tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (ih x).1 zero_le _ = (∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * runStatelessOracle o₂ (k x) next b) + ∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * runFinderOracle o₂ isBad extract (k x) none isGood true := by - simp only [mul_add, ENNReal.tsum_add] + simp only [mul_add, tsum_add] · calc ∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * runStatelessOracle o₂ (k x) next b ≤ ∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * (runStatelessOracle o₁ (k x) next b + runFinderOracle o₂ isBad extract (k x) none isGood true) := - ENNReal.tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (ih x).2 zero_le + tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (ih x).2 zero_le _ = (∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * runStatelessOracle o₁ (k x) next b) + ∑' x, PMF.uniformOfFintype (Fin (m + 1)) x * runFinderOracle o₂ isBad extract (k x) none isGood true := by - simp only [mul_add, ENNReal.tsum_add] + simp only [mul_add, tsum_add] · rw [runStatelessOracle_query_inr, runStatelessOracle_query_inr, runFinderOracle_query_inr] by_cases hb : isBad req.2 = true · simp only [hb, ↓reduceIte] diff --git a/Complexity/Crypto/Primitives/PRG/NextBit.lean b/Complexity/Crypto/Primitives/PRG/NextBit.lean index 886b68555..76fe10070 100644 --- a/Complexity/Crypto/Primitives/PRG/NextBit.lean +++ b/Complexity/Crypto/Primitives/PRG/NextBit.lean @@ -121,9 +121,9 @@ private theorem bind_apply_add_of_forall {α β : Type*} (μ : PMF α) {f g h : {c : ℝ≥0∞} (hfg : ∀ x, f x b + g x b = h x b + c) : μ.bind f b + μ.bind g b = μ.bind h b + c := by simp only [PMF.bind_apply] - rw [← ENNReal.tsum_add] + rw [← tsum_add] simp_rw [← mul_add, hfg, mul_add] - rw [ENNReal.tsum_add, ENNReal.tsum_mul_right, μ.tsum_coe, one_mul] + rw [tsum_add, ENNReal.tsum_mul_right, μ.tsum_coe, one_mul] /-- **The distinguisher/predictor lemma** [Boneh and Shoup, Lemma 3.5][BonehShoup2023]. Draw `x` from `μ`. The guess `guessOfDistinguisher (d x)` equals `target x` with probability `1 / 2`, plus diff --git a/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean b/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean index b88c043a5..ca41828a6 100644 --- a/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean +++ b/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean @@ -1955,7 +1955,7 @@ private theorem idealGame_apply_le_realGame_add_of_keyDist (keyDist : PMF (G × calc (∑' res : Bool × (Cache G × Cache G), M_ideal res * keyDist.toOuterMeasure {k | isBadEvenMansourKey res.2.1 res.2.2 k = true}) ≤ ∑' res : Bool × (Cache G × Cache G), M_ideal res * ε := by - refine ENNReal.tsum_le_tsum fun res => ?_ + refine tsum_le_tsum fun res => ?_ by_cases hmem : res ∈ M_ideal.support · refine mul_le_mul_of_nonneg_left (hbad_le res.2.1 res.2.2 ?_ ?_) zero_le · simpa using length_fst_idealLazyHandler_le hcall.1 hmem @@ -1968,14 +1968,14 @@ private theorem idealGame_apply_le_realGame_add_of_keyDist (keyDist : PMF (G × ≤ ∑' k : G × G, keyDist k * ((((OracleComp.interpret (realLazyHandler k) program).run []).map Prod.fst) b + M_ideal.toOuterMeasure {res | isBadEvenMansourKey res.2.1 res.2.2 k = true}) := - ENNReal.tsum_le_tsum fun k => mul_le_mul_of_nonneg_left (hpoint k) zero_le + tsum_le_tsum fun k => mul_le_mul_of_nonneg_left (hpoint k) zero_le _ = (∑' k : G × G, keyDist k * (((OracleComp.interpret (realLazyHandler k) program).run []).map Prod.fst) b) + (∑' k : G × G, keyDist k * M_ideal.toOuterMeasure {res | isBadEvenMansourKey res.2.1 res.2.2 k = true}) := by - simp_rw [mul_add, ENNReal.tsum_add] + simp_rw [mul_add, tsum_add] _ ≤ _ := add_le_add le_rfl hsum_bad private theorem advantage_le_of_forall_bool_le {g₁ g₂ : Game} {ε : ℝ≥0∞} (hε : ε ≠ ⊤) diff --git a/Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean b/Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean index ac6f10219..a46a9a06e 100644 --- a/Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean +++ b/Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean @@ -1013,7 +1013,7 @@ private theorem tsum_seed_toOuterMeasure_hasCollision_le {seed₁ : PMF K₁} {h ∑' x, idealRun x * ∑' k₁, ({k₁ : K₁ | hasUCollision (h₁ k₁) x.2 = true}.indicator seed₁ k₁) := by simp only [← ENNReal.tsum_mul_left] - rw [ENNReal.tsum_comm] + rw [tsum_comm] refine tsum_congr fun x => tsum_congr fun k₁ => ?_ by_cases hx : hasUCollision (h₁ k₁) x.2 = true · rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, mul_comm] @@ -1022,7 +1022,7 @@ private theorem tsum_seed_toOuterMeasure_hasCollision_le {seed₁ : PMF K₁} {h calc ∑' x, idealRun x * ∑' k₁, ({k₁ : K₁ | hasUCollision (h₁ k₁) x.2 = true}.indicator seed₁ k₁) ≤ ∑' x, idealRun x * (Q.choose 2 * ε) := by - refine ENNReal.tsum_le_tsum fun x => ?_ + refine tsum_le_tsum fun x => ?_ by_cases hmem : x ∈ idealRun.support · refine mul_le_mul_of_nonneg_left ?_ zero_le rw [← PMF.toOuterMeasure_apply] @@ -1045,10 +1045,10 @@ private theorem tsum_seed_toOuterMeasure_hasCollision_le {seed₁ : PMF K₁} {h ≤ ∑' k₁, seed₁ k₁ * (idealRun.toOuterMeasure {x | hasUCollision (h₁ k₁) x.2 = true} + idealRun.toOuterMeasure {x | hasVCollision x.2 = true}) := - ENNReal.tsum_le_tsum fun k₁ => mul_le_mul_of_nonneg_left (hsplit k₁) zero_le + tsum_le_tsum fun k₁ => mul_le_mul_of_nonneg_left (hsplit k₁) zero_le _ = (∑' k₁, seed₁ k₁ * idealRun.toOuterMeasure {x | hasUCollision (h₁ k₁) x.2 = true}) + (∑' k₁, seed₁ k₁ * idealRun.toOuterMeasure {x | hasVCollision x.2 = true}) := by - simp only [mul_add, ENNReal.tsum_add] + simp only [mul_add, tsum_add] _ ≤ Q.choose 2 * ε + Q.choose 2 * (Fintype.card G : ℝ≥0∞)⁻¹ := add_le_add hu hv /-- For every fixed `f₁`, the acceptance probability of `feistel3FixedGame f₁ program` and @@ -1092,13 +1092,13 @@ theorem feistel3HashIdealGame_apply_le {seed₁ : PMF K₁} {h₁ : K₁ → G ≤ ∑' k₁, seed₁ k₁ * (randomFunctionGame program b + ((OracleComp.interpret (memoize (fun _ : G × G => PMF.uniformOfFintype (G × G))) program).run []).toOuterMeasure {x | hasCollision (h₁ k₁) x.2 = true}) := - ENNReal.tsum_le_tsum fun k₁ => + tsum_le_tsum fun k₁ => mul_le_mul_of_nonneg_left (feistel3FixedGame_apply_le (h₁ k₁) program b) zero_le _ = randomFunctionGame program b + ∑' k₁, seed₁ k₁ * ((OracleComp.interpret (memoize (fun _ : G × G => PMF.uniformOfFintype (G × G))) program).run []).toOuterMeasure {x | hasCollision (h₁ k₁) x.2 = true} := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, seed₁.tsum_coe, one_mul] + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, seed₁.tsum_coe, one_mul] _ ≤ randomFunctionGame program b + (Q.choose 2 * ε + Q.choose 2 * (Fintype.card G : ℝ≥0∞)⁻¹) := add_le_add le_rfl (tsum_seed_toOuterMeasure_hasCollision_le hh₁ hQ) @@ -1120,14 +1120,14 @@ theorem randomFunctionGame_apply_le_feistel3HashIdealGame {seed₁ : PMF K₁} { ≤ ∑' k₁, seed₁ k₁ * (feistel3FixedGame (h₁ k₁) program b + ((OracleComp.interpret (memoize (fun _ : G × G => PMF.uniformOfFintype (G × G))) program).run []).toOuterMeasure {x | hasCollision (h₁ k₁) x.2 = true}) := - ENNReal.tsum_le_tsum fun k₁ => + tsum_le_tsum fun k₁ => mul_le_mul_of_nonneg_left (randomFunctionGame_apply_le_feistel3FixedGame (h₁ k₁) program b) zero_le _ = (∑' k₁, seed₁ k₁ * feistel3FixedGame (h₁ k₁) program b) + ∑' k₁, seed₁ k₁ * ((OracleComp.interpret (memoize (fun _ : G × G => PMF.uniformOfFintype (G × G))) program).run []).toOuterMeasure {x | hasCollision (h₁ k₁) x.2 = true} := by - simp only [mul_add, ENNReal.tsum_add] + simp only [mul_add, tsum_add] _ ≤ (∑' k₁, seed₁ k₁ * feistel3FixedGame (h₁ k₁) program b) + (Q.choose 2 * ε + Q.choose 2 * (Fintype.card G : ℝ≥0∞)⁻¹) := add_le_add le_rfl (tsum_seed_toOuterMeasure_hasCollision_le hh₁ hQ) @@ -1619,7 +1619,7 @@ theorem le_idealStrongGame_feistel3CCAAttack_false {l₀ l₁ l₂ r₀ : G} _ ≤ ∑' π : Equiv.Perm (G × G), PMF.uniformOfFintype (Equiv.Perm (G × G)) π * OracleComp.interpret (feistelStrongOracle π) (feistel3CCAAttack l₀ l₁ r₀) false := - ENNReal.le_tsum (f := fun π : Equiv.Perm (G × G) => + le_tsum (f := fun π : Equiv.Perm (G × G) => PMF.uniformOfFintype (Equiv.Perm (G × G)) π * OracleComp.interpret (feistelStrongOracle π) (feistel3CCAAttack l₀ l₁ r₀) false) π₀ @@ -1875,9 +1875,9 @@ theorem idealStrongGame_feistel3CCAAttack_true_le {l₀ l₁ : G} (r₀ : G) (h0 (fun x => decide (-vw₀.1 + x.1.2 = -vw₁.1 + r₀))) true ≤ ∑' vw₁, ((PMF.uniformOfFintype (G × G)) vw₁ * (Fintype.card G : ℝ≥0∞)⁻¹ + ({q₃} : Set (G × G)).indicator (PMF.uniformOfFintype (G × G)) vw₁) := - ENNReal.tsum_le_tsum hvw₁ + tsum_le_tsum hvw₁ _ = (Fintype.card G : ℝ≥0∞)⁻¹ + (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := by - rw [ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, + rw [tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, ← PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply_singleton, PMF.uniformOfFintype_apply] calc ∑' vw₀, (PMF.uniformOfFintype (G × G)) vw₀ * @@ -1888,7 +1888,7 @@ theorem idealStrongGame_feistel3CCAAttack_true_le {l₀ l₁ : G} (r₀ : G) (h0 (fun x => decide (-vw₀.1 + x.1.2 = -vw₁.1 + r₀))) true ≤ ∑' vw₀, (PMF.uniformOfFintype (G × G)) vw₀ * ((Fintype.card G : ℝ≥0∞)⁻¹ + (Fintype.card (G × G) : ℝ≥0∞)⁻¹) := - ENNReal.tsum_le_tsum fun vw₀ => mul_le_mul_of_nonneg_left (hvw₀ vw₀) zero_le + tsum_le_tsum fun vw₀ => mul_le_mul_of_nonneg_left (hvw₀ vw₀) zero_le _ = (Fintype.card G : ℝ≥0∞)⁻¹ + (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := by rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] have hchoose : ((Nat.choose 3 2 : ℕ) : ℝ≥0∞) = 3 := rfl @@ -3043,7 +3043,7 @@ private theorem tsum_toOuterMeasure_of_pointwise_le {α β : Type} (μ : PMF α) (∑' a, μ a * ∑' y, {y | P a y}.indicator d y) = ∑' y, d y * ∑' a, {a | P a y}.indicator μ a := by simp only [← ENNReal.tsum_mul_left] - rw [ENNReal.tsum_comm] + rw [tsum_comm] refine tsum_congr fun y => tsum_congr fun a => ?_ by_cases h : P a y · rw [Set.indicator_of_mem h, Set.indicator_of_mem h, mul_comm] @@ -3051,7 +3051,7 @@ private theorem tsum_toOuterMeasure_of_pointwise_le {α β : Type} (μ : PMF α) rw [hcomm] calc ∑' y, d y * ∑' a, {a | P a y}.indicator μ a ≤ ∑' y, d y * M := - ENNReal.tsum_le_tsum fun y => mul_le_mul_of_nonneg_left (by + tsum_le_tsum fun y => mul_le_mul_of_nonneg_left (by rw [← PMF.toOuterMeasure_apply] exact hM y) zero_le _ = M := by rw [ENNReal.tsum_mul_right, d.tsum_coe, one_mul] @@ -3155,14 +3155,14 @@ private theorem tsum_uniform_toOuterMeasure_hasCollision4_le d.toOuterMeasure {x | IsGoodCache4 Q x.2 ∧ hasVCollision4 f₄ x.2 = true} + (Q.choose 2 : ℝ≥0∞) * (Fintype.card (G × G) : ℝ≥0∞)⁻¹) := - ENNReal.tsum_le_tsum fun f₄ => + tsum_le_tsum fun f₄ => mul_le_mul_of_nonneg_left (toOuterMeasure_hasCollision4_le f₁ f₄ hQ) zero_le _ = d.toOuterMeasure {x | IsGoodCache4 Q x.2 ∧ hasUCollision f₁ x.2 = true} + (∑' f₄, unif f₄ * d.toOuterMeasure {x | IsGoodCache4 Q x.2 ∧ hasVCollision4 f₄ x.2 = true}) + (Q.choose 2 : ℝ≥0∞) * (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, unif.tsum_coe, one_mul] + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, unif.tsum_coe, one_mul] _ ≤ _ := add_le_add (add_le_add le_rfl (tsum_uniform_toOuterMeasure_hasVCollision4_le d Q)) le_rfl calc ∑' f₁, unif f₁ * ∑' f₄, unif f₄ * d.toOuterMeasure {x | hasCollision4 f₁ f₄ x.2 = true} @@ -3171,12 +3171,12 @@ private theorem tsum_uniform_toOuterMeasure_hasCollision4_le {x | IsGoodCache4 Q x.2 ∧ hasUCollision f₁ x.2 = true} + Q.choose 2 * (Fintype.card G : ℝ≥0∞)⁻¹ + (Q.choose 2 : ℝ≥0∞) * (Fintype.card (G × G) : ℝ≥0∞)⁻¹) := - ENNReal.tsum_le_tsum fun f₁ => mul_le_mul_of_nonneg_left (hinner f₁) zero_le + tsum_le_tsum fun f₁ => mul_le_mul_of_nonneg_left (hinner f₁) zero_le _ = (∑' f₁, unif f₁ * d.toOuterMeasure {x | IsGoodCache4 Q x.2 ∧ hasUCollision f₁ x.2 = true}) + Q.choose 2 * (Fintype.card G : ℝ≥0∞)⁻¹ + (Q.choose 2 : ℝ≥0∞) * (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, unif.tsum_coe, one_mul] + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, unif.tsum_coe, one_mul] _ ≤ Q.choose 2 * (Fintype.card G : ℝ≥0∞)⁻¹ + Q.choose 2 * (Fintype.card G : ℝ≥0∞)⁻¹ + (Q.choose 2 : ℝ≥0∞) * (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := @@ -3253,13 +3253,13 @@ theorem feistel4StrongRandomRoundsGame_apply_le (forgetVal + ((OracleComp.interpret RandomPermutation.forgetfulAnswer prog).run []).toOuterMeasure {x | hasCollision4 f₁ f₄ x.2 = true}) := - ENNReal.tsum_le_tsum fun f₁ => mul_le_mul_of_nonneg_left - (ENNReal.tsum_le_tsum fun f₄ => mul_le_mul_of_nonneg_left + tsum_le_tsum fun f₁ => mul_le_mul_of_nonneg_left + (tsum_le_tsum fun f₄ => mul_le_mul_of_nonneg_left (feistel4StrongFixedGame_apply_le f₁ f₄ program b) zero_le) zero_le _ = forgetVal + ∑' f₁, unif f₁ * ∑' f₄, unif f₄ * ((OracleComp.interpret RandomPermutation.forgetfulAnswer prog).run []).toOuterMeasure {x | hasCollision4 f₁ f₄ x.2 = true} := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, unif.tsum_coe, one_mul] + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, unif.tsum_coe, one_mul] _ ≤ _ := add_le_add le_rfl (tsum_uniform_toOuterMeasure_hasCollision4_le hQ') have hperm := RandomPermutation.forgetfulAnswer_bind_apply_le_uniformPerm hQ' PMF.pure b simp only [Probability.PMF.monad_bind_eq_bind, PMF.bind_pure] at hperm @@ -3303,14 +3303,14 @@ theorem idealStrongGame_apply_le_feistel4StrongRandomRoundsGame (feistel4StrongFixedGame f₁ f₄ program b + ((OracleComp.interpret RandomPermutation.forgetfulAnswer prog).run []).toOuterMeasure {x | hasCollision4 f₁ f₄ x.2 = true}) := - ENNReal.tsum_le_tsum fun f₁ => mul_le_mul_of_nonneg_left - (ENNReal.tsum_le_tsum fun f₄ => mul_le_mul_of_nonneg_left + tsum_le_tsum fun f₁ => mul_le_mul_of_nonneg_left + (tsum_le_tsum fun f₄ => mul_le_mul_of_nonneg_left (forgetfulAnswer_apply_le_feistel4StrongFixedGame f₁ f₄ program b) zero_le) zero_le _ = (∑' f₁, unif f₁ * ∑' f₄, unif f₄ * feistel4StrongFixedGame f₁ f₄ program b) + ∑' f₁, unif f₁ * ∑' f₄, unif f₄ * ((OracleComp.interpret RandomPermutation.forgetfulAnswer prog).run []).toOuterMeasure {x | hasCollision4 f₁ f₄ x.2 = true} := by - simp only [mul_add, ENNReal.tsum_add] + simp only [mul_add, tsum_add] _ ≤ _ := add_le_add le_rfl (tsum_uniform_toOuterMeasure_hasCollision4_le hQ') have hperm := RandomPermutation.uniformPerm_bind_apply_le_forgetful hQ' PMF.pure b simp only [Probability.PMF.monad_bind_eq_bind, PMF.bind_pure] at hperm diff --git a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean index dd32115b4..4b4f2bb30 100644 --- a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean +++ b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean @@ -3802,10 +3802,10 @@ theorem randomNonceSimHandler_not_nodup_le {α : Type} [Fintype N] [Nonempty N] PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true ≤ ∑' x, PMF.uniformOfFintype N x * ((PMF.pure (decide (x ∈ tr.map (fun e => e.1.2)))) true + B) := - ENNReal.tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (hx_bound x) zero_le + tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (hx_bound x) zero_le _ = ((PMF.uniformOfFintype N).bind fun x => PMF.pure (decide (x ∈ tr.map (fun e => e.1.2)))) true + B := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, (PMF.uniformOfFintype N).tsum_coe, one_mul, PMF.bind_apply] _ ≤ (tr.length : ℝ≥0∞) / Fintype.card N + B := add_le_add hmem_le le_rfl _ = ((∑ i ∈ Finset.range (Q + 1), (tr.length + i) : ℕ) : ℝ≥0∞) / Fintype.card N := by @@ -4029,11 +4029,11 @@ theorem randomNonceStrongGame_le_sum_add_max {seed : PMF K} {hash : K → M → ≤ ∑' res, simPMF res * ((PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true + max ε (Fintype.card Y : ℝ≥0∞)⁻¹) := - ENNReal.tsum_le_tsum fun res => mul_le_mul_of_nonneg_left (hpoint res) zero_le + tsum_le_tsum fun res => mul_le_mul_of_nonneg_left (hpoint res) zero_le _ = (simPMF.bind fun res => PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true + max ε (Fintype.card Y : ℝ≥0∞)⁻¹ := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, simPMF.tsum_coe, one_mul, + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, simPMF.tsum_coe, one_mul, PMF.bind_apply] _ ≤ ((∑ i ∈ Finset.range Q, i : ℕ) : ℝ≥0∞) / Fintype.card N + max ε (Fintype.card Y : ℝ≥0∞)⁻¹ := by @@ -4485,10 +4485,10 @@ theorem probOracleComp_randomNonceSimHandler_not_nodup_le {α : Type} PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true ≤ ∑' x, PMF.uniformOfFintype N x * ((PMF.pure (decide (x ∈ tr.map (fun e => e.1.2)))) true + B) := - ENNReal.tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (hx_bound x) zero_le + tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (hx_bound x) zero_le _ = ((PMF.uniformOfFintype N).bind fun x => PMF.pure (decide (x ∈ tr.map (fun e => e.1.2)))) true + B := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, (PMF.uniformOfFintype N).tsum_coe, one_mul, PMF.bind_apply] _ ≤ (tr.length : ℝ≥0∞) / Fintype.card N + B := add_le_add hmem_le le_rfl _ = ((∑ i ∈ Finset.range (Q + 1), (tr.length + i) : ℕ) : ℝ≥0∞) / Fintype.card N := by @@ -4610,11 +4610,11 @@ theorem seed_uniform_probOracleComp_checkRandomNonceSUF_le {α : Type} ≤ ∑' res, simPMF res * ((PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true + max ε (Fintype.card Y : ℝ≥0∞)⁻¹) := - ENNReal.tsum_le_tsum fun res => mul_le_mul_of_nonneg_left (hpoint res) zero_le + tsum_le_tsum fun res => mul_le_mul_of_nonneg_left (hpoint res) zero_le _ = (simPMF.bind fun res => PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true + max ε (Fintype.card Y : ℝ≥0∞)⁻¹ := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, simPMF.tsum_coe, one_mul, + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, simPMF.tsum_coe, one_mul, PMF.bind_apply] _ ≤ ((∑ i ∈ Finset.range Q, i : ℕ) : ℝ≥0∞) / Fintype.card N + max ε (Fintype.card Y : ℝ≥0∞)⁻¹ := by diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean index 2075b932a..39a83a0cb 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/FiatShamir.lean @@ -391,7 +391,7 @@ private theorem toOuterMeasure_flag_le (P : SigmaProtocol X Y T C Z) (key : X × {x | x.2.2 = true} ≤ ∑' ts, (P.commit key.1 key.2) ts * {ts : T × P.State | (st.1.1.lookup (m, ts.1)).isSome}.indicator 1 ts := by - refine ENNReal.tsum_le_tsum fun ts => mul_le_mul_of_nonneg_left ?_ zero_le + refine tsum_le_tsum fun ts => mul_le_mul_of_nonneg_left ?_ zero_le by_cases hts : (st.1.1.lookup (m, ts.1)).isSome · rw [Set.indicator_of_mem (show ts ∈ {ts : T × P.State | (st.1.1.lookup (m, ts.1)).isSome} from hts), Pi.one_apply] @@ -828,12 +828,12 @@ private theorem bind_apply_le_add {α β : Type} {μ : PMF α} {f g : α → PMF (μ.bind f) b ≤ (μ.bind g) b + K := by simp only [PMF.bind_apply] calc ∑' a, μ a * f a b ≤ ∑' a, μ a * (g a b + K) := by - refine ENNReal.tsum_le_tsum fun a => ?_ + refine tsum_le_tsum fun a => ?_ by_cases ha : a ∈ μ.support · exact mul_le_mul_of_nonneg_left (h a ha) zero_le · rw [(PMF.apply_eq_zero_iff _ _).mpr ha, zero_mul, zero_mul] _ = ∑' a, μ a * g a b + K := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] omit [DecidableEq C] in /-- **The game hops** for one key and one choice of the forger's coins: the experiment wins at diff --git a/Complexity/Languages/Probabilistic/BoundedUniform.lean b/Complexity/Languages/Probabilistic/BoundedUniform.lean index 6fa41f00f..a4166310d 100644 --- a/Complexity/Languages/Probabilistic/BoundedUniform.lean +++ b/Complexity/Languages/Probabilistic/BoundedUniform.lean @@ -187,7 +187,7 @@ private theorem retry_some (bound value : ℕ) (next : PMF (Option ℕ)) : simp [hib, hiv] change (∑' i, μ i * (if i < bound then PMF.pure (some i) else next) (some value)) = _ simp_rw [hterm] - rw [ENNReal.tsum_add] + rw [tsum_add] simp only [tsum_ite_eq] rw [show μ bound = (intervalFailure bound : ℝ≥0∞) from eval_sampleBoundedIndex_sentinel bound] by_cases hv : value < bound @@ -342,7 +342,7 @@ private theorem uniformFin_nat_apply (bound value : ℕ) [NeZero bound] : · intro i hi have : value ≠ i.val := fun h => hi (Fin.ext h.symm) simp [this] - · rw [ENNReal.tsum_eq_zero.mpr] + · rw [tsum_eq_zero_iff.mpr] · simp [hv] · intro i have : value ≠ i.val := by omega @@ -364,7 +364,7 @@ theorem eval_sampleUniformInterval_some_eq (bound attempts value : ℕ) [NeZero private theorem tsum_option_eq {α : Type} (f : Option α → ℝ≥0∞) : ∑' x, f x = f none + ∑' x, f (some x) := by rw [← (Equiv.optionEquivSumPUnit.{0, 0} α).symm.tsum_eq f] - rw [ENNReal.summable.tsum_sum ENNReal.summable] + rw [CompleteLattice.summable.tsum_sum CompleteLattice.summable] simp [add_comm] private theorem optional_map_density {α β : Type} (μ : PMF (Option α)) (ν : PMF α) diff --git a/Complexity/Languages/Probabilistic/Expect.lean b/Complexity/Languages/Probabilistic/Expect.lean index 3785b103e..6b22d82f8 100644 --- a/Complexity/Languages/Probabilistic/Expect.lean +++ b/Complexity/Languages/Probabilistic/Expect.lean @@ -70,7 +70,7 @@ theorem expect_zero (m : ProbComp α) : expect m (fun _ => 0) = 0 := theorem expect_add (m : ProbComp α) (f g : α → ℝ≥0∞) : expect m (fun a => f a + g a) = expect m f + expect m g := by - simp only [expect, mul_add, ENNReal.tsum_add] + simp only [expect, mul_add, tsum_add] theorem expect_mul_left (m : ProbComp α) (c : ℝ≥0∞) (f : α → ℝ≥0∞) : expect m (fun a => c * f a) = c * expect m f := by @@ -86,7 +86,7 @@ theorem expect_mul_right (m : ProbComp α) (f : α → ℝ≥0∞) (c : ℝ≥0 theorem expect_bind (m : ProbComp α) (k : α → ProbComp β) (f : β → ℝ≥0∞) : expect (m >>= k) f = expect m (fun a => expect (k a) f) := by simp only [expect, eval_bind, PMF.bind_apply, ← ENNReal.tsum_mul_right] - rw [ENNReal.tsum_comm] + rw [tsum_comm] congr 1 funext a simp only [mul_assoc, ENNReal.tsum_mul_left] @@ -107,7 +107,7 @@ theorem expect_congr_on_support {m : ProbComp α} {f g : α → ℝ≥0∞} theorem expect_mono_on_support {m : ProbComp α} {f g : α → ℝ≥0∞} (h : ∀ a ∈ m.support, f a ≤ g a) : expect m f ≤ expect m g := by - refine ENNReal.tsum_le_tsum fun a => ?_ + refine tsum_le_tsum fun a => ?_ by_cases ha : a ∈ m.support · exact mul_le_mul_right (h a ha) _ · have hzero : (eval m) a = 0 := (PMF.apply_eq_zero_iff (eval m) a).mpr (by @@ -129,7 +129,7 @@ theorem expect_eq_top_of_mem_support {m : ProbComp α} {f : α → ℝ≥0∞} { refine top_unique ?_ calc (⊤ : ℝ≥0∞) = (eval m) a * f a := by rw [hf, ENNReal.mul_top hpos] - _ ≤ expect m f := ENNReal.le_tsum (f := fun b => (eval m) b * f b) a + _ ≤ expect m f := le_tsum (f := fun b => (eval m) b * f b) a theorem expect_unifFin (n : ℕ) (f : Fin (n + 1) → ℝ≥0∞) : expect (unifFin n) f = (∑ k : Fin (n + 1), f k) / (n + 1 : ℝ≥0∞) := by diff --git a/Complexity/Languages/Probabilistic/Oracle/Interaction.lean b/Complexity/Languages/Probabilistic/Oracle/Interaction.lean index 6aa1215f3..d822a739c 100644 --- a/Complexity/Languages/Probabilistic/Oracle/Interaction.lean +++ b/Complexity/Languages/Probabilistic/Oracle/Interaction.lean @@ -168,7 +168,7 @@ theorem acceptProbWith_bind_ite_le (program : ProbOracleComp spec Bool) acceptProbWith oracle program s := by conv_rhs => rw [← bind_pure program, acceptProbWith_bind] rw [acceptProbWith_bind] - refine ENNReal.tsum_le_tsum fun x => mul_le_mul_right ?_ _ + refine tsum_le_tsum fun x => mul_le_mul_right ?_ _ cases x.1 · simp only [Bool.false_eq_true, ↓reduceIte, le_refl] · simp only [↓reduceIte, acceptProbWith_pure] diff --git a/Complexity/Languages/Probabilistic/RandomPermutation.lean b/Complexity/Languages/Probabilistic/RandomPermutation.lean index f8b175e6d..153ac0a84 100644 --- a/Complexity/Languages/Probabilistic/RandomPermutation.lean +++ b/Complexity/Languages/Probabilistic/RandomPermutation.lean @@ -1175,9 +1175,9 @@ theorem toOuterMeasure_bad_choose_two_le {ι σ β : Type} {spec : ι → Type} calc ∑' y, (handler q s) y * ((OracleComp.interpret handler (cont y.1)).run y.2).toOuterMeasure {x | bad x.2} ≤ ∑' y, (handler q s) y * ({x : spec q × σ | bad x.2}.indicator 1 y + K) := - ENNReal.tsum_le_tsum hterm + tsum_le_tsum hterm _ = (handler q s).toOuterMeasure {x | bad x.2} + K := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, PMF.toOuterMeasure_apply] congr 1 refine tsum_congr fun y => ?_ @@ -1413,8 +1413,8 @@ theorem toOuterMeasure_forgetfulAnswer_le_pairwise_and_length_le_add {β : Type} {x | (x.2.Pairwise (fun a b => a.1 ≠ b.1) ∧ x.2.Pairwise (fun a b => a.2 ≠ b.2) ∧ x.2.length ≤ Q) ∧ P x.2}) + q.toOuterMeasure {x | x.2.2 = true} - simp only [PMF.toOuterMeasure_apply, ← ENNReal.tsum_add] - refine ENNReal.tsum_le_tsum fun ⟨a, c, b⟩ => ?_ + simp only [PMF.toOuterMeasure_apply, ← tsum_add] + refine tsum_le_tsum fun ⟨a, c, b⟩ => ?_ by_cases hmem : (a, (c, b)) ∈ q.support · by_cases hP : P c · cases b with diff --git a/Complexity/Languages/Probabilistic/UntilBad.lean b/Complexity/Languages/Probabilistic/UntilBad.lean index 7bcd7e202..ac26422b6 100644 --- a/Complexity/Languages/Probabilistic/UntilBad.lean +++ b/Complexity/Languages/Probabilistic/UntilBad.lean @@ -129,8 +129,8 @@ theorem bind_apply_le (h : IdenticalUntilBad first second bad) (program : Oracle ((interpret first program).run s).toOuterMeasure {x | bad x.2} := by classical simp only [PMF.bind_apply, PMF.toOuterMeasure_apply] - rw [← ENNReal.tsum_add] - refine ENNReal.tsum_le_tsum fun x => ?_ + rw [← tsum_add] + refine tsum_le_tsum fun x => ?_ by_cases hx : bad x.2 · have hbad : x ∈ {x : α × σ | bad x.2} := hx rw [Set.indicator_of_mem hbad] @@ -153,7 +153,7 @@ private theorem toOuterMeasure_bad_add_good (p : PMF (α × σ)) : p.toOuterMeasure {x | bad x.2} + p.toOuterMeasure {x | ¬bad x.2} = 1 := by classical simp only [PMF.toOuterMeasure_apply] - rw [← ENNReal.tsum_add, ← p.tsum_coe] + rw [← tsum_add, ← p.tsum_coe] refine tsum_congr fun x => ?_ by_cases hx : bad x.2 · rw [Set.indicator_of_mem (show x ∈ {x : α × σ | bad x.2} from hx), @@ -244,9 +244,9 @@ theorem toOuterMeasure_bad_le {handler : (q : ι) → StateT σ PMF (spec q)} {b calc ∑' y, (handler q s) y * ((interpret handler (cont y.1)).run y.2).toOuterMeasure {x | bad x.2} ≤ ∑' y, (handler q s) y * ({x : spec q × σ | bad x.2}.indicator 1 y + K) := - ENNReal.tsum_le_tsum hterm + tsum_le_tsum hterm _ = (handler q s).toOuterMeasure {x | bad x.2} + K := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, + simp only [mul_add, tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, PMF.toOuterMeasure_apply] congr 1 refine tsum_congr fun y => ?_ diff --git a/Complexity/Languages/Probabilistic/Vector.lean b/Complexity/Languages/Probabilistic/Vector.lean index 5e43aaaa5..4f3e7ead7 100644 --- a/Complexity/Languages/Probabilistic/Vector.lean +++ b/Complexity/Languages/Probabilistic/Vector.lean @@ -274,7 +274,7 @@ theorem eval_pi {m : ℕ} {α : Fin m → Type} [∀ i, Finite (α i)] funext i simpa using (congrFun hEq (Fin.succ i)).symm · intro a ha - simp only [mul_eq_zero, ENNReal.tsum_eq_zero] + simp only [mul_eq_zero, tsum_eq_zero_iff] right intro b rw [ite_eq_right] diff --git a/Complexity/Probability/Conditioning.lean b/Complexity/Probability/Conditioning.lean index faca6d699..340e70ef4 100644 --- a/Complexity/Probability/Conditioning.lean +++ b/Complexity/Probability/Conditioning.lean @@ -48,7 +48,7 @@ variable {α β : Type*} theorem map_fst_apply (joint : PMF (α × β)) (a : α) : (joint.map Prod.fst) a = ∑' b, joint (a, b) := by classical - rw [PMF.map_apply, ENNReal.tsum_prod'] + rw [PMF.map_apply, tsum_prod'] rw [tsum_eq_single a] · simp · intro x hx @@ -72,9 +72,9 @@ theorem conditionalSnd_apply (joint : PMF (α × β)) (a : α) conditionalSnd joint a b = joint (a, b) / (joint.map Prod.fst) a := by classical have hpost : a ∈ (joint.bind (fun pair => PMF.pure pair.1)).support := ha - simp only [conditionalSnd, hpost, dite_true, PMF.map_apply, ENNReal.tsum_prod', + simp only [conditionalSnd, hpost, dite_true, PMF.map_apply, tsum_prod', posteriorDist_apply, bind_pair_apply, PMF.pure_apply] - simp [ENNReal.tsum_prod', div_eq_mul_inv] + simp [tsum_prod', div_eq_mul_inv] /-- Multiplying by the marginal recovers the joint mass, also at zero-probability observations. -/ theorem marginal_mul_conditionalSnd (joint : PMF (α × β)) (a : α) (b : β) : diff --git a/Complexity/Probability/CorrelatedSampling.lean b/Complexity/Probability/CorrelatedSampling.lean index 5e9f61775..ae9ebd647 100644 --- a/Complexity/Probability/CorrelatedSampling.lean +++ b/Complexity/Probability/CorrelatedSampling.lean @@ -171,7 +171,7 @@ theorem map_firstIn_weightedOrderAux (w : Ω → ℝ≥0) : rcases o with _ | c · rw [PMF.bind_apply, PMF.map_apply] simp only [reduceCtorEq, ite_false, tsum_zero] - refine ENNReal.tsum_eq_zero.mpr fun a => ?_ + refine tsum_eq_zero_iff.mpr fun a => ?_ split_ifs <;> simp [PMF.map_apply] rw [PMF.bind_apply, tsum_fintype, hrhs] set du := weightedDraw w U hU0 diff --git a/Complexity/Probability/Forking.lean b/Complexity/Probability/Forking.lean index 960ea5e2e..b13827992 100644 --- a/Complexity/Probability/Forking.lean +++ b/Complexity/Probability/Forking.lean @@ -215,7 +215,7 @@ private theorem bind_match_apply {X : Type} (μ : PMF X) (index : X → Option ( | some j => decide (event j x))) true = ∑ j, (μ.bind fun x => PMF.pure (decide (index x = some j ∧ event j x))) true := by simp only [PMF.bind_apply, PMF.pure_apply] - rw [← Summable.tsum_finsetSum fun _ _ => ENNReal.summable] + rw [← Summable.tsum_finsetSum fun _ _ => CompleteLattice.summable] refine tsum_congr fun x => ?_ rw [← Finset.mul_sum] congr 1 diff --git a/Complexity/Probability/IID.lean b/Complexity/Probability/IID.lean index 74388f5b5..0a600cf4a 100644 --- a/Complexity/Probability/IID.lean +++ b/Complexity/Probability/IID.lean @@ -73,7 +73,7 @@ noncomputable def iid (μ : PMF α) : (k : ℕ) → PMF (Fin k → α) intro h exact absurd (by rw [h, Fin.tail_cons]) hw · intro a ha - rw [PMF.map_apply, ENNReal.tsum_eq_zero.mpr, mul_zero] + rw [PMF.map_apply, tsum_eq_zero_iff.mpr, mul_zero] intro w simp only [ite_eq_right_iff] intro h diff --git a/Complexity/Probability/MinEntropy.lean b/Complexity/Probability/MinEntropy.lean index 15120ffd6..29fd28b12 100644 --- a/Complexity/Probability/MinEntropy.lean +++ b/Complexity/Probability/MinEntropy.lean @@ -183,7 +183,7 @@ theorem le_minEntropy_bind (μ : PMF β) (f : β → PMF α) {k : ℝ} apply ENNReal.toReal_le_of_le_ofReal hk calc μ.bind f a = ∑' b, μ b * f b a := PMF.bind_apply μ f a - _ ≤ ∑' b, μ b * ENNReal.ofReal (2 ^ (-k)) := ENNReal.tsum_le_tsum hcomponent + _ ≤ ∑' b, μ b * ENNReal.ofReal (2 ^ (-k)) := tsum_le_tsum hcomponent _ = ENNReal.ofReal (2 ^ (-k)) := by rw [ENNReal.tsum_mul_right, μ.tsum_coe, one_mul] /-! ### Weak random sources -/ diff --git a/Complexity/Probability/Minimax.lean b/Complexity/Probability/Minimax.lean index e34129b86..ba395a192 100644 --- a/Complexity/Probability/Minimax.lean +++ b/Complexity/Probability/Minimax.lean @@ -213,10 +213,10 @@ theorem exists_mem_support_tsum_mul_le (μ : PMF α) (ν : PMF β) (loss : α calc ∑' a, μ a * ∑' b, ν b * loss a b = ∑' b, ν b * ∑' a, μ a * loss a b := by simp only [← ENNReal.tsum_mul_left] - rw [ENNReal.tsum_comm] + rw [tsum_comm] exact tsum_congr fun b => tsum_congr fun a => by ring _ ≤ ∑' b, ν b * ε := by - refine ENNReal.tsum_le_tsum fun b => ?_ + refine tsum_le_tsum fun b => ?_ by_cases hb : b ∈ ν.support · gcongr exact h b hb diff --git a/Complexity/Probability/PMF/Bind.lean b/Complexity/Probability/PMF/Bind.lean index fcdd9502b..c3b9858bc 100644 --- a/Complexity/Probability/PMF/Bind.lean +++ b/Complexity/Probability/PMF/Bind.lean @@ -53,7 +53,7 @@ theorem bind_sigma_apply {β : α → Type*} (p : PMF α) (f : (a : α) → PMF (p.bind (fun a => (f a).map (Sigma.mk a))) ⟨a, b⟩ = p a * f a b := by classical simp only [PMF.bind_apply, PMF.map_apply, ← ENNReal.tsum_mul_left, mul_ite, mul_zero] - rw [← ENNReal.tsum_sigma] + rw [← tsum_sigma] simp /-- A continuation only needs to agree on outcomes the preceding distribution can produce. -/ @@ -76,7 +76,7 @@ theorem le_bind_apply_on_support (μ : PMF α) {f : α → PMF β} {b : β} {c : (h : ∀ a ∈ μ.support, c ≤ f a b) : c ≤ μ.bind f b := by rw [PMF.bind_apply] calc c = ∑' a, μ a * c := by rw [ENNReal.tsum_mul_right, μ.tsum_coe, one_mul] - _ ≤ ∑' a, μ a * f a b := ENNReal.tsum_le_tsum fun a => by + _ ≤ ∑' a, μ a * f a b := tsum_le_tsum fun a => by by_cases ha : a ∈ μ.support · exact mul_le_mul_right (h a ha) _ · simp [(PMF.apply_eq_zero_iff μ a).2 ha] @@ -87,7 +87,7 @@ theorem bind_apply_le_on_support (μ : PMF α) {f : α → PMF β} {b : β} {c : (h : ∀ a ∈ μ.support, f a b ≤ c) : μ.bind f b ≤ c := by rw [PMF.bind_apply] calc ∑' a, μ a * f a b - _ ≤ ∑' a, μ a * c := ENNReal.tsum_le_tsum fun a => by + _ ≤ ∑' a, μ a * c := tsum_le_tsum fun a => by by_cases ha : a ∈ μ.support · exact mul_le_mul_right (h a ha) _ · simp [(PMF.apply_eq_zero_iff μ a).2 ha] @@ -98,7 +98,7 @@ probability in the whole experiment. The sample spaces may be infinite. -/ theorem bind_apply_mono_on_support (μ : PMF α) {f g : α → PMF β} (b : β) (h : ∀ a ∈ μ.support, f a b ≤ g a b) : μ.bind f b ≤ μ.bind g b := by simp only [PMF.bind_apply] - apply ENNReal.tsum_le_tsum + apply tsum_le_tsum intro a by_cases ha : a ∈ μ.support · exact mul_le_mul_right (h a ha) _ @@ -117,7 +117,7 @@ theorem exists_bind_apply_le [Finite α] (μ : PMF α) (f : α → PMF β) (b : /-- An average of values at most `B` is at most `B`. -/ theorem tsum_mul_le_of_forall_le (μ : PMF α) {f : α → ℝ≥0∞} {B : ℝ≥0∞} (h : ∀ a, f a ≤ B) : ∑' a, μ a * f a ≤ B := - calc ∑' a, μ a * f a ≤ ∑' a, μ a * B := ENNReal.tsum_le_tsum fun a => mul_le_mul_right (h a) _ + calc ∑' a, μ a * f a ≤ ∑' a, μ a * B := tsum_le_tsum fun a => mul_le_mul_right (h a) _ _ = B := by rw [ENNReal.tsum_mul_right, μ.tsum_coe, one_mul] /-- Values at most `1` on a finite set `T` and at most `B` elsewhere average to at most @@ -126,9 +126,9 @@ theorem tsum_mul_le_card_mul_add [DecidableEq α] (μ : PMF α) {ε : ℝ≥0∞ (T : Finset α) {f : α → ℝ≥0∞} {B : ℝ≥0∞} (h : ∀ a, f a ≤ (if a ∈ T then 1 else 0) + B) : ∑' a, μ a * f a ≤ T.card * ε + B := by calc ∑' a, μ a * f a ≤ ∑' a, (μ a * (if a ∈ T then 1 else 0) + μ a * B) := - ENNReal.tsum_le_tsum fun a => (mul_le_mul_right (h a) _).trans_eq (mul_add _ _ _) + tsum_le_tsum fun a => (mul_le_mul_right (h a) _).trans_eq (mul_add _ _ _) _ = ∑ a ∈ T, μ a + B := by - rw [ENNReal.tsum_add, ENNReal.tsum_mul_right, μ.tsum_coe, one_mul, + rw [tsum_add, ENNReal.tsum_mul_right, μ.tsum_coe, one_mul, tsum_eq_sum (s := T) fun a ha => by simp only [ha, ↓reduceIte, mul_zero]] congr 1 exact Finset.sum_congr rfl fun a ha => by simp only [ha, ↓reduceIte, mul_one] diff --git a/Complexity/Probability/PMF/Event.lean b/Complexity/Probability/PMF/Event.lean index ce673d7ce..16a45d6e8 100644 --- a/Complexity/Probability/PMF/Event.lean +++ b/Complexity/Probability/PMF/Event.lean @@ -73,7 +73,7 @@ theorem toOuterMeasure_ne_top (p : PMF α) (event : Set α) : p.toOuterMeasure e /-- An event has probability at most one. -/ theorem toOuterMeasure_le_one (p : PMF α) (event : Set α) : p.toOuterMeasure event ≤ 1 := by rw [PMF.toOuterMeasure_apply, ← p.tsum_coe] - exact ENNReal.tsum_le_tsum (fun a => Set.indicator_apply_le (fun _ => le_rfl)) + exact tsum_le_tsum (fun a => Set.indicator_apply_le (fun _ => le_rfl)) /-- The event that `f a` deviates from `m` by at least `ε` is covered by the upper tail `m + ε ≤ f a` and the lower tail `f a ≤ m - ε`. -/ @@ -111,7 +111,7 @@ theorem toOuterMeasure_apply_toReal [Fintype α] (p : PMF α) (event : Set α) : theorem toOuterMeasure_toReal_add_compl (p : PMF α) (event : Set α) : (p.toOuterMeasure event).toReal + (p.toOuterMeasure eventᶜ).toReal = 1 := by have h : p.toOuterMeasure event + p.toOuterMeasure eventᶜ = 1 := by - rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add] + rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← tsum_add] convert p.tsum_coe using 1 congr 1 funext a @@ -154,7 +154,7 @@ theorem toOuterMeasure_bind_failure_le (p : PMF α) (kernel : α → PMF β) rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply] calc _ ≤ ∑' a, ((preᶜ).indicator p a + p a * error) := by - apply ENNReal.tsum_le_tsum + apply tsum_le_tsum intro a by_cases ha : a ∈ pre · simp only [Set.indicator_of_notMem (show a ∉ preᶜ by simpa), zero_add] @@ -165,7 +165,7 @@ theorem toOuterMeasure_bind_failure_le (p : PMF α) (kernel : α → PMF β) · simp only [Set.indicator_of_mem (show a ∈ preᶜ from ha)] exact (mul_le_mul_of_nonneg_left (toOuterMeasure_le_one (kernel a) failure) zero_le).trans (by simp) - _ = _ := by rw [ENNReal.tsum_add, ENNReal.tsum_mul_right, p.tsum_coe, one_mul] + _ = _ := by rw [tsum_add, ENNReal.tsum_mul_right, p.tsum_coe, one_mul] /-- The real-valued error rule for a randomized continuation. -/ theorem toOuterMeasure_bind_failure_toReal_le (p : PMF α) (kernel : α → PMF β) @@ -193,7 +193,7 @@ theorem toOuterMeasure_bind_ge_mul (p : PMF α) (kernel : α → PMF β) classical have hle : p.toOuterMeasure pre * ENNReal.ofReal s₂ ≤ (p.bind kernel).toOuterMeasure event := by rw [PMF.toOuterMeasure_bind_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_mul_right] - refine ENNReal.tsum_le_tsum fun a => ?_ + refine tsum_le_tsum fun a => ?_ by_cases ha : a ∈ pre · simp only [Set.indicator_of_mem ha] by_cases hs : a ∈ p.support @@ -242,7 +242,7 @@ theorem map_true_mono (p : PMF α) {E F : α → Bool} (h : ∀ a ∈ p.support, E a = true → F a = true) : (p.map E) true ≤ (p.map F) true := by rw [PMF.map_apply, PMF.map_apply] - refine ENNReal.tsum_le_tsum fun a => ?_ + refine tsum_le_tsum fun a => ?_ by_cases ha : a ∈ p.support · by_cases hE : true = E a · simp [← hE, h a ha hE.symm] @@ -253,8 +253,8 @@ theorem map_true_mono (p : PMF α) {E F : α → Bool} theorem map_true_le_add (p : PMF α) {E A B : α → Bool} (h : ∀ a ∈ p.support, E a = true → A a = true ∨ B a = true) : (p.map E) true ≤ (p.map A) true + (p.map B) true := by - rw [PMF.map_apply, PMF.map_apply, PMF.map_apply, ← ENNReal.tsum_add] - refine ENNReal.tsum_le_tsum fun a => ?_ + rw [PMF.map_apply, PMF.map_apply, PMF.map_apply, ← tsum_add] + refine tsum_le_tsum fun a => ?_ by_cases ha : a ∈ p.support · by_cases hE : true = E a · rcases h a ha hE.symm with hA | hB diff --git a/Complexity/Probability/PMF/Map.lean b/Complexity/Probability/PMF/Map.lean index eed796d9b..4aad0a45d 100644 --- a/Complexity/Probability/PMF/Map.lean +++ b/Complexity/Probability/PMF/Map.lean @@ -40,7 +40,7 @@ variable {α β : Type*} theorem le_map_apply (p : PMF α) (f : α → β) (a : α) : p a ≤ (p.map f) (f a) := by classical rw [PMF.map_apply] - simpa using ENNReal.le_tsum (f := fun x => if f a = f x then p x else 0) a + simpa using le_tsum (f := fun x => if f a = f x then p x else 0) a /-- Relabeling a distribution by an equivalence preserves each corresponding point mass. -/ theorem map_equiv_apply (p : PMF α) (e : α ≃ β) (b : β) : diff --git a/Complexity/Probability/ProductConditioning/SideInformation.lean b/Complexity/Probability/ProductConditioning/SideInformation.lean index 316b7c63c..11c12f8fe 100644 --- a/Complexity/Probability/ProductConditioning/SideInformation.lean +++ b/Complexity/Probability/ProductConditioning/SideInformation.lean @@ -186,7 +186,7 @@ theorem sideJoint_apply (μ : PMF T) (J : T → PMF ((∀ i, β i) × V)) (t : T exact hx (Prod.ext (congrArg Prod.snd h).symm (congrArg (·.2) (congrArg Prod.fst h)).symm) · intro t' ht' rw [PMF.map_apply] - refine mul_eq_zero_of_right _ (ENNReal.tsum_eq_zero.mpr fun x => ite_eq_right fun h => ?_) + refine mul_eq_zero_of_right _ (tsum_eq_zero_iff.mpr fun x => ite_eq_right fun h => ?_) exact absurd (congrArg (·.1) (congrArg Prod.fst h)) (Ne.symm ht') /-- The pairs `(u, v)` that complete `(t, v)` to an outcome in `W`. -/ diff --git a/Complexity/Probability/RejectionSampling.lean b/Complexity/Probability/RejectionSampling.lean index d317c0d2f..83b85bf82 100644 --- a/Complexity/Probability/RejectionSampling.lean +++ b/Complexity/Probability/RejectionSampling.lean @@ -144,7 +144,7 @@ theorem shiftReject_apply_some (hv : ∀ z ∈ S, z - v ∈ B) (z : α) : · intro y hy have hyz : y + v ≠ z := fun h => hy (eq_sub_of_add_eq h) split_ifs <;> simp_all [eq_comm] - · refine ENNReal.tsum_eq_zero.mpr fun y => ?_ + · refine tsum_eq_zero_iff.mpr fun y => ?_ split_ifs with h₁ h₂ <;> simp_all /-- **Rejection sampling, aborts.** Under the same hypothesis, the sampler aborts with @@ -156,7 +156,7 @@ theorem shiftReject_apply_none (hv : ∀ z ∈ S, z - v ∈ B) : rw [tsum_eq_sum (s := S) fun z hz => by simp [hz], Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul, div_eq_mul_inv] have htotal := (shiftReject B S hB v).tsum_coe - rw [ENNReal.tsum_eq_add_tsum_ite none, ← (Option.some_injective α).tsum_eq] at htotal + rw [tsum_eq_add_tsum_ite none, ← (Option.some_injective α).tsum_eq] at htotal · simp only [reduceCtorEq, ite_false, hsome] at htotal exact ENNReal.eq_sub_of_add_eq (ENNReal.div_ne_top (ENNReal.natCast_ne_top _) (by simpa using hB.ne_empty)) htotal From d7dcd7985e43c0678127230df389fa8ea3e3ea61 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 15:21:52 -0400 Subject: [PATCH 3/5] fix(build): adapt proofs to the rc2 Mathlib API Qualify newly protected matrix and finite-sum lemmas, publicly import the relocated Matrix.Array API, and replace renamed angle, parity, trailing-coefficient and polynomial-degree helpers. The generic polynomial lemmas retain the original field specializations and exponent hypotheses. No theorem statement or definition body changes. Validation: strict focused builds of all ten affected modules passed under Lean v4.36.0-rc2. Source comparison against d6ccb24f shows all Lean edits are inside theorem proofs except the required Bird import. --- Complexity/Computability/Circuit/Bird.lean | 1 + Complexity/Computability/Circuit/Quantum/Basic.lean | 4 ++-- Complexity/Computability/Circuit/Rational/Wronskian.lean | 2 +- .../Foundations/BooleanAnalysis/LowDegree/Addition.lean | 2 +- .../Foundations/BooleanAnalysis/SparseEquations.lean | 2 +- .../FieldTheory/Finite/LinearizedPolynomial.lean | 6 +++--- Complexity/Foundations/LinearAlgebra/Matrix/ListProd.lean | 4 ++-- Complexity/Foundations/LinearAlgebra/Matrix/Rank.lean | 2 +- .../Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean | 8 ++++---- Complexity/Foundations/Probability/Gaussian/Sheppard.lean | 2 +- 10 files changed, 17 insertions(+), 16 deletions(-) diff --git a/Complexity/Computability/Circuit/Bird.lean b/Complexity/Computability/Circuit/Bird.lean index 62b11531b..a39c61ae9 100644 --- a/Complexity/Computability/Circuit/Bird.lean +++ b/Complexity/Computability/Circuit/Bird.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Init +public import Mathlib.LinearAlgebra.Matrix.Array public import Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic import Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite diff --git a/Complexity/Computability/Circuit/Quantum/Basic.lean b/Complexity/Computability/Circuit/Quantum/Basic.lean index 7797874a4..c9265f0f4 100644 --- a/Complexity/Computability/Circuit/Quantum/Basic.lean +++ b/Complexity/Computability/Circuit/Quantum/Basic.lean @@ -172,7 +172,7 @@ theorem place_apply (A : Fin k ↪ Fin n) (U : unitaryGroup (Fin k → Bool) ℂ (place A U : Matrix _ _ ℂ) y x = if ∀ j, (¬∃ i, A i = j) → y j = x j then (U : Matrix _ _ ℂ) (y ∘ A) (x ∘ A) else 0 := by simp only [place, MonoidHom.coe_mk, OneHom.coe_mk, submatrix_apply, kroneckerMap_apply, - splitEquiv_apply_fst, splitEquiv_apply_snd, one_apply, funext_iff, Subtype.forall] + splitEquiv_apply_fst, splitEquiv_apply_snd, Matrix.one_apply, funext_iff, Subtype.forall] split_ifs <;> simp namespace PlacedGate @@ -281,7 +281,7 @@ theorem hadamardMatrix_mem_unitaryGroup : hadamardMatrix ∈ unitaryGroup Bool rw [mem_unitaryGroup_iff] ext b c cases b <;> cases c <;> - simp [hadamardMatrix, mul_apply, star_eq_conjTranspose, Complex.conj_ofReal, h2, h1] + simp [hadamardMatrix, Matrix.mul_apply, star_eq_conjTranspose, Complex.conj_ofReal, h2, h1] theorem star_hadamardMatrix : star hadamardMatrix = hadamardMatrix := by ext b c diff --git a/Complexity/Computability/Circuit/Rational/Wronskian.lean b/Complexity/Computability/Circuit/Rational/Wronskian.lean index f2ce76817..138a37718 100644 --- a/Complexity/Computability/Circuit/Rational/Wronskian.lean +++ b/Complexity/Computability/Circuit/Rational/Wronskian.lean @@ -148,7 +148,7 @@ lemma wronskian_order_of_distinct_orders {K : Type*} [Field K] [CharZero K] Matrix.det_mul_row (fun j => (f j).trailingCoeff) (Matrix.of fun i j : Fin h => ((f j).natTrailingDegree.descFactorial i.val : K))] exact mul_ne_zero (Finset.prod_ne_zero_iff.mpr fun j _ => - trailingCoeff_nonzero_iff_nonzero.mpr (hf j)) (det_descFactorial_ne_zero _ hd) + trailingCoeff_ne_zero.mpr (hf j)) (det_descFactorial_ne_zero _ hd) have hB0 : B.det ≠ 0 := fun hz => by simp [hz] at hBc have hA0 : A.det ≠ 0 := hdet ▸ mul_ne_zero (pow_ne_zero _ X_ne_zero) hB0 have hscale : A.det = X ^ (∑ i : Fin h, i.val) * wronskianFamily f := by diff --git a/Complexity/Foundations/BooleanAnalysis/LowDegree/Addition.lean b/Complexity/Foundations/BooleanAnalysis/LowDegree/Addition.lean index 905b6c11a..271991b3b 100644 --- a/Complexity/Foundations/BooleanAnalysis/LowDegree/Addition.lean +++ b/Complexity/Foundations/BooleanAnalysis/LowDegree/Addition.lean @@ -82,7 +82,7 @@ theorem hasSliceDecomposition_add (p q : ℕ) : have hexpand : (fun x y : ι → Bool => monomial K S.1 (x + y)) = ∑ T ∈ S.1.powerset, (fun x y => monomial K T x * monomial K (S.1 \ T) y) := by funext x y - simp only [sum_apply, monomial_add] + simp only [Finset.sum_apply, monomial_add] rw [hexpand] apply (sliceSpace (lowDegree K ι p) (lowDegree K ι q)).sum_mem intro T hT diff --git a/Complexity/Foundations/BooleanAnalysis/SparseEquations.lean b/Complexity/Foundations/BooleanAnalysis/SparseEquations.lean index d9daca94e..d1bc719e3 100644 --- a/Complexity/Foundations/BooleanAnalysis/SparseEquations.lean +++ b/Complexity/Foundations/BooleanAnalysis/SparseEquations.lean @@ -143,7 +143,7 @@ is even. -/ theorem monomialSum_zmod_two_eq_zero_iff_even (𝓜 : Finset (Finset ι)) (x : ι → Bool) : monomialSum (ZMod 2) 𝓜 x = 0 ↔ Even (monomialSum ℤ 𝓜 x) := by rw [monomialSum_eq_card_filter (ZMod 2), monomialSum_eq_card_filter ℤ, - ZMod.natCast_eq_zero_iff_even, Int.even_coe_nat] + ZMod.natCast_eq_zero_iff_even, Int.even_natCast] /-- An assignment `x : ι → Bool` is a common zero of the family `{P i}_{i ∈ I}` over `𝔽₂` if every equation `P i` (`i ∈ I`) evaluates to `0` in `ZMod 2` at `x`. -/ diff --git a/Complexity/Foundations/FieldTheory/Finite/LinearizedPolynomial.lean b/Complexity/Foundations/FieldTheory/Finite/LinearizedPolynomial.lean index 09309146e..a27032be5 100644 --- a/Complexity/Foundations/FieldTheory/Finite/LinearizedPolynomial.lean +++ b/Complexity/Foundations/FieldTheory/Finite/LinearizedPolynomial.lean @@ -252,7 +252,7 @@ private theorem comp_eq_X_pow_card_sub_X [Fintype F] {P Q : F[X]} ⟨by rw [natDegree_comp, hdeg], hQm.comp hPm hPdeg⟩ have hX : IsMonicOfDegree (X ^ Fintype.card F - X : F[X]) (Fintype.card F) := by rw [isMonicOfDegree_iff] - refine ⟨(FiniteField.X_pow_card_sub_X_natDegree_eq F hq1).le, ?_⟩ + refine ⟨(natDegree_X_pow_sub_X (R := F) hq1).le, ?_⟩ have h1 : (1 : ℕ) ≠ Fintype.card F := hq1.ne simp [coeff_X, h1] rw [← sub_eq_zero] @@ -410,10 +410,10 @@ theorem exists_subfield_card_le [Finite F] {n k : ℕ} (hn : finrank (ZMod 2) F have h1 : 1 < 2 ^ k := Nat.one_lt_two_pow hk0.ne' have hcard : Fintype.card F = 2 ^ n := by rw [Module.card_eq_pow_finrank (K := ZMod 2) (V := F), ZMod.card, hn] - refine FiniteField.X_pow_card_sub_X_ne_zero F h1 + refine X_pow_sub_X_ne_zero (R := F) h1 (eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ (f := id) Function.injective_id (fun x => by simp [hall x]) ?_) - rw [FiniteField.X_pow_card_sub_X_natDegree_eq F h1, hcard] + rw [natDegree_X_pow_sub_X (R := F) h1, hcard] exact Nat.pow_lt_pow_right (by norm_num) hkn · by_cases hW : ∃ y₀ ∈ W, y₀ ≠ 0 · obtain ⟨y₀, hy₀W, hy₀⟩ := hW diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/ListProd.lean b/Complexity/Foundations/LinearAlgebra/Matrix/ListProd.lean index 11579b762..50ea8c7ef 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/ListProd.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/ListProd.lean @@ -38,7 +38,7 @@ theorem list_prod_ofFn_apply : ∀ {d : ℕ} (M : Fin d → Matrix ι ι R) (a b if p 0 = a ∧ p (Fin.last d) = b then ∏ i : Fin d, M i (p i.castSucc) (p i.succ) else 0 | 0, M, a, b => by rw [← (Equiv.funUnique (Fin 1) ι).symm.sum_comp] - simp only [List.ofFn_zero, List.prod_nil, one_apply, Finset.univ_eq_empty, + simp only [List.ofFn_zero, List.prod_nil, Matrix.one_apply, Finset.univ_eq_empty, Finset.prod_empty, Equiv.funUnique_symm_apply, Fin.last_zero, uniqueElim_const] by_cases hab : a = b · subst hab @@ -51,7 +51,7 @@ theorem list_prod_ofFn_apply : ∀ {d : ℕ} (M : Fin d → Matrix ι ι R) (a b have hL : (List.ofFn M).prod a b = ∑ q : Fin (d + 1) → ι, if q (Fin.last d) = b then M 0 a (q 0) * ∏ i : Fin d, M i.succ (q i.castSucc) (q i.succ) else 0 := by - rw [List.ofFn_succ, List.prod_cons, mul_apply] + rw [List.ofFn_succ, List.prod_cons, Matrix.mul_apply] simp only [list_prod_ofFn_apply (fun i => M i.succ), Finset.mul_sum, mul_ite, mul_zero] rw [Finset.sum_comm] refine Finset.sum_congr rfl fun q _ => ?_ diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/Rank.lean b/Complexity/Foundations/LinearAlgebra/Matrix/Rank.lean index 04e6d3604..de84069b6 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/Rank.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/Rank.lean @@ -87,7 +87,7 @@ theorem exists_eq_mul_rank (A : Matrix m n K) : (b.sum_repr (col j)) simp only [Submodule.coe_sum, Submodule.coe_smul, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] at h - simpa [mul_apply, col, mul_comm] using h.symm + simpa [Matrix.mul_apply, col, mul_comm] using h.symm /-- The natural rank of a finite matrix agrees with the cardinal rank of its linear map. -/ theorem natCast_rank_eq_rank_toLin' [DecidableEq n] (M : Matrix m n K) : diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean b/Complexity/Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean index 16c25ab37..7d6f58267 100644 --- a/Complexity/Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean +++ b/Complexity/Foundations/LinearAlgebra/Matrix/SubmatrixRobust.lean @@ -340,17 +340,17 @@ theorem add_blockRank_le_cutRank_add_transpose [Finite ι] (hfg.symm.mono inter_subset_right inter_subset_right) (fun i hi j hj hj' => by have hjY : j ∉ Y := fun h => hj' ⟨hj, h⟩ - simp only [add_apply, transpose_apply, hMY i j hjY, hMY j i (hnotY i hi.2), add_zero]) + simp only [Matrix.add_apply, transpose_apply, hMY i j hjY, hMY j i (hnotY i hi.2), add_zero]) (fun i hi j hj hj' => by have hjX : j ∉ X := fun h => hj' ⟨hj, h⟩ - simp only [add_apply, transpose_apply, hMX i j (hnotX i hi.2), hMX j i hjX, add_zero]) + simp only [Matrix.add_apply, transpose_apply, hMX i j (hnotX i hi.2), hMX j i hjX, add_zero]) have hb₁ : R.blockRank (f ⁻¹' U) (g ⁻¹' Uᶜ) ≤ (M + Mᵀ).blockRank (U ∩ X) Uᶜ := by calc R.blockRank (f ⁻¹' U) (g ⁻¹' Uᶜ) = M.blockRank (U ∩ X) (Uᶜ ∩ Y) := by rw [← hMR, M.blockRank_submatrix hf hg, image_preimage_eq_inter_range, image_preimage_eq_inter_range] _ = (M + Mᵀ).blockRank (U ∩ X) (Uᶜ ∩ Y) := blockRank_congr fun i hi j _ => by - simp only [add_apply, transpose_apply, hMY j i (hnotY i hi.2), add_zero] + simp only [Matrix.add_apply, transpose_apply, hMY j i (hnotY i hi.2), add_zero] _ ≤ (M + Mᵀ).blockRank (U ∩ X) Uᶜ := blockRank_mono_right _ _ inter_subset_left have hb₂ : R.blockRank (f ⁻¹' Uᶜ) (g ⁻¹' U) ≤ (M + Mᵀ).blockRank (U ∩ Y) Uᶜ := by calc R.blockRank (f ⁻¹' Uᶜ) (g ⁻¹' U) @@ -359,7 +359,7 @@ theorem add_blockRank_le_cutRank_add_transpose [Finite ι] image_preimage_eq_inter_range] _ = Mᵀ.blockRank (U ∩ Y) (Uᶜ ∩ X) := (M.blockRank_transpose _ _).symm _ = (M + Mᵀ).blockRank (U ∩ Y) (Uᶜ ∩ X) := blockRank_congr fun i hi j _ => by - simp only [add_apply, transpose_apply, hMX i j (hnotX i hi.2), zero_add] + simp only [Matrix.add_apply, transpose_apply, hMX i j (hnotX i hi.2), zero_add] _ ≤ (M + Mᵀ).blockRank (U ∩ Y) Uᶜ := blockRank_mono_right _ _ inter_subset_left unfold cutRank omega diff --git a/Complexity/Foundations/Probability/Gaussian/Sheppard.lean b/Complexity/Foundations/Probability/Gaussian/Sheppard.lean index e3c419ba0..e18ca8f6d 100644 --- a/Complexity/Foundations/Probability/Gaussian/Sheppard.lean +++ b/Complexity/Foundations/Probability/Gaussian/Sheppard.lean @@ -308,7 +308,7 @@ theorem measureReal_stdGaussian_mem_uIoc_le_angle {u v : E} (huv : ‖u‖ = ‖ simp only [hu, hv, inner_zero_left, uIoc_of_le le_rfl, Ioc_self, mem_empty_iff_false, ofPred_false, measureReal_empty] exact div_nonneg (InnerProductGeometry.angle_nonneg _ _) pi_pos.le - · rw [eq_neg_of_add_eq_zero_right hne, InnerProductGeometry.angle_self_neg_of_nonzero hu, + · rw [eq_neg_of_add_eq_zero_right hne, InnerProductGeometry.angle_self_neg_of_ne_zero hu, div_self pi_ne_zero] exact measureReal_le_one · rw [InnerProductGeometry.angle_eq_two_mul_arctan huv hne] From f5a70cb9826c88744c1dfbc560340d3efebbfb04 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 15:26:19 -0400 Subject: [PATCH 4/5] test(quantum): qualify the protected matrix lemma Preserve the existing non-unitary matrix counterexample under rc2 Mathlib by explicitly selecting Matrix.mul_apply, as in the library proof repairs. --- ComplexityTests/QuantumCircuit.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ComplexityTests/QuantumCircuit.lean b/ComplexityTests/QuantumCircuit.lean index a440e1a4b..cca9dbe2c 100644 --- a/ComplexityTests/QuantumCircuit.lean +++ b/ComplexityTests/QuantumCircuit.lean @@ -158,7 +158,7 @@ example : ¬Circuit.IsOver {⟨3, Gate.toffoli⟩} [h₀] := fun h => example : !![(1 : ℂ), 1; 0, 1] ∉ unitaryGroup (Fin 2) ℂ := by intro h have := congrFun (congrFun (mem_unitaryGroup_iff.mp h) 0) 0 - simp [mul_apply, Fin.sum_univ_two, star_eq_conjTranspose] at this + simp [Matrix.mul_apply, Fin.sum_univ_two, star_eq_conjTranspose] at this -- A two-qubit gate cannot be placed on a one-qubit register: the wires must be distinct. example : IsEmpty (Fin 2 ↪ Fin 1) := From bb3e910dfc197e46f4b11e0c666b6546a075b7c8 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 15:46:20 -0400 Subject: [PATCH 5/5] fix(build): normalize goals before proof automation Use expected-type-directed refinement for the generic zero-sum lemma and expose the determinant variable-count function before fun_prop. Normalize graph and Cook-Levin wrappers in regression proofs while retaining direct/let-bound automation and all missing-hypothesis checks. Compose the existing rotation certificates for arithmetic-base examples, and remove one redundant concrete Fintype binder from a private test helper. Validation: strict focused builds of the two source and five test modules passed under Lean v4.36.0-rc2. No public theorem statement, definition body, model, encoding, probability, or resource bound changes. No heartbeat or fun_prop compatibility option was introduced. --- Complexity/Algorithms/WordRAM/KargerMinCut.lean | 2 +- .../Computability/Circuit/Arithmetic/Determinant.lean | 4 +++- ComplexityTests/ExpanderContraction.lean | 3 ++- ComplexityTests/ExpanderFamily.lean | 1 + ComplexityTests/ExplicitExpanders.lean | 8 ++++++-- ComplexityTests/Iteration/SparseDisplacement.lean | 2 +- ComplexityTests/MultiTapePolyTime.lean | 1 + 7 files changed, 15 insertions(+), 6 deletions(-) diff --git a/Complexity/Algorithms/WordRAM/KargerMinCut.lean b/Complexity/Algorithms/WordRAM/KargerMinCut.lean index c07c84a3c..5cf511394 100644 --- a/Complexity/Algorithms/WordRAM/KargerMinCut.lean +++ b/Complexity/Algorithms/WordRAM/KargerMinCut.lean @@ -1181,7 +1181,7 @@ theorem ampLoop_spec {w sb n R : ℕ} {W : Fin n → Fin n → ℕ} {mem₀ : obtain ⟨m_r, hm_r, _, hsup_r, _⟩ := hnext z₁ hz₁ rw [hml_def, hm_r.codeComp_eq, PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply] - convert tsum_eq_zero_iff.mpr _ + refine tsum_eq_zero_iff.mpr ?_ intro z₂ by_cases hz₂_eval : z₂ ∈ m_r.eval.support · have hz₂ : z₂ ∈ m_r.support := (ProbComp.support_eval m_r) ▸ hz₂_eval diff --git a/Complexity/Computability/Circuit/Arithmetic/Determinant.lean b/Complexity/Computability/Circuit/Arithmetic/Determinant.lean index 1f231b4cf..01cf49231 100644 --- a/Complexity/Computability/Circuit/Arithmetic/Determinant.lean +++ b/Complexity/Computability/Circuit/Arithmetic/Determinant.lean @@ -272,7 +272,9 @@ generic determinants has `n * n` variables, degree at most `n` and arithmetic ci `3 * n ^ 4 + 4` gates. -/ theorem detFamily_mem_VP : detFamily K ∈ VP K := by choose c hc hsize using exists_circuit_det (K := K) - refine ⟨⟨by fun_prop, PolynomiallyBounded.id.mono_of_le fun n => + refine ⟨⟨?_, PolynomiallyBounded.id.mono_of_le fun n => totalDegree_det_genericMatrix_le n⟩, c, PolynomiallyBounded.mono_of_le (by fun_prop) hsize, hc⟩ + change PolynomiallyBounded (fun n : ℕ => n * n) + fun_prop end Cslib.Circuits.Arithmetic diff --git a/ComplexityTests/ExpanderContraction.lean b/ComplexityTests/ExpanderContraction.lean index ac59474d9..1bd9d7150 100644 --- a/ComplexityTests/ExpanderContraction.lean +++ b/ComplexityTests/ExpanderContraction.lean @@ -68,7 +68,7 @@ example : ComputableInPolyTime threeVertices.rot have hg : ComputableInPolyTime completeFive.rot (encPair (encFinEnum (Fin 5)) (encFinEnum (Fin 5))) (encPair (encFinEnum (Fin 5)) (encFinEnum (Fin 5))) := .of_finite _ - fun_prop [threeVertices, RotationMap.contractFin] + exact ComputableInPolyTime.rotationMap_contract he hd hg example {V W I D : Type} (G : RotationMap V D) (encode : V → W × I) (decode : W × I → Option V) (hinv : Function.IsPartialInv encode decode) @@ -80,6 +80,7 @@ example {V W I D : Type} (G : RotationMap V D) (encode : V → W × I) (fun p : (W × (I × D)) × Bool => ((RotationMap.contract encode decode hinv G).rot p.1, !p.2)) (encPair (encPair ew (encPair ei ed)) encBool) (encPair (encPair ew (encPair ei ed)) encBool) := by + dsimp only [RotationMap.contract, RotationMap.contractRot, RotationMap.contractDart] fail_if_success (clear he; fun_prop) fail_if_success (clear hd; fun_prop) fail_if_success (clear hg; fun_prop) diff --git a/ComplexityTests/ExpanderFamily.lean b/ComplexityTests/ExpanderFamily.lean index 0dd5ac6e9..51163712e 100644 --- a/ComplexityTests/ExpanderFamily.lean +++ b/ComplexityTests/ExpanderFamily.lean @@ -96,6 +96,7 @@ example {V W D : Type} (G : RotationMap V D) (e : V ≃ W) let next := (G.reindex e).rot p.1 (next, !p.2)) (encPair (encPair ew ed) encBool) (encPair (encPair ew ed) encBool) := by + dsimp only [RotationMap.reindex, RotationMap.reindexRot] fail_if_success (clear hf; fun_prop) fail_if_success (clear hb; fun_prop) fail_if_success (clear hg; fun_prop) diff --git a/ComplexityTests/ExplicitExpanders.lean b/ComplexityTests/ExplicitExpanders.lean index a912aabc8..c8d706921 100644 --- a/ComplexityTests/ExplicitExpanders.lean +++ b/ComplexityTests/ExplicitExpanders.lean @@ -64,7 +64,8 @@ example {K : Type} [Field K] (encode : K ↪ List Bool) ComputableInPolyTime (RotationMap.affinePlaneTowerBase K).rot (encPair (baseEncoding encode) (planeEncoding encode)) (encPair (baseEncoding encode) (planeEncoding encode)) := by - fun_prop [RotationMap.affinePlaneTowerBase] + have hplane := ComputableInPolyTime.rotationMap_affinePlane hmul hsub + exact ((hplane.rotationMap_tensor hplane).rotationMap_zigzag hplane).rotationMap_zigzag hplane -- Only the fixed field operations use the finite-domain theorem; graph products compose them. example (encode : ZMod 257 ↪ List Bool) : @@ -75,7 +76,8 @@ example (encode : ZMod 257 ↪ List Bool) : (planeEncoding encode) encode := .of_finite _ have hsub : ComputableInPolyTime (fun p : ZMod 257 × ZMod 257 => p.1 - p.2) (planeEncoding encode) encode := .of_finite _ - fun_prop [RotationMap.affinePlaneTowerBase] + have hplane := ComputableInPolyTime.rotationMap_affinePlane hmul hsub + exact ((hplane.rotationMap_tensor hplane).rotationMap_zigzag hplane).rotationMap_zigzag hplane -- Equivalent direct and let-bound spellings, with a supplied rotation on an arbitrary type. example {V D E : Type} (G : RotationMap V D) (H : RotationMap D E) @@ -86,6 +88,7 @@ example {V D E : Type} (G : RotationMap V D) (H : RotationMap D E) (fun p : ((V × D) × (E × E)) × Bool => ((G.zigzag H).rot p.1, !p.2)) (encPair (encPair (encPair vertex label) (encPair small small)) encBool) (encPair (encPair (encPair vertex label) (encPair small small)) encBool) := by + dsimp only [RotationMap.zigzag, RotationMap.zigzagRot] fail_if_success (clear hG; fun_prop) fail_if_success (clear hH; fun_prop) fun_prop @@ -100,6 +103,7 @@ example {V D E : Type} (G : RotationMap V D) (H : RotationMap D E) (next, !p.2)) (encPair (encPair (encPair vertex label) (encPair small small)) encBool) (encPair (encPair (encPair vertex label) (encPair small small)) encBool) := by + dsimp only [RotationMap.zigzag, RotationMap.zigzagRot] fun_prop end ComplexityTests.ExplicitExpanders diff --git a/ComplexityTests/Iteration/SparseDisplacement.lean b/ComplexityTests/Iteration/SparseDisplacement.lean index 634e74f09..fbe746f4f 100644 --- a/ComplexityTests/Iteration/SparseDisplacement.lean +++ b/ComplexityTests/Iteration/SparseDisplacement.lean @@ -34,7 +34,7 @@ example : private def editedCounter : Equiv.Perm (BitVec 2) := (Equiv.swap 0 1).trans (Equiv.addRight 1) -private theorem editedCounter_disagreement [Fintype (BitVec 2)] : +private theorem editedCounter_disagreement : disagreement editedCounter (fun x => x + 1) = {0, 1} := by ext x simp only [mem_disagreement, Finset.mem_insert, Finset.mem_singleton] diff --git a/ComplexityTests/MultiTapePolyTime.lean b/ComplexityTests/MultiTapePolyTime.lean index 2042aace5..8fde4c4a0 100644 --- a/ComplexityTests/MultiTapePolyTime.lean +++ b/ComplexityTests/MultiTapePolyTime.lean @@ -139,6 +139,7 @@ example {α : Type} (enc : α ↪ List Bool) (p : Polynomial ℕ) (c d : ℕ) : ComputableTidilyInPolyTime (fun a => List.range (Cslib.Complexity.CookLevin.parameters p c d enc a).2.2) enc (encList encUnary) := by + dsimp only [Cslib.Complexity.CookLevin.parameters] fun_prop private def finish (move : SignType) (symbol : Bool) : Turing.MultiTapeTM 0 Bool Unit :=