StepSevenEndPoincare

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

t.regularity Step 7d, part one: e.cg.Poincare.with.rhs.grad.applied

The target

  3^{-m'}‖∇u‖_{B^{-1}_{2,2}(z'+□_{m'-1})} 1_{𝒢(m',z;·,·)}
    ≤ C σ_{m'}^{-1/2} ν^{1/2}‖∇u‖_{L²(z'+□_{m'-1})}
        + C σ_{m'}^{-1} 3^{sm'}[𝐠]_{H^s(z'+□_{m'-1})}
    ≤ C 3^{(1/2)(d+γ)(m-m')} ( σ_m^{-1/2} ν^{1/2}‖∇u‖_{L²(□_m)}
        + σ_m^{-1} 3^{sm}[𝐠]_{H^s(□_m)} ) .

Two independent inequalities, proved here as two independent theorems on the S the display names (/ discipline), plus the C₁-largeness accounting that absorbs the transport exponent.

The scalar carriers

• besov — 3^{-m'}‖∇u‖_{B^{-1}_{2,2}(z'+□_{m'-1})}·1_{𝒢}, the left-hand side.
• lamInv — λ_{1/4,2}^{-1}(z+□_{m'};𝐚_{L,m'})·1_{𝒢}, the coarse-graining lemma's ellipticity weight at the lattice centre.
• shomMpInv / shomMinv — σ_{m'}^{-1} and σ_m^{-1}.
• gradLoc / gradM — ν^{1/2}‖∇u‖_{L²} on z'+□_{m'-1} and on □_m: for 𝐚_L = ν I + 𝐤 with 𝐤 antisymmetric this is the symmetric coefficient energy.
• dataLoc / dataM — 3^{sm'}[𝐠]_{H^s(z'+□_{m'-1})} and 3^{sm}[𝐠]_{H^s(□_m)}.
• Kg, Kd, Ks — the three transport factors of the second inequality: the L² volume ratio, the H^s window restriction, and the σ comparison.

The conditional inputs, and nothing else

• hcg — l.coarse.graining.RHS applied on z'+□_{m'-1} at the good scale m', in the ellipticity-weighted form the display quotes: besov ≤ C(√lamInv·gradLoc) + C(lamInv·dataLoc).
• hlambda — e.lambda.stability.applied, the lower leg at k' = m': λ_{1/4,2}^{-1}(z+□_{m'};𝐚_{L,m'})1_{𝒢} ≤ C σ_{m'}^{-1}. This is the first conjunct of the printed display, in exactly the rendering discipline the Step-7c hlambda uses for the second conjunct (lattice centre, indicator absorbed, one scalar inequality weight ≤ C · σ-power), so that a single future Step-7b theorem discharges both.

The three transport ingredients hgrad, hdata, hshom are not conditional inputs of this module: they are the caller's own geometry/σ facts, and each is supplied unconditionally elsewhere in the development (normalizedL2On_le_of_subset for Kg, the window restriction for Kd, and sigmaBar_le_rpow_mul_sigmaBar_of_inductionState for Ks).

The C₁-largeness accounting (the transport exponent)

The transport exponent (1/2)(d+γ)(m-m') is absorbed into 3^{(1/4)(1-α)(m-n)} by the third and fourth C₁-largeness conditions. The C₁ floor already carries the exact clause: stepOneC1's second maximand is 2d+2, which reads as 2(d+γ) ≤ C₁ for γ ≤ 1 — the pin whose docstring names this transport. So

  (1/2)(d+γ)(m-m') ≤ (1/2)(d+γ)·3 + 1/4 + (1/4)(1-α)(m-n)

with NO new largeness demand: the quarter-bound on (d+γ)/(2C₁) needs exactly 2d+2 ≤ C₁ and γ ≤ 1. Nothing was enlarged.

References

• ABK26, e.cg.Poincare.with.rhs.grad.applied.
• ABK26, graining.; e.lambda.stability.applied.

2. The first inequality: the coarse-graining Poincaré after hlambda

theorem Algsuperdiff.Section4.Provider.Regularity.cgPoincareShom_compose {Ccg Clam lamInv shomInv besov gradLoc dataLoc : ℝ} (hCcg : 0 ≤ Ccg) (hClam : 0 ≤ Clam) (hshomInv : 0 ≤ shomInv) (hgradLoc : 0 ≤ gradLoc) (hdataLoc : 0 ≤ dataLoc) (hcg : besov ≤ Ccg * (√lamInv * gradLoc) + Ccg * (lamInv * dataLoc)) (hlambda : lamInv ≤ Clam * shomInv) : besov ≤ Ccg * (√Clam + Clam) * (√shomInv * gradLoc) + Ccg * (√Clam + Clam) * (shomInv * dataLoc)

e.cg.Poincare.with.rhs.grad.applied, first inequality, on abstract reals.

l.coarse.graining.RHS produces the Besov left-hand side against the weight λ^{-1} (square root on the gradient leg, full power on the data leg); e.lambda.stability.applied replaces λ^{-1} by C σ_{m'}^{-1}. The two legs are then carried by the single constant Ccg(√Clam + Clam).

3. The second inequality: the transport to □_m

theorem Algsuperdiff.Section4.Provider.Regularity.cgPoincareTransport_compose {Kg Kd Ks gradLoc dataLoc gradM dataM shomMpInv shomMinv : ℝ} (hKs : 0 ≤ Ks) (hshomMinv : 0 ≤ shomMinv) (hgradLoc : 0 ≤ gradLoc) (hdataLoc : 0 ≤ dataLoc) (hgrad : gradLoc ≤ Kg * gradM) (hdata : dataLoc ≤ Kd * dataM) (hshom : shomMpInv ≤ Ks * shomMinv) : √shomMpInv * gradLoc + shomMpInv * dataLoc ≤ √Ks * Kg * (√shomMinv * gradM) + Ks * Kd * (shomMinv * dataM)

e.cg.Poincare.with.rhs.grad.applied, second inequality, on abstract reals: the three transports

  gradLoc ≤ Kg · gradM ,   dataLoc ≤ Kd · dataM ,   σ_{m'}^{-1} ≤ Ks · σ_m^{-1}

(the L² volume ratio, the H^s window restriction, and the σ comparison) carry the weighted bracket from z'+□_{m'-1} to □_m at the two factors √Ks·Kg and Ks·Kd.

4. The display

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCgPoincareApplied {Ccg Clam Kg Kd Ks Ktr lamInv shomMpInv shomMinv besov gradLoc dataLoc gradM dataM : ℝ} (hCcg : 0 ≤ Ccg) (hClam : 0 ≤ Clam) (hKs : 0 ≤ Ks) (hshomMpInv : 0 ≤ shomMpInv) (hshomMinv : 0 ≤ shomMinv) (hgradLoc : 0 ≤ gradLoc) (hdataLoc : 0 ≤ dataLoc) (hgradM : 0 ≤ gradM) (hdataM : 0 ≤ dataM) (hcg : besov ≤ Ccg * (√lamInv * gradLoc) + Ccg * (lamInv * dataLoc)) (hlambda : lamInv ≤ Clam * shomMpInv) (hgrad : gradLoc ≤ Kg * gradM) (hdata : dataLoc ≤ Kd * dataM) (hshom : shomMpInv ≤ Ks * shomMinv) (hKgb : √Ks * Kg ≤ Ktr) (hKdb : Ks * Kd ≤ Ktr) : besov ≤ Ccg * (√Clam + Clam) * Ktr * (√shomMinv * gradM + shomMinv * dataM)

e.cg.Poincare.with.rhs.grad.applied, as printed.

The two inequalities composed, at a single transport factor Ktr dominating both legs' factors:

  besov ≤ Ccg(√Clam + Clam) · Ktr · ( √σ_m^{-1}·gradM + σ_m^{-1}·dataM ) .

hcg and hlambda are the only conditional inputs; hgrad, hdata, hshom, hKgb, hKdb are the caller's own transport data.