ReindexEllipticity

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

The child-frame coarse-graining objects at the slot n+3

InteriorEllipticity caps the two coarse-graining objects the interior chain carries at the child cube □_n — the q = 1 error at depth 0 and the ellipticity factors inside CoarseGraining's forcing bracket — at the proved slot n+2. The frozen statement reads them at the slot n+3, so this module re-runs the same three-step composition one scale up:

• the frame bridge (InteriorGlueFrame) is k-generic: homogenizationErrorOnCube_parentRebasedFamily_eq_offGrid takes the slot as a parameter and is an identity;
• the off-grid cap is ReindexSlot's, at the depth-3 factor 3^{3s/8} in place of the proved depth-2 factor 3^{s/4} — the only quantitative cost of this file, one extra 3^{s/8} ≤ 3^{1/8};
• the good event is the n+3 slot's own 𝒢(n+3, z; s/8, 1/2).

The last section re-runs the x-frame composition (InteriorEllipticitySlot.eLpNorm_sub_weaklyHarmonic_le_coarseGraining_rebased) at the re-based family of the n+3 flux increment.

References

• ABK26, e.mathcalE.stability.applied; e.bound.Lambdas.by.Es.v2; e.homogenization.L2.interior.

0. The comparator, in the two spellings

1. The frame bridge at the n+3 re-based family

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_homogenizationErrorOnCube_rebased_le_representative_addThree {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) (z : HCPolySupport.Vec d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (x : HCPolySupport.Vec 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) → HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d n) (s / 6) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 3) x z omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (n + 3))) ≤ √(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))

The child-frame 𝓔_{s/6,∞,2} at the n+3 family, against the anchor's representative.

2. The energy leg's 𝓔 factor, at the n+3 slot

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_coarseGrainingErrorAtDepth_rebased_le_representative_addThree {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) (z : HCPolySupport.Vec d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (x : HCPolySupport.Vec 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) → HCPolySupport.Book.Ch03.coarseGrainingHomogenizationErrorAtDepth (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 3) x z omega) (scalarComparator ⋯) (s / 3) 0 ≤ √(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))

The q = 1 error at depth 0 of the re-cut slot, at the anchor's representative.

3. The ellipticity ratio at the child frame, n+3 slot

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_ellipticityRatio_rebased_le_representative_addThree {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) (z : HCPolySupport.Vec d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (x : HCPolySupport.Vec 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) → max ((↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ * HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d n) (s / 6) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 3) x z omega)) (↑(Section3.Annealed.sigmaBar M (n + 3)) * (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d n) (s / 6) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 3) x z omega))⁻¹) ≤ 2 * ↑d * ((√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) ^ 2 + 1)

e.bound.Lambdas.by.Es.v2 at the child cube, in the child's own frame, at the n+3 slot.

4. CoarseGraining's forcing bracket at the child frame, n+3 slot

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_forceBracket_rebased_le_addThree {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) (z : HCPolySupport.Vec d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (x : HCPolySupport.Vec 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) → coarseGrainingForceBracket (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 3) x z omega) (scalarComparator ⋯) (s / 3) ≤ √(2 * ↑d * ((√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) ^ 2 + 1)) * (√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) + 2 * (2 * ↑d * ((√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) ^ 2 + 1))

The forcing bracket at the child frame, in terms of the anchor's representative. The comparator's scale σ_{n+3} cancels between the ellipticity factors and the matrix norm, exactly as at the proved slot.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_sub_weaklyHarmonic_le_coarseGraining_rebased_addThree {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 + 3) 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 + 3) 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 n+3 re-based family and the re-cut slot.

InteriorEllipticitySlot.eLpNorm_sub_weaklyHarmonic_le_coarseGraining_rebased with the family's slot moved from n+2 to n+3.