StepFourBoundaryPairTrim

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The trimmed harmonic replacement pair, and the hvn residue produced

The residue

Every statement of the boundary lane carries

   hvn : MemLp v.toFun 2 (volume.restrict (truncatedWindow z m n))

as a hypothesis — a standing residue. It has no producer, and for a good reason: v = u - w with w ∈ H¹₀(moved cube), and an H¹₀ witness constrains its function only on its own domain (H10Function's memL2, gradMemL2, hasWeakGradient and tendsto_approx are all read on volume.restrict U), so w.toFun is unconstrained off the cube and v.toFun need not be in L² of any larger window.

The fix, and why it is not a cheat

Re-read the pair with w replaced by 1_U · w. So exists_harmonicReplacementPair_movedCube_memLp delivers the pair with hvn included, and excessDecay_stepFour_decay_allCentres_datumSplit_trimmed is the Step-4 slot with both the competitor disjunction and hvn gone.

What remains

Exactly one carried input: hgradh: HasGradientOn (truncatedWindow z m (n-2)) h.toFun h.grad, the classical C¹ half of the print's h ∈ C^{1,1/2}(□_m), which the frozen root's binder block does not carry.

References

• ABK26, l.excess.decay.good.scales; t.regularity Step 4.

theorem Algsuperdiff.Section4.Provider.Regularity.hasWeakGradientOn_congr_on {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) {f g : HCPolySupport.Vec d → ℝ} {Du : HCPolySupport.Vec d → HCPolySupport.Vec d} (hfg : ∀ y ∈ U, f y = g y) (hf : HCPolySupport.HasWeakGradientOn U f Du) : HCPolySupport.HasWeakGradientOn U g Du

theorem Algsuperdiff.Section4.Provider.Regularity.ae_eq_of_forall_mem {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) {f g : HCPolySupport.Vec d → ℝ} (hfg : ∀ y ∈ U, f y = g y) : f =ᵐ[MeasureTheory.volume.restrict U] g

noncomputable def Algsuperdiff.Section4.Provider.Regularity.h1Trim {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (v : HCPolySupport.H1Function U) : HCPolySupport.H1Function U

Re-reading an H¹(U) function as 1_U · f: the H¹ structure sees only U.

Equations

• Algsuperdiff.Section4.Provider.Regularity.h1Trim hU v = { toFun := U.indicator v.toFun, grad := v.grad, memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ }

@[simp]

theorem Algsuperdiff.Section4.Provider.Regularity.h1Trim_toFun {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (v : HCPolySupport.H1Function U) : (h1Trim hU v).toFun = U.indicator v.toFun

@[simp]

theorem Algsuperdiff.Section4.Provider.Regularity.h1Trim_grad {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (v : HCPolySupport.H1Function U) : (h1Trim hU v).grad = v.grad

noncomputable def Algsuperdiff.Section4.Provider.Regularity.h10Trim {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (w : HCPolySupport.H10Function U) : HCPolySupport.H10Function U

The same re-reading for an H¹₀(U) function.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algsuperdiff.Section4.Provider.Regularity.h10Trim_toFun {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (w : HCPolySupport.H10Function U) : (h10Trim hU w).toFun = U.indicator w.toFun

theorem Algsuperdiff.Section4.Provider.Regularity.memLp_indicator_of_memL2 {d : ℕ} {U W : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict U)) : MeasureTheory.MemLp (U.indicator f) 2 (MeasureTheory.volume.restrict W)

Membership in L² of the trimmed corrector, on ANY window.

theorem Algsuperdiff.Section4.Provider.Regularity.exists_harmonicReplacementPair_movedCube_memLp {d : ℕ} [NeZero d] {m n : ℤ} {z : HCPolySupport.Vec d} (hnm : n - 2 ≤ m) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) : ∃ (v : HCPolySupport.H1Function ((fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)))) (w : HCPolySupport.H10Function ((fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)))), Support.IsWeaklyHarmonicOn ((fun (y : HCPolySupport.Vec d) => ExcessDecay.wellPlacedCentre z m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2))) v ∧ (∀ (y : HCPolySupport.Vec d), v.toFun y = u.toFun y - w.toFun y) ∧ (∀ (y : HCPolySupport.Vec d), v.grad y = u.grad y - w.grad y) ∧ ∀ (W : Set (HCPolySupport.Vec d)), MeasureTheory.MemLp u.toFun 2 (MeasureTheory.volume.restrict W) → MeasureTheory.MemLp v.toFun 2 (MeasureTheory.volume.restrict W)

The trimmed harmonic replacement pair.

The pair at the moved cube, re-read so that the H¹₀ corrector vanishes off its own cube. Every clause of the original is preserved and the pair now also carries MemLp v.toFun 2 on every window — the standing residue hvn of the boundary Step-4 slot.

3. The slot with the disjunction AND hvn discharged

theorem Algsuperdiff.Section4.Provider.Regularity.excessDecay_stepFour_decay_allCentres_datumSplit_trimmed (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ) (Ccap : ℝ) (Cb : ℝ), 0 < C ∧ 0 < Ccap ∧ 0 ≤ Cb ∧ ∃ (k₀ : ℕ), 3 ≤ k₀ ∧ ∀ (k : ℕ), k₀ ≤ k → ∀ (M : Section3.ABKModel d), ∀ s ∈ Set.Icc (64 * M.gamma) 1, M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ Ccap⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ (hs : 0 < s), ∀ delta ∈ Set.Ioc 0 1, delta ≤ 64 * (C ^ 2)⁻¹ * s ^ 6 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (s / 8 * √delta) → ExcessDecay.edBridgeEpsConstGen d (max (ExcessDecay.Schauder.schauderWindowConst d) Cb) C k * Ccap * s.rpow (-3) * √delta ≤ 1 / 2 * 3 ^ (-(1 / 4) * (↑k + 1)) → ∀ (L m : ℤ), m ≤ L → ∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (n : ℤ), n + 1 ≤ m → omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 1) z ⟨s / 8, ⋯⟩ (s / 8 * √delta) → ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (gflux : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u hdat gflux → MeasureTheory.MemLp gflux 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 gflux) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 hdat.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → ∀ (Kh : ℝ), 0 ≤ Kh → Support.HolderSeminormBoundOn (ExcessDecay.truncatedWindow z m (n - 2)) (1 / 2) Kh hdat.grad → Support.HasGradientOn (ExcessDecay.truncatedWindow z m (n - 2)) hdat.toFun hdat.grad → ∀ (c : ℝ) (gmin : HCPolySupport.Vec d), Support.IsAffineMinimizer (ExcessDecay.truncatedWindow z m (n + 1)) u.toFun c gmin → Support.affineExcess (ExcessDecay.truncatedWindow z m (n + 1 - ↑(k + 1))) u.toFun ≤ 3 ^ (-(1 / 4) * (↑k + 1)) * Support.affineExcess (ExcessDecay.truncatedWindow z m (n + 1)) u.toFun + ExcessDecay.edBridgeEps M (ExcessDecay.edBridgeEpsConstGen d (max (ExcessDecay.Schauder.schauderWindowConst d) Cb) C k) L s ⟨s / 8, ⋯⟩ z omega n * Support.slopeMagnitude gmin + (ExcessDecay.edBridgeDeltaErrorWeighted M C (ExcessDecay.edBridgeRemWeightGen d (max (ExcessDecay.Schauder.schauderWindowConst d) Cb) k) L m s ⟨s / 8, ⋯⟩ z gflux hdat.grad omega n + ExcessDecay.edBridgeDatumLeg d (max (ExcessDecay.Schauder.schauderWindowConst d) Cb) k n Kh)

The Step-4 decay at every centre, both boundary residues gone.

The slot of StepFourBoundaryDatumPackage with the harmonic replacement pair produced internally in its trimmed form, so that hvn disappears from the binder block. What is left is the slot's own data plus the single input hgradh — the classical C¹ half of the printed datum hypothesis h ∈ C^{1,1/2}(□_m), which the frozen root does not carry.