ReindexEnergy

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

The interior Caccioppoli energy at the slot n+3: the (n+3) family on □_{n+2}

The sharpened interior energy estimate is proved at the proved slot: the coefficient family is ã_{L,n+2}, the comparator is σ_{n+2}, and the good event is 𝒢(n+2, z; s/8, 1/2). The frozen general clause reads the good event and the flux index at n+3, so this module re-runs the same estimate with

• the comparator σ_{n+3} in place of σ_{n+2};
• the caps read on the chain's own cube □_{n+2} through the depth-1 centre-child transport of ReindexSlot (factor 3^{s/8} ≤ 3^{1/8}).

Everything geometric is unchanged: the Caccioppoli triple is the author's own outer = □_{n+2}, patch = w + □_{n+1}, core = w + □_n. The cube of the display, its 3-power weights 3^{-2(n+2)} and 3^{2s(n+2)}, the parameter pair (1/4, s/4), the Besov index s/2 → s comparison and the force envelope s^{-6} are all the proved ones, byte-for-byte.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS; e.energy.bound.interior; l.harmonic.approximation.good.scales.

1. The display object, in the cube's own frame

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.constantDatumEnergyRHSAddThree {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : ℝ) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d (n + 2))).carrier) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) : ℝ

The sharpened interior Caccioppoli right-hand side at the n+3 slot. The sharpened interior right-hand side with the comparator index moved to n+3; the cube and both 3-power weights are unchanged.

Equations

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

2. The two private arithmetic helpers

3. The equation at the (n+3) family

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isForcedEquation_fluxCorrectedCoeffFamily_translated_addThree {d : ℕ} {m n : ℤ} (M : Section3.ABKModel d) (L : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) {u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hfr : (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ frontier (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) = ∅) (heq : Support.IsDivFormWeakSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u g) : HCPolySupport.Book.Ch03.IsForcedEquation (HCPolySupport.originCube d (n + 2)) (Support.fluxCorrectedCoeffFamily M L (n + 3) (HCPolySupport.originCube d (n + 3)) (Section3.Cutoff.translateCutoffSample z omega)) (HCPolySupport.H1Function.untranslate z (u.restrict ⋯ ⋯)) fun (x : HCPolySupport.Vec d) => -g (x + z)

4. The energy estimate on the good event, in the cube's own frame

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_constantDatumEnergy_harmonicSlot_addThree (d : ℕ) [NeZero d] : ∃ (C : ℝ) (Cout : ℝ), 0 < C ∧ 0 < Cout ∧ ∀ (M : Section3.ABKModel d), ∀ s ∈ Set.Icc (64 * M.gamma) 1, M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (1 / 2) → ∀ (hs : 0 < s) (n : ℤ) (z : HCPolySupport.Vec d), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → ∀ (L : ℤ), n + 3 ≤ L → ∀ (w : HCPolySupport.Vec d) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d (n + 2))).carrier), HCPolySupport.Book.Ch03.openCubeAtScale w (n + 1) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) → HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) s g → HCPolySupport.Book.Ch03.IsForcedEquation (HCPolySupport.originCube d (n + 2)) (Support.fluxCorrectedCoeffFamily M L (n + 3) (HCPolySupport.originCube d (n + 3)) (Section3.Cutoff.translateCutoffSample z omega)) u g → HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.Book.Ch03.caccioppoliCoreSet (HCPolySupport.originCube d (n + 2)) w) ((Support.fluxCorrectedCoeffFamily M L (n + 3) (HCPolySupport.originCube d (n + 3)) (Section3.Cutoff.translateCutoffSample z omega)).coeffOn (HCPolySupport.originCube d (n + 2))) u ≤ Cout * constantDatumEnergyRHSAddThree M n s u g

The sharpened e.energy.bound.interior at the n+3 slot.

Almost surely on the frozen general clause's good event 𝒢(n+3, z; s/8, 1/2), for every L ≥ n+3, every window centre w whose Dirichlet patch w + □_{n+1} sits inside □_{n+2}, and every H¹(□_{n+2}) solution of -∇·ã_{L,n+3}∇u = ∇·g,

  ⨍_{□_{n+2} ∩ (w+□_n)} ∇u · ã_{L,n+3} ∇u ≤ Cout · constantDatumEnergyRHSAddThree M n s u g .

5. The display in the frozen theorem's own carriers

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.constantDatumAnchorEnergyRHSOnAddThree {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : ℝ) (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) : ℝ

The sharpened right-hand side at the n+3 slot, in the anchor's own carriers.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.constantDatumEnergyRHS_le_anchorRHS_addThree {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (n : ℤ) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) {z : HCPolySupport.Vec d} {f : HCPolySupport.Vec d → ℝ} (v : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d (n + 2))).carrier) (hv : v.toFun = fun (y : HCPolySupport.Vec d) => f (y + z)) (hmem : MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => f (y + z)) 2 (HCPolySupport.normalizedCubeMeasure (HCPolySupport.originCube d (n + 2)))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (hgL2 : MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))))) (hgW : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))))) : (constantDatumEnergyRHSAddThree M n s v fun (y : HCPolySupport.Vec d) => -g (y + z)) ≤ (besovGagliardoConstant d ^ 2 + 1) * constantDatumAnchorEnergyRHSOnAddThree M n s ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) f g

The carrier conversion of the n+3 display.

6. The energy estimate at the anchor's own geometry

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_constantDatumEnergy_anchorWindow_addThree (d : ℕ) [NeZero d] : ∃ (C : ℝ) (Cout : ℝ), 0 < C ∧ 0 < Cout ∧ ∀ (M : Section3.ABKModel d), ∀ s ∈ Set.Icc (64 * M.gamma) 1, M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (1 / 2) → ∀ (hs : 0 < s) (L m n : ℤ), m ≤ L → n + 3 ≤ m → ∀ (x z : HCPolySupport.Vec d) (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → ∀ (hfr : (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ frontier (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) = ∅), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u hdat g → MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → HCPolySupport.Book.Ch03.localizedCoeffEnergyValue ((fun (y : HCPolySupport.Vec d) => x - z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ((Support.fluxCorrectedCoeffFamily M L (n + 3) (HCPolySupport.originCube d (n + 3)) (Section3.Cutoff.translateCutoffSample z omega)).coeffOn (HCPolySupport.originCube d (n + 2))) (HCPolySupport.H1Function.untranslate z (u.restrict ⋯ ⋯)) ≤ Cout * constantDatumAnchorEnergyRHSOnAddThree M n s ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun g

The (n+3) interior energy estimate, at the frozen statement's binders.

Verbatim the sharpened interior energy estimate — same hypotheses (with the frozen binder n + 3 ≤ m and the general clause's good event), same left-hand energy value, same window — with the coefficient family and the comparator index at n+3.