CoarseGrainingL2Interior

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

The interior L² homogenization estimate

What is proved

ABK26's Step 1 runs the chain

  ‖u - v‖_{L²(x+□_n)}  ≤  C 3^{(1-s/2)n} ‖∇u - ∇v‖_{H_hat^{-s/2}(x+□_n)}
                        ≤  C 3^{n} σ^{-1} · (coarse-graining right-hand side) ,

the second step being e.homogenization.L2.interior, i.e. p.general.coarse.graining at p = 2, m = n, flux term discarded.

coarseGraining_scaled_l2_le below is that chain in one inequality, at CoarseGraining's carriers and with CoarseGraining's own right-hand side; and the §4.3 slot reads it with every constant explicit. The comparator σ₀ stays on the left, exactly as the printed display writes it (3^{-sn/2} σ_n ‖∇u − ∇v‖); dividing by σ₀ is left to the consumer.

Note that the scale factor is 3^{-Q.scale} on the left and carries no s-dependence: CoarseGraining's negative Besov seminorm is scale-normalized, so the printed 3^{(1-s/2)n} and the exponent choice below differ only inside the normalization and cancel. Consequently the comparison exponent enters the final bound only through the factor s_prop⁻¹.

Honest exponents (reported)

No γ-exponent is touched anywhere. See CoarseGrainingEnvelope.lean for the term-by-term account.

What this leg does NOT do

• The window here is a triadic cube Q. §4.3 applies the estimate on the off-grid cube x+□_n; under the development's A4 convention that window is the origin cube □_n read in the x-translated frame, so the statement below is the right one — but the resulting error 𝓔(□_n; ã, σ) then lives in the x-frame while the anchor's right-hand side carries 𝓔(□_{n+2}; ã, σ) in the z-frame. Nothing here assumes it.
• Consequently the good-event caps (GoodEventCaps.lean) are not applied here: they are stated at □_{n+2} in the z-frame.
• The H¹₀ witness and the pointwise gradient identity are taken as given — they are the anchor's own binders (v = u - w, ∇v = ∇u - ∇w).
• w.v is the auxiliary solution v_g of the forced constant-coefficient problem, not the harmonic replacement v; the passage v_g → v is the forcing correction, carried out in ReplacementDatumHarmonic.lean.

References

• ABK26, l.harmonic.approximation.good.scales.
• ABK26, p.general.coarse.graining.

1. The composed estimate

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGraining_scaled_l2_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) {t r r₂ : ℝ} {j : ℕ} (ht : 0 < t) (ht1 : t < 1 / 2) (hr : 0 < r) (hrt : r < t) (hr₂ : r ≤ r₂) (hg : HCPolySupport.Book.Ch03.ForceBesovRegularity Q r₂ g) : sigma0 * (HCPolySupport.cubeBesovScaleWeight 1 Q * HCPolySupport.cubeLpNorm Q 2 fun (x : HCPolySupport.Vec d) => z.toFun x) ≤ negNormBaseConst d * √(1 - Real.rpow 3 (-2 * (1 / 2 - t)))⁻¹ * HCPolySupport.Book.Ch03.generalCoarseGrainingL2TwoExponentRHS (coarseGrainingP2Const d) Q a (scalarComparator hsigma0) (2 * t) r r₂ j g w.u

The interior L² homogenization estimate.

For a coarse-graining datum w on the triadic cube Q with scalar background σ₀ Id, and an H¹₀ function z whose gradient is ∇u − ∇v:

  σ₀ · 3^{-Q.scale} ‖z‖_{L²(Q)}
      ≤ C(d) · sqrt((1 - 3^{-2(1/2 - t)})⁻¹)
          · generalCoarseGrainingL2TwoExponentRHS (coarseGrainingP2Const d) …

at comparison exponent 2t. This is the negative-norm-to-L² step composed with the interior estimate, with the flux summand discarded.

2. The analytic tail factor at the slot

theorem Algsuperdiff.Section4.Provider.ExcessDecay.negNormSqrtFactor_slot_le_three {s : ℝ} (hs1 : s ≤ 1) : √(1 - Real.rpow 3 (-2 * (1 / 2 - 3 * s / 8)))⁻¹ ≤ 3

The Besov-tail factor at the slot exponent t = 3s/8 is at most 3.