InteriorComposed

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

The interior clause, composed at the honest exponents

The payoff of the-- residue: one almost-sure statement, entered at the frozen theorem's own binders and concluded in the frozen theorem's own carriers,

  1_𝒢 ‖u − v‖_{L²(x+□_n)}
      ≤ C ( s^{-4}    𝓔_{s/8}(z+□_{n+2}; ã_{L,n+2}, σ_{n+2}) ‖u − (u)_W‖_{L²(W)}
          + s^{-19/2} σ_{n+2}^{-1} 3^{(1+s)n} [g]_{H^s(W)} ) ,
      W = (z + □_{n+2}) ∩ □_m .

This is the frozen interior clause at the honest s-powers: the printed display carries s^{-3/2} and s^{-7} where the proved chain gives s^{-4} and s^{-19/2}. Every other carrier is the anchor's, byte for byte: the same left-hand eLpNorm, the same fluxCorrectedErrorRepresentative at the printed index s/8 and at the translated sample, the same mean-subtracted parent norm, the same normalizedGagliardo on the parent-intersected window.

What goes into it

• InteriorEllipticitySlot: the coarse-graining slot re-cut at r = s/3 (so that the child's coarse-graining index is s/6 > s/8), and the x-frame composition at the re-based family;
• InteriorEllipticity: the child-frame 𝓔 against the anchor's own representative, and CoarseGraining's forcing bracket collapsed on the good event;
• InteriorWindowMove: the Gagliardo seminorm from the child window to the anchor's parent-intersected window;
• GoodEventCaps: the representative's cap, used only in the second summand (the first keeps it, as the frozen statement does).

Deviations from the printed statement

• the σ index: the second summand carries σ_{n+2}^{-1}; the printed one carries σ_n^{-1}, and SigmaBarIndex.exists_inv_sigmaBar_add_two_le converts at the factor 4 inside the anchor's own regime.
• no γ-move is made anywhere.

References

• ABK26, l.harmonic.approximation.good.scales; e.homogenization.L2.interior.

1. The composed interior estimate

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_interiorClause_honest (d : ℕ) [NeZero d] : ∃ (C : ℝ) (Cfin : ℝ), 0 < C ∧ 0 < Cfin ∧ ∀ (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 + 2 ≤ m → ∀ (x z : HCPolySupport.Vec d), 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) → (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 + 2) 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 (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → ∀ (v : HCPolySupport.H1Function ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) (w : HCPolySupport.H10Function ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))), Support.IsWeaklyHarmonicOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) 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) → (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))).toReal ≤ Cfin * (s.rpow (-4) * Support.fluxCorrectedErrorRepresentative M L (n + 2) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) * (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + s.rpow (-(19 / 2)) * (↑(Section3.Annealed.sigmaBar M (n + 2)))⁻¹ * Real.rpow 3 ((1 + s) * ↑n) * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s g).toReal)

The interior clause at the honest exponents.

See the module docstring for the deviation list; the two s-powers are the proved chain's own, not the printed ones.