From 97de3c9e17b5af397706ebb10e26a95cf51093ab Mon Sep 17 00:00:00 2001 From: Moritz Doll Date: Wed, 24 Jun 2026 14:44:15 +1000 Subject: [PATCH] fixes --- DynamicalSystems/Basic/Autonomous.lean | 2 +- DynamicalSystems/Engineering/RLCCircuit.lean | 2 +- lake-manifest.json | 28 ++++++++++---------- lakefile.toml | 4 +-- lean-toolchain | 2 +- 5 files changed, 19 insertions(+), 19 deletions(-) diff --git a/DynamicalSystems/Basic/Autonomous.lean b/DynamicalSystems/Basic/Autonomous.lean index 32982ed..1573f06 100644 --- a/DynamicalSystems/Basic/Autonomous.lean +++ b/DynamicalSystems/Basic/Autonomous.lean @@ -91,7 +91,7 @@ theorem IsSemigroupOn.comm [AddCommMagma ι] [Zero ι] (hΦ : IsSemigroupOn Φ s rw [← hΦ.add t₀ t₁ x hx, ← hΦ.add t₁ t₀ x hx, add_comm] variable [TopologicalSpace E] [AddCommMonoid ι] [Preorder ι] [IsDirectedOrder ι] [AddLeftMono ι] - [TopologicalSpace ι] [ContinuousAdd ι] + [TopologicalSpace ι] open Filter diff --git a/DynamicalSystems/Engineering/RLCCircuit.lean b/DynamicalSystems/Engineering/RLCCircuit.lean index 0ef0fe4..5bc5f24 100644 --- a/DynamicalSystems/Engineering/RLCCircuit.lean +++ b/DynamicalSystems/Engineering/RLCCircuit.lean @@ -39,7 +39,7 @@ theorem integral_differentiableAt (hf : Continuous f) (a) : variable {μ : MeasureTheory.Measure ℝ} {a b : ℝ} -- should be in mathlib -theorem integral_nonneg_of_Ioo [MeasureTheory.NoAtoms μ] (hab : a ≤ b) +theorem integral_nonneg_of_Ioo [MeasureTheory.NullSingletonClass μ] (hab : a ≤ b) (hf : IntervalIntegrable f μ a b) (h : ∀ x ∈ Set.Ioo a b, 0 ≤ f x) : 0 ≤ ∫ u in a..b, f u ∂μ := by convert intervalIntegral.integral_mono_on_of_le_Ioo hab _ hf h diff --git a/lake-manifest.json b/lake-manifest.json index 2be3a58..ec7d8b8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,27 +5,27 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f", + "rev": "3ee3f85eb48438ad4f8ce98b79a198f6573d5f70", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "master-2026-06-22", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/verso", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "891a59f2318e507d7df274c92a8f827dcc6823ea", + "rev": "8cb04559a9b9feb8efab43e135f662514561f668", "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0-rc1", + "inputRev": "v4.32.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", + "rev": "f3f26cc72646205ca167117487c008ee1dafe816", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d", + "rev": "41f407a8e85b0fdc00910633a8f14754139b63f4", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9", + "rev": "e6518a674e62de322b8f79eebeda7bcae2a36bc3", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f", + "rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", + "rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fa08db58b30eb033edcdab331bba000827f9f785", + "rev": "7d1b02eb63b526dff04cb990cf05b06b38ccbd3f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "08da3f6f41c075e0c18d37eb0fd417c10ed77b6e", + "rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e", "name": "illuminate", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,7 +115,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ce893b9042128037e2d3c0158b9567fab9fae268", + "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -125,10 +125,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", + "rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "DynamicalSystems", diff --git a/lakefile.toml b/lakefile.toml index 08a2996..27b8003 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -14,12 +14,12 @@ warn.sorry = false [[require]] name = "verso" scope = "leanprover" -rev = "v4.31.0" +rev = "v4.32.0-rc1" [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.31.0" +rev = "master-2026-06-22" [[lean_lib]] name = "DynamicalSystems" diff --git a/lean-toolchain b/lean-toolchain index 133a3f7..63f51ea 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.31.0 \ No newline at end of file +leanprover/lean4:v4.32.0-rc1 \ No newline at end of file