InteriorGlue

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

The interior clause's glue: the frame containment, the s-envelope of the

correction, and the correction leg in the anchor's own carriers

Three of the four glue items the interior-clause assembly was priced with.

• the frame containment (translateSet_cubeSet_subset_of_anchorGeometry) — the frozen theorem's geometry binder gives the half-open containment `(x−z)
  • □n ⊆ □{n+2} that the proved off-grid stability cap (ae_offGridErrorFunctional_le_fluxCorrectedErrorFunctionalAtRoot) consumes. The open containment is CaccioppoliInteriorGeometry's; the half-open one is proved here directly from the two coordinate windows — the arithmetic slack is a factor 9/4` per coordinate, so no boundary case arises.
• , the s-envelope of the correction factor (negativeToL2Factor_le_rpow_neg_half) — (1 − 3^{−s})^{−1/2} ≤ √(3/2)·s^{−1/2} on (0,1], through the chord bound 1 − 3^{−s} ≥ 2s/3 (convexity of exp, no nlinarith, no numerical rpow evaluation).
• + composed (correctionLeg_le_anchorGagliardo) — the correction summand of the harmonic replacement's coarse-graining slot, written in the frozen theorem's own Gagliardo carrier on the translated window w + □_n, at the explicit d-only constant interiorCorrectionConst d and the honest s-power s^{−1/2}.

The s-power of the correction leg, against the anchor's display

Dividing the harmonic display by its own prefactor σ·3^{−n} turns the bound below into

  σ^{-1} · interiorCorrectionConst d · s^{-1/2} · 3^{(1+s)n} · [g]_{H^s(w+□_n)} ,

which is exactly the shape of the frozen statement's second interior summand C s^{-7} σ_n^{-1} 3^{(1+s)n} [g]_{H^s(W)}, with the s-power −1/2 in place of the printed −7: stronger than printed, and dominated by it on (0,1]. Nothing is claimed at the printed power here; the weakening is the assembly's arithmetic step.

References

• ABK26, l.harmonic.approximation.good.scales, (the geometry binder and the interior clause); the forcing correction.

1. The frame containment, in the half-open realization

theorem Algsuperdiff.Section4.Provider.ExcessDecay.translateSet_cubeSet_subset_of_anchorGeometry {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} (hsub : (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.translateSet (x - z) (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 2))

The anchor's geometry binder gives the half-open child-in-parent containment.

The proved off-grid stability cap is stated with translateSet w (cubeSet P) ⊆ cubeSet K — the half-open realizations, because the flux-corrected ellipticity envelope of the parent is available pointwise there. The frozen theorem supplies the open containment x + □_n ⊆ (z + □_{n+1}) ∩ □_m; the half-open one at the two-scale gap follows with room to spare (2·3^n against the available (9/2)·3^n).

2.: the honest s-envelope of the correction factor

theorem Algsuperdiff.Section4.Provider.ExcessDecay.two_mul_div_three_le_one_sub_three_rpow_neg {s : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : 2 * s / 3 ≤ 1 - Real.rpow 3 (-s)

The chord bound for 3^{−s}.

On [0,1], 1 − 3^{−s} ≥ (2/3)s: the convexity of exp against the chord through (0,1) and (1,1/3). Equality holds at both endpoints.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.negativeToL2Factor_le_rpow_neg_half {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : negativeToL2Factor s ≤ √(3 / 2) * s.rpow (-(1 / 2))

. The closed-form correction factor (1 − 3^{−s})^{−1/2} carried by ReplacementDatumHarmonic.negativeToL2Factor obeys the honest envelope √(3/2) · s^{−1/2} on (0,1].

3. +: the correction leg in the anchor's Gagliardo carrier

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.interiorCorrectionConst (d : ℕ) : ℝ

The d-only constant of the composed correction leg: 2 C_neg(d) √(3/2) √d · C_BG(d).

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.interiorCorrectionConst_pos (d : ℕ) [NeZero d] : 0 < interiorCorrectionConst d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.correctionLeg_le_anchorGagliardo {d : ℕ} [NeZero d] (n : ℤ) {w : HCPolySupport.Vec d} {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hL2 : MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => w + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))) (hW : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn ((fun (y : HCPolySupport.Vec d) => w + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))) : 2 * negNormBaseConst d * negativeToL2Factor s * (√↑(Fintype.card (Fin d)) * HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d n) s fun (y : HCPolySupport.Vec d) => -g (y + w)) ≤ interiorCorrectionConst d * s.rpow (-(1 / 2)) * Real.rpow 3 (s * ↑n) * (Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => w + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) s g).toReal

The composed correction leg +.

The correction summand of the harmonic display, read at the translated window w + □_n, is bounded by

  interiorCorrectionConst d · s^{-1/2} · 3^{s n} · [g]_{H^s(w+□_n)} ,

the frozen theorem's own Gagliardo object on the right. The s-power is the honest −1/2; the scale weight 3^{sn} is the manuscript's own; the constant is d-only and explicit. Both hypotheses are the anchor's clause-(iv) data, restricted to the window the leg is read at.