InteriorEllipticitySlot

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

The coarse-graining slot re-cut at r = s/3

At t = s/8 no admissible u exists.

The obstruction is an artefact of the slot, not of the analysis: CoarseGraining's package constrains only 0 < r < t_prop < 1/2 and r ≤ r₂, so any r ∈ (s/4, 3s/8) is admissible, and every such r has r/2 > s/8. This module re-cuts the slot at

  (s_prop, r, r₂, j) = (3s/4, s/3, s, 0) ,        r/2 = s/6 ,

which is exactly the index the proved off-grid cap (InteriorGlueCap.ae_offGridChildError_le_representative_harmonicSlot, printed slot (s/6, s/8)) delivers.

Deviations from the printed statement

• the slot index r moves from s/4 to s/3. No γ-move and no s-power move is made.
• the constants 216, 1944 replace 1024/3, 16384/3; both are smaller.

References

• ABK26, p.general.coarse.graining; e.homogenization.L2.interior.

1. Two elementary s-power facts

2. The envelope at the re-cut slot

theorem Algsuperdiff.Section4.Provider.ExcessDecay.generalCoarseGrainingL2TwoExponentRHS_thirdSlot_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.Book.Ch03.ForceBesovRegularity Q s g) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) : HCPolySupport.Book.Ch03.generalCoarseGrainingL2TwoExponentRHS 1 Q a a0 (3 * s / 4) (s / 3) s 0 g u ≤ 216 * s⁻¹ ^ 4 * coarseGrainingEnergyTerm Q a a0 (s / 3) u + 1944 * s⁻¹ ^ 6 * coarseGrainingForceTerm Q a a0 (s / 3) s g

The s-envelope at the slot (3s/4, s/3, s, 0).

  RHS₁ ≤ 216 s^{-4} · |a₀|^{1/2} 𝓔_{s/3,∞,1}(Q) ‖∇u‖_a
       + 1944 s^{-6} · (CoarseGraining forcing bracket at `r = s/3`) · [g]_{H^s(Q)} .

3. e.homogenization.L2.interior at the re-cut slot

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGraining_l2_thirdSlot_le {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {sigma0 : ℝ} (hsigma0 : 0 < sigma0) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (w : HCPolySupport.Book.Ch03.CoarseGrainingComparisonDatum Q a (scalarComparator hsigma0) g) (z : HCPolySupport.H10Function (HCPolySupport.cubeSet Q)) (hz : ∀ (x : HCPolySupport.Vec d), z.grad x = w.u.grad x - w.v.grad x) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hg : HCPolySupport.Book.Ch03.ForceBesovRegularity Q s g) : sigma0 * (HCPolySupport.cubeBesovScaleWeight 1 Q * HCPolySupport.cubeLpNorm Q 2 fun (x : HCPolySupport.Vec d) => z.toFun x) ≤ 3 * negNormBaseConst d * coarseGrainingP2Const d * (216 * s⁻¹ ^ 4 * coarseGrainingEnergyTerm Q a (scalarComparator hsigma0) (s / 3) w.u + 1944 * s⁻¹ ^ 6 * coarseGrainingForceTerm Q a (scalarComparator hsigma0) (s / 3) s g)

The interior L² estimate at the slot (3s/4, s/3, s, 0).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGraining_l2_thirdSlot_le_of_isForcedEquation {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {sigma0 : ℝ} (hsigma0 : 0 < sigma0) {u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : HCPolySupport.Book.Ch03.IsForcedEquation Q a u g) (hgL2 : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet Q) g) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hg : HCPolySupport.Book.Ch03.ForceBesovRegularity Q s g) : sigma0 * (HCPolySupport.cubeBesovScaleWeight 1 Q * HCPolySupport.cubeLpNorm Q 2 fun (x : HCPolySupport.Vec d) => (replacementDefect (scalarComparator hsigma0) u hgL2).toFun x) ≤ 3 * negNormBaseConst d * coarseGrainingP2Const d * (216 * s⁻¹ ^ 4 * coarseGrainingEnergyTerm Q a (scalarComparator hsigma0) (s / 3) u + 1944 * s⁻¹ ^ 6 * coarseGrainingForceTerm Q a (scalarComparator hsigma0) (s / 3) s g)

The re-cut slot estimate, entered at the equation alone.

4. The harmonic display at the re-cut slot

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGraining_l2_thirdSlot_harmonic_le {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {sigma0 : ℝ} (hsigma0 : 0 < sigma0) {u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : HCPolySupport.Book.Ch03.IsForcedEquation Q a u g) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hg : HCPolySupport.Book.Ch03.ForceBesovRegularity Q s g) : sigma0 * (HCPolySupport.cubeBesovScaleWeight 1 Q * HCPolySupport.cubeLpNorm Q 2 fun (x : HCPolySupport.Vec d) => (harmonicCorrector (scalarComparator hsigma0) u).toFun x) ≤ 3 * negNormBaseConst d * coarseGrainingP2Const d * (216 * s⁻¹ ^ 4 * coarseGrainingEnergyTerm Q a (scalarComparator hsigma0) (s / 3) u + 1944 * s⁻¹ ^ 6 * coarseGrainingForceTerm Q a (scalarComparator hsigma0) (s / 3) s g) + 2 * negNormBaseConst d * negativeToL2Factor s * (√↑(Fintype.card (Fin d)) * HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q s g)

5. The interior clause's left-hand side, at the re-based family

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_sub_weaklyHarmonic_le_coarseGraining_rebased {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L : ℤ) (omega : Section3.Cutoff.CutoffSample d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) {n m : ℤ} {x z : HCPolySupport.Vec d} (hsub : HCPolySupport.translateSet x (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (hsol : Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u hdat g) (hgL2 : MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) (hgW : 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))) (hharm : Support.IsWeaklyHarmonicOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) v) (hval : ∀ (y : HCPolySupport.Vec d), v.toFun y = u.toFun y - w.toFun y) (hgrad : ∀ (y : HCPolySupport.Vec d), v.grad y = u.grad y - w.grad y) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) : sigma0 * (HCPolySupport.cubeBesovScaleWeight 1 (HCPolySupport.originCube d n) * (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) ≤ 3 * negNormBaseConst d * coarseGrainingP2Const d * (216 * s⁻¹ ^ 4 * coarseGrainingEnergyTerm (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 2) x z omega) (scalarComparator hsigma0) (s / 3) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hsub)) + 1944 * s⁻¹ ^ 6 * coarseGrainingForceTerm (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 2) x z omega) (scalarComparator hsigma0) (s / 3) s fun (y : HCPolySupport.Vec d) => -g (y + x)) + interiorCorrectionConst d * s.rpow (-(1 / 2)) * Real.rpow 3 (s * ↑n) * (Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) s g).toReal

The x-frame composition at the re-based family and the re-cut slot.

• the slot index r = s/3 (§2--§4),

so that both right-hand coarse-graining objects are read at the index s/6, which is exactly the index the proved off-grid cap delivers.