Leanbump

Benchmark / DirichletProblem

DirichletProblem: Mathlib v4.29.0 → v4.33.0

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

Project: mcdoll/DirichletProblem. First build after the bump: 37.3 s, 0 deprecation warnings (0 with a replacement an alias rewrite would apply).

Local copies removed. 9 declarations the project defined itself, now provided by Mathlib at v4.33.0 (each checked there):
  • DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean::Lp.coe_fourierTransformInv
  • DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean::Lp.fourierTransformInv
  • DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean::Lp.fourierTransformInvCLM
  • DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean::Lp.fourierTransformInvCLM_apply
  • DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean::Lp.fourierTransformInv_apply
  • DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean::Lp.fourierTransformInv_toLp
  • DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean::compContinuousCLM
  • DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean::compContinuousCLM_apply
  • DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean::fourierInv_congr_ae

Repairs

Armlake buildRebuildsAgent minLabelled changes
Arm A (diagnosing session, not blind)green4151 signature change, 3 reproof
Arm A2 (fresh agent, compiler output only: blind)green471 signature change, 2 reproof
Arm B (fresh agent, compiler output plus enclosing declarations: blind)green481 signature change, 2 reproof

What changed, labelled

LabelFileWhat changed in Mathlib, and the repair
signature changeDirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean9 local declarations (compContinuousCLM, Real.Lp.fourierTransformInv & co.) were upstreamed to Mathlib under the same names: 'already declared'. Local copies deleted.
reproofDirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.leanTwo norm_*_le_toLp_one steps: simp no longer closes the goal after the upstream norm_toZeroAtInfty simp lemma; replaced `simpa using` with show/rw/exact (x2).
reproofDirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.leanAdded SchwartzMap.fourier_coe to a simpa call (coercion form of 𝓕 changed).
reproofDirichletProblem/Sobolev/Basic.leanCascade after the first fix: simpa only set needed toDistr_smul, RingHom.id_apply.

The diff

diff --git a/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean b/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean
index c9f1cf7..5a3977f 100644
--- a/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean
+++ b/DirichletProblem/Mathlib/Analysis/Fourier/FourierTransform.lean
@@ -20,69 +20,3 @@ variable [FiniteDimensional ℝ V]
open scoped BoundedContinuousFunction FourierTransform
open MeasureTheory
-
-section CompContinuousCLM
-
-namespace BoundedContinuousFunction
-
-variable {𝕜 α β γ : Type*} [TopologicalSpace α] [SeminormedAddCommGroup β] [TopologicalSpace γ]
- [NormedField 𝕜] [NormedSpace 𝕜 β]
-
-variable (𝕜) in
-def compContinuousCLM (g : C(γ, α)) : (α →ᵇ β) →L[𝕜] γ →ᵇ β :=
- LinearMap.mkContinuous
- { toFun f := f.compContinuous g,
- map_add' := by intros; ext; simp,
- map_smul' := by intros; ext; simp }
- 1 (by simpa using norm_compContinuous_le · g)
-
-@[simp]
-theorem compContinuousCLM_apply (f : α →ᵇ β) (g : C(γ, α)) :
- compContinuousCLM 𝕜 g f = f.compContinuous g := rfl
-
-end BoundedContinuousFunction
-
-end CompContinuousCLM
-
-namespace Real
-
-/-- The Fourier transform from `L1` functions to bounded continuous functions. -/
-def Lp.fourierTransformInv (f : Lp (α := V) E 1) : V →ᵇ E :=
- (Lp.fourierTransform f).compContinuous (-ContinuousMap.id V)
-
-theorem fourierInv_congr_ae {f₁ f₂ : V → E} (hf : f₁ =ᵐ[volume] f₂) (x : V) :
- 𝓕⁻ f₁ x = 𝓕⁻ f₂ x := by
- apply integral_congr_ae
- filter_upwards [hf] with _ hf'
- rw [hf']
-
-@[simp]
-theorem Lp.fourierTransformInv_apply (f : Lp (α := V) E 1) (x : V) :
- Lp.fourierTransformInv f x = 𝓕⁻ (f : V → E) x := by
- simp [Lp.fourierTransformInv, fourierInv_eq_fourier_neg]
-
-@[norm_cast]
-theorem Lp.coe_fourierTransformInv (f : Lp (α := V) E 1) :
- (Lp.fourierTransformInv f : V → E) = 𝓕⁻ (f : V → E) := by
- ext x
- simp
-
-@[simp]
-theorem Lp.fourierTransformInv_toLp {f : V → E} (hf : MemLp f 1) :
- (Lp.fourierTransformInv hf.toLp : V → E) = 𝓕⁻ f := by
- simp only [Lp.coe_fourierTransformInv]
- ext x
- exact (Real.fourierInv_congr_ae hf.coeFn_toLp) x
-
-variable (V E) in
-/-- The Fourier transform from `L1` functions to bounded continuous functions as a continuous linear
-map. -/
-def Lp.fourierTransformInvCLM : Lp (α := V) E 1 →L[ℂ] V →ᵇ E :=
- BoundedContinuousFunction.compContinuousCLM ℂ (-ContinuousMap.id V) ∘L Lp.fourierTransformCLM V E
-
-@[simp]
-theorem Lp.fourierTransformInvCLM_apply (f : Lp (α := V) E 1) :
- Lp.fourierTransformInvCLM V E f = Lp.fourierTransformInv f := by
- simp [Lp.fourierTransformInvCLM, Lp.fourierTransformInv]
-
-end Real
diff --git a/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean b/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean
index 9477fa6..f07bedd 100644
--- a/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean
+++ b/DirichletProblem/Mathlib/Analysis/Fourier/ZeroAtInfty.lean
@@ -42,8 +42,10 @@ theorem Lp.fourierTransformZeroAtInftyCLM_toLp_apply (f : 𝓢(V, E)) (x : V) :
apply LinearMap.extendOfNorm_eq
· apply SchwartzMap.denseRange_toLpCLM
norm_num
- use 1
- simpa using norm_fourier_toBoundedContinuousFunction_le_toLp_one
+ refine ⟨1, fun f ↦ ?_⟩
+ show ‖(𝓕 f).toZeroAtInfty‖ ≤ 1 * ‖f.toLp 1 volume‖
+ rw [SchwartzMap.norm_toZeroAtInfty, one_mul]
+ exact norm_fourier_toBoundedContinuousFunction_le_toLp_one f
_ = 𝓕 f x := by simp
@[simp]
@@ -54,7 +56,7 @@ theorem Lp.fourierTransformZeroAtInftyCLM_toBCF (f : Lp (α := V) E 1) :
(isClosed_eq (by fun_prop) (Real.Lp.fourierTransformCLM V E).cont)
intro f
ext x
- simpa using Real.fourier_congr_ae (coeFn_toLp f 1 volume).symm x
+ simpa [SchwartzMap.fourier_coe] using Real.fourier_congr_ae (coeFn_toLp f 1 volume).symm x
theorem Lp.fourierTransformZeroAtInftyCLM_apply_apply (f : Lp (α := V) E 1) (x : V) :
Lp.fourierTransformZeroAtInftyCLM V E f x = 𝓕 (f : V → E) x := by
@@ -82,8 +84,10 @@ theorem Lp.fourierTransformInvZeroAtInftyCLM_toLp_apply (f : 𝓢(V, E)) (x : V)
apply LinearMap.extendOfNorm_eq
· apply SchwartzMap.denseRange_toLpCLM
norm_num
- use 1
- simpa using norm_fourierInv_toBoundedContinuousFunction_le_toLp_one
+ refine ⟨1, fun f ↦ ?_⟩
+ show ‖(𝓕⁻ f).toZeroAtInfty‖ ≤ 1 * ‖f.toLp 1 volume‖
+ rw [SchwartzMap.norm_toZeroAtInfty, one_mul]
+ exact norm_fourierInv_toBoundedContinuousFunction_le_toLp_one f
_ = 𝓕⁻ f x := by simp
@[simp]
diff --git a/DirichletProblem/Sobolev/Basic.lean b/DirichletProblem/Sobolev/Basic.lean
index 2386c61..4ab2663 100644
--- a/DirichletProblem/Sobolev/Basic.lean
+++ b/DirichletProblem/Sobolev/Basic.lean
@@ -300,7 +300,7 @@ def laplacianₗ {s : ℝ} : Sobolev E F s 2 →ₗ[ℂ] Sobolev E F (s - 2) 2 w
simpa using (LineDeriv.laplacianCLM ℂ E 𝓢'(E, F)).map_add f.toDistr g.toDistr
map_smul' c f := by
ext1
- simpa only [laplacian_toDistr, laplacianCLM_apply] using
+ simpa only [laplacian_toDistr, laplacianCLM_apply, toDistr_smul, RingHom.id_apply] using
(LineDeriv.laplacianCLM ℂ E 𝓢'(E, F)).map_smul c f.toDistr
end Sobolev

Re-run it

source bench/env.sh
python3 bench/lbbench.py setup dirichletproblem      # clone mcdoll/DirichletProblem at v4.29.0, bump the Mathlib pin to v4.33.0
python3 bench/lbbench.py build dirichletproblem      # cache get + lake build; writes the raw errors to bench/runs/dirichletproblem/v4.33.0/errors.json
git -C bench/work/dirichletproblem/proj apply ../../../runs/dirichletproblem/v4.33.0/armA.diff   # replay the recorded repair
python3 bench/lbbench.py build dirichletproblem --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.