OneStepSchauderComposeInterior

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

The interior-branch excess-decay endpoint, conditional only on the anchor

OneStepSchauderChain.excessDecay_oneStep_interior_of_harmonicApprox closed the Schauder slot of the interior branch, but it still assumed that the competitor is classically harmonic on the replacement window (hharmclass). What the competitor producer (ResidualCorrectorExistence.exists_weaklyHarmonicOn_of_datum) delivers is the variational Support.IsWeaklyHarmonicOn. Weyl's lemma (OneStepWeylRepresentative.exists_harmonicRepresentative_full) bridges the two, and this module performs the composition.

The result, excessDecay_oneStep_interior_of_weaklyHarmonic, carries exactly one derived-result hypothesis, hharm, transcribed verbatim from OneStepConditional (the anchor's conclusion), plus the standing frame and the variational harmonicity of the competitor. The four Schauder slots and hharmclass are gone.

Why the competitor lives on the moved replacement cube

The anchor states its L² bound on the moved replacement cube R = y + □_{n-2} with y = wellPlacedCentre x m (n-2) — a full open cube — and OneStepWindows.truncatedWindow_subset_image_add_windowChoice puts the replacement window (x + □_{n-2}) ∩ □_m inside it. Weyl's lemma is therefore applied at U := R, where it yields harmonicity on all of R (the full form, obtained in OneStepWeylRepresentative by gluing the fixed-radius representatives), hence on the replacement window; and the same statement gives v = w almost everywhere on R, which is exactly what makes hharm transfer from w to v — eLpNorm is an almost-everywhere invariant. Both MemLp slots come free: the representative agrees almost everywhere with the zero extension 𝟙_R w, hence is globally square integrable.

1. The moved replacement cube as a domain

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOpen_movedReplacementCube {d : ℕ} (x : HCPolySupport.Vec d) (m n : ℤ) : IsOpen (movedReplacementCube x m n)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.measurableSet_movedReplacementCube {d : ℕ} (x : HCPolySupport.Vec d) (m n : ℤ) : MeasurableSet (movedReplacementCube x m n)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow_subset_movedReplacementCube {d : ℕ} (x : HCPolySupport.Vec d) {m n : ℤ} (hnm : n - 2 ≤ m) : truncatedWindow x m (n - 2) ⊆ movedReplacementCube x m n

theorem Algsuperdiff.Section4.Provider.ExcessDecay.movedReplacementCube_subset_truncatedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m n : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 2 ≤ m) : movedReplacementCube x m n ⊆ truncatedWindow x m n

2. The competitor's smooth harmonic representative

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_classicalCompetitor_movedReplacementCube {d : ℕ} [NeZero d] (x : HCPolySupport.Vec d) (m n : ℤ) {w : HCPolySupport.H1Function (movedReplacementCube x m n)} (hw : Support.IsWeaklyHarmonicOn (movedReplacementCube x m n) w) : ∃ (v : HCPolySupport.Vec d → ℝ), InnerProductSpace.HarmonicOnNhd (v ∘ ⇑Schauder.toEuc.symm) (⇑Schauder.toEuc '' movedReplacementCube x m n) ∧ MeasureTheory.MemLp v 2 MeasureTheory.volume ∧ v =ᵐ[MeasureTheory.volume.restrict (movedReplacementCube x m n)] w.toFun

The classical competitor. From a variationally harmonic H¹ function on the anchor's moved replacement cube, Weyl's lemma produces a globally square-integrable representative which is classically harmonic on the whole cube and agrees with it almost everywhere there.

3. The composed interior endpoint

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessDecay_oneStep_interior_of_weaklyHarmonic {d : ℕ} [NeZero d] (hd : d ≠ 0) {m n : ℤ} {k : ℕ} (hk : 3 ≤ k) {M : Section3.ABKModel d} {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) {delta : ℝ} (hdelta1 : delta ≤ 1) {x z : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 1 ≤ m) (hcube : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {u : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (truncatedWindow x m n))) {w : HCPolySupport.H1Function ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)))} (hw : Support.IsWeaklyHarmonicOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2))) w) {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n - 2 + 3) z ⟨s / 8, ⋯⟩ (s / 8 * √delta)) {B : ENNReal} (hB : B ≠ ⊤) (hharm : (Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n - 2 + 3) z ⟨s / 8, ⋯⟩ (1 / 2)).indicator (fun (_omega' : Section3.Cutoff.CutoffSample d) => MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u y - w.toFun y) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2))))) omega ≤ B) : Support.affineExcess (truncatedWindow x m (n - ↑k)) u ≤ taylorContractionConst d * Schauder.schauderWindowConst d * windowRatioConst d 2 * (3 ^ (-↑k)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m n) u + triangleRemainderConst d (Schauder.schauderWindowConst d) k * (3 ^ (-n) * (√((3 ^ 2) ^ d) * B.toReal)) + taylorContractionConst d * (3 ^ (n - ↑k)) ^ (1 / 2) * 0

The one-step excess-decay contraction on the interior branch, conditional only on the harmonic-approximation anchor.

Identical to OneStepConditional.excessDecay_oneStep_of_harmonicApprox with Csch = schauderWindowConst d and K_h = 0, and with the four Schauder slots and the classical-harmonicity slot of OneStepSchauderChain all discharged: the competitor enters only through the variational condition Support.IsWeaklyHarmonicOn on the anchor's own moved replacement cube, which is what ResidualCorrectorExistence.exists_weaklyHarmonicOn_of_datum produces.

The hharm binder is transcribed verbatim from OneStepConditional, with the competitor read as w.toFun; eLpNorm is an almost-everywhere invariant, so the smooth representative may be substituted inside the proof without touching the statement.