CoarseGrainingEnvelope #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The s-envelope of the coarse-graining right-hand side at the §4.3 slot #
The slot #
ABK26's e.homogenization.L2.interior is p.general.coarse.graining read at
p = 2 and m = n — i.e. at depth j = 0 — with the manuscript exponents
(s_prop, s_1, s_2) = (s/2, s/4, s).
CoarseGraining's package asks r < s_prop / 2 where the printed proposition
asks only s_1 < s_prop. Keeping the printed error index s_1 = s/4 (the
index the q = 1 ← q = 2 comparison converts into the good event's own s/8)
therefore forces the comparison exponent above the printed s/2.
s_prop := 3s/4 , r := s/4 , r₂ := s , j := 0 ,
which satisfies every CoarseGraining hypothesis on the whole anchor range s ∈ (0,1] (3s/4 < 1 even at the endpoint s = 1), keeps the printed
𝓔_{s/4,∞,1}, and costs only the harmless factor 4/3 on the s_prop^{-1}
prefactor: the comparison exponent enters CoarseGraining's right-hand side
only through s_prop⁻¹.
The honest envelope (reported, not hidden) #
The s-powers proved below are
| term | printed | proved here |
|---|---|---|
𝓔 · ν^{1/2}‖∇u‖ | C s^{-3/2} | (1024/3) s^{-4} |
forcing [g]_{H^s} | C s^{-11/2} | (16384/3) s^{-6} |
Both are weaker than the printed envelopes, so nothing here may be presented
as the printed display. Two of the three forcing summands land on the printed
s^{-11/2} exactly; only the |a₀| λ^{-1}_{r/2,2} summand costs s^{-6}.
The forcing bracket #
The printed proposition writes the forcing prefactor as (1 + 𝓔²_{s_1/2,∞,2});
CoarseGraining writes it through the coarse-grained ellipticity factors. Both
are capped by C(d) on the good event 𝒢 — the first by
e.good.set.giveth.v2, the second by e.bound.Lambdas.by.Es.v2 (the
l.mathcal.E.to.Lambdas leg proved in LambdaCaps.lean/GoodEventCaps.lean)
— so the two forms are interchangeable exactly where §4.3 uses them.
coarseGrainingForceBracket below is CoarseGraining's form, carried
explicitly.
References #
- ABK26,
p.general.coarse.graining. - ABK26,
e.homogenization.L2.interior.
1. The two development-facing right-hand terms #
The energy term of e.homogenization.L2.interior, at depth 0:
|a₀|^{1/2} 𝓔_{r,∞,1}(Q; a, a₀) ‖∇u‖_{a,L²(Q)}. For the ABK operator
a_L = ν Id + κ_L with κ_L antisymmetric, the coefficient-energy norm on the
right is ν^{1/2}‖∇u‖_{L²}, which is what the display prints.
Equations
- One or more equations did not get rendered due to their size.
Instances For
CoarseGraining's forcing bracket, the replacement for the printed (1 + 𝓔²_{s_1/2,∞,2}): it is built from the coarse-grained ellipticity factors
λ^{-1/2}_{r/2,2}, Λ^{1/2}_{r/2,2} and λ^{-1}_{r/2,2}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forcing term of e.homogenization.L2.interior, at depth 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
2. Nonnegativity #
Nonnegativity of the coarse-graining homogenization error at depth j.
3. Depth-zero weights #
4. The depth-zero right-hand side, unpacked #
CoarseGraining's right-hand side at depth 0, with its three forcing summands
displayed and their individual r-powers intact.