Benchmark / DynamicalSystems

DynamicalSystems: Mathlib v4.31.0 → v4.35.0

lake build passes after repair. The bump spans 4 Mathlib releases and produced 7 raw build errors in 2 files; an alias rewrite resolves 0 of them.

Project: mcdoll/DynamicalSystems. First build after the bump: 60.8 s, 6 deprecation warnings (1 with a replacement an alias rewrite would apply).

Local copies removed. 1 declaration the project defined itself, now provided by Mathlib at v4.35.0 (each checked there):

DynamicalSystems/Mathlib/Dynamics/Basic.lean::flow

Repairs

Arm	lake build	Rebuilds	Agent min	Labelled changes
Arm A (diagnosing session, not blind)	green	5	20	4 signature change, 1 rename

What changed, labelled

Label	File	What changed in Mathlib, and the repair
signature change	DynamicalSystems/Mathlib/Dynamics/Basic.lean	Homeomorph.flow was upstreamed under the same name ('already declared'); local copy deleted.
signature change	DynamicalSystems/Basic/LpLoc.lean	memLp_indicator_iff_restrict / MemLp.indicator now take NullMeasurableSet: added .nullMeasurableSet at 2 call sites.
signature change	DynamicalSystems/Basic/LpLoc.lean	MemLp is now a def for `eLpNorm f p μ < ∞` (measurability dropped): anonymous-constructor proofs replaced by the plain hypotheses.
rename	DynamicalSystems/Engineering/RLCCircuit.lean	MeasureTheory.NoAtoms is now an alias of NullSingletonClass and no longer usable as an instance binder: [NoAtoms μ] -> [NullSingletonClass μ].
signature change	DynamicalSystems/InputOutput/Stability.lean	Cascade: same NullMeasurableSet argument (4 sites), eLpNorm_indicator_le gained its measurability argument, Lp.eLpNorm_le_of_ae_tendsto gained a measurability goal for the limit (hfu u hu), MemLp constructor removed.

The diff

diff --git a/DynamicalSystems/Basic/LpLoc.lean b/DynamicalSystems/Basic/LpLoc.lean

index f4941da..c1e1dbd 100644

--- a/DynamicalSystems/Basic/LpLoc.lean

+++ b/DynamicalSystems/Basic/LpLoc.lean

@@ -94,7 +94,7 @@ theorem MemLpLoc.const_smul (hu : MemLpLoc u p μ) : MemLpLoc (c • u) p μ :=

theorem memLpLoc_iff_memLp_indicator :

MemLpLoc u p μ ↔ ∀ s : Set α, MeasurableSet s ∧ IsBounded s → MemLp (s.indicator u) p μ := by

congrm (∀ s, (hs : _) → ?_)

- rw [memLp_indicator_iff_restrict hs.1]

+ rw [memLp_indicator_iff_restrict hs.1.nullMeasurableSet]

theorem MemLpLoc.memLp_indicator {s₀ : Set α} (hs₀ : MeasurableSet s₀) (hs₀' : IsBounded s₀)

(hu : MemLpLoc u p μ) : MemLp (s₀.indicator u) p μ := by

@@ -105,7 +105,7 @@ theorem MemLpLoc.memLp_indicator {s₀ : Set α} (hs₀ : MeasurableSet s₀) (h

theorem MemLpLoc.indicator {s₀ : Set α} (hs₀ : MeasurableSet s₀) (hu : MemLpLoc u p μ) :

MemLpLoc (s₀.indicator u) p μ := by

intro s hs

- exact (hu s hs).indicator hs₀

+ exact (hu s hs).indicator hs₀.nullMeasurableSet

@[fun_prop]

theorem MemLp.memLpLoc (hu : MemLp u p μ) : MemLpLoc u p μ := by

@@ -174,8 +174,9 @@ def LpLoc (μ : Measure α := by volume_tac) : AddSubgroup (α →ₘ[μ] E) whe

apply AEEqFun.coeFn_zero

add_mem' {f g} hf hg := by

intro s hs

- convert eLpNorm_add_lt_top

- ⟨f.aestronglyMeasurable.restrict, hf s hs⟩ ⟨g.aestronglyMeasurable.restrict, hg s hs⟩ using 1

+ have hf' : MemLp f p (μ.restrict s) := hf s hs

+ have hg' : MemLp g p (μ.restrict s) := hg s hs

+ convert eLpNorm_add_lt_top hf' hg' using 1

apply eLpNorm_congr_ae

apply Filter.EventuallyEq.restrict

filter_upwards [AEEqFun.coeFn_add f g] with x h

diff --git a/DynamicalSystems/Engineering/RLCCircuit.lean b/DynamicalSystems/Engineering/RLCCircuit.lean

index f9bf99f..f738b94 100644

--- a/DynamicalSystems/Engineering/RLCCircuit.lean

+++ b/DynamicalSystems/Engineering/RLCCircuit.lean

@@ -40,7 +40,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/DynamicalSystems/InputOutput/Stability.lean b/DynamicalSystems/InputOutput/Stability.lean

index 0f3bee3..76ba108 100644

--- a/DynamicalSystems/InputOutput/Stability.lean

+++ b/DynamicalSystems/InputOutput/Stability.lean

@@ -137,13 +137,13 @@ theorem isLpStable (hf : IsFiniteGainStableWith f k β s p μ)

(hfu : ∀ u (_hu : MemLp u p μ), AEStronglyMeasurable (f u) μ)

(hs : AECover μ atTop s) :

IsLpStable f p μ := by

- refine ⟨fun u hu ↦ ⟨hfu u hu, ?_⟩⟩

+ refine ⟨fun u hu ↦ ?_⟩

/- For every `t ∈ I`, we have that `‖(f u)ₜ‖ ≤ k * ‖uₜ‖ + β ≤ k * ‖u‖ + β`-/

have : ∀ᶠ t in atTop, eLpNorm ((s t).indicator (f u)) p μ ≤ k * eLpNorm u p μ + β := by

filter_upwards with t

calc

_ = eLpNorm (f u) p (μ.restrict (s t)) :=

- eLpNorm_indicator_eq_eLpNorm_restrict (hs.measurableSet t)

+ eLpNorm_indicator_eq_eLpNorm_restrict (hs.measurableSet t).nullMeasurableSet

_ ≤ k * eLpNorm u p (μ.restrict <| s t) + β := hf.stableWith t u hu.memLpLoc

_ ≤ _ := by gcongr; exact Measure.restrict_le_self

calc

@@ -151,6 +151,7 @@ theorem isLpStable (hf : IsFiniteGainStableWith f k β s p μ)

apply MeasureTheory.Lp.eLpNorm_le_of_ae_tendsto this

· intro t

exact (hfu u hu).indicator (hs.measurableSet t)

+ · exact hfu u hu

· apply hs.ae_tendsto_indicator

_ < _ := by

simp [MemLp.eLpNorm_lt_top hu, ENNReal.mul_lt_top_iff]

@@ -171,16 +172,16 @@ theorem IsCausal.isFiniteGainStableWith (hf : IsCausal f s p μ) (k β : ℝ≥0

· intro t u hu

calc

_ = eLpNorm ((s t).indicator (f u)) p μ :=

- (eLpNorm_indicator_eq_eLpNorm_restrict (hs t).1).symm

+ (eLpNorm_indicator_eq_eLpNorm_restrict (hs t).1.nullMeasurableSet).symm

_ = eLpNorm ((s t).indicator (f <| (s t).indicator u)) p μ := by

rw [← hf.causal t u hu]

_ ≤ eLpNorm (f <| (s t).indicator u) p μ :=

- eLpNorm_indicator_le (f ((s t).indicator u))

+ eLpNorm_indicator_le (f ((s t).indicator u)) (hs t).1.nullMeasurableSet

_ ≤ ↑k * eLpNorm ((s t).indicator u) p μ + β := by

apply h

exact hu.memLp_indicator (hs t).1 (hs t).2

_ = _ := by

- rw [eLpNorm_indicator_eq_eLpNorm_restrict (hs t).1]

+ rw [eLpNorm_indicator_eq_eLpNorm_restrict (hs t).1.nullMeasurableSet]

/- Todo: define the gain -/

diff --git a/DynamicalSystems/Mathlib/Dynamics/Basic.lean b/DynamicalSystems/Mathlib/Dynamics/Basic.lean

index e248840..63420e9 100644

--- a/DynamicalSystems/Mathlib/Dynamics/Basic.lean

+++ b/DynamicalSystems/Mathlib/Dynamics/Basic.lean

@@ -50,23 +50,6 @@ example : f ^ 0 = Equiv.refl _ := by

simp only [pow_zero]

exact Equiv.Perm.one_def

-namespace Homeomorph

-variable [TopologicalSpace α] (f : Homeomorph α α)

-/-- The discrete flow `ℤ → α → α` induced by a homeomorphism `f : α → α`. -/

-def flow (f : Homeomorph α α) : Flow ℤ α where

- toFun n x := (f ^ n) x

- cont' := by

- rw [continuous_prod_of_discrete_left]

- intro n

- simp only [Function.uncurry_apply_pair]

- fun_prop

- map_add' n₁ n₂ := by

- simp_rw [← mul_apply, ← Homeomorph.ext_iff, zpow_add]

- map_zero' x := by simp

-end Homeomorph

end Discrete

Re-run it

source bench/env.sh
python3 bench/lbbench.py setup dynamicalsystems      # clone mcdoll/DynamicalSystems at v4.31.0, bump the Mathlib pin to v4.35.0
python3 bench/lbbench.py build dynamicalsystems      # cache get + lake build; writes the raw errors to bench/runs/dynamicalsystems/v4.35.0/errors.json
git -C bench/work/dynamicalsystems/proj apply ../../../runs/dynamicalsystems/v4.35.0/armA.diff   # replay the recorded repair
python3 bench/lbbench.py build dynamicalsystems --pass replay        # a green replay prints "build rc=0"

Files

Correct this page

Something wrong on this row, or you maintain this project and want it off the benchmark? Correct this row or remove my project.