StepSixInteriorEndpoint

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

theorem Algsuperdiff.Section4.Provider.Regularity.edFinal_oscillationHolderBound_interior (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ) (Cann : ℝ), 0 < C ∧ 0 < Cann ∧ ∃ (k₀ : ℕ), 3 ≤ k₀ ∧ ∀ (k : ℕ), k₀ ≤ k → 2 ≤ k → ∃ (Cout : ℝ) (Citer : ℝ), 0 < Cout ∧ 0 ≤ Citer ∧ ∀ (M : Section3.ABKModel d) (m0 : ℤ) (Ecap : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Ecap → M.gamma < 1 / 2 → M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ Cann⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ 1 / 256 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (stepOneS / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (C⁻¹ * stepOneS ^ 4) → ∀ (Cedos Cannp alpha : ℝ), alpha ≤ 1 → stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha ∈ Set.Ioc 0 (1 / 2) → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp (stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha) → edFinalEpsCoeff d C k stepOneS * (Cann * stepOneEp (stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha)) ≤ 1 / 2 * 3 ^ (-(1 / 4) * ↑k) → ∀ (L m n : ℤ), m ≤ L → m ≤ m0 → 14 ≤ m - n → ∀ v ∈ Support.latticeCubeSet d n m, Support.triadicLatticePoint n v ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), GoodScaleWindows M stepOneSEighth (stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha) stepOneSEighth_pos n m omega → ↑(stepThreeBadSet M (stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha) n m (Support.triadicLatticePoint n v) omega).card ≤ stepOneDelta (stepOneC1 d Cedos Cannp Citer k) alpha * (↑m - ↑n + 1) → ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg : ℝ), 0 ≤ Kg → 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 stepOneS 2 g) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 hdat.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → ∀ (c : ℤ → ℝ) (slope : ℤ → HCPolySupport.Vec d), (∀ j ≤ m, Support.IsAffineMinimizer (stepThreeWindow (Support.triadicLatticePoint n v) m j) u.toFun (c j) (slope j)) → ∀ (n' m' : ℤ), n ≤ n' → ⋯

For z = 3^n v ∈ □_{m-1} and every n ≤ n' ≤ m' ≤ m,

   3^{-n'} ‖u - (u)_{U_{n'}}‖_{L²(U_{n'})}
     ≤ (C_out + C_out²) 3^{(1/2)(1-α)(m-n)} 3^{-m'} ‖u - (u)_{U_{m'}}‖_{L²(U_{m'})}
       + (C_out + C_out²) 3^{(1/2)(1-α)(m-n)} ( dataG + 0 ) .

No Step-4 decay hypothesis and no Step-5 conditional: the whole chain runs off the harmonic-approximation anchor and the Step-3 supply events.