StepSevenWireCgMatching #

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

`t.regularity` Step 7d: matching `l.coarse.graining.RHS` to the §4.4 data #

The gap this module closes #

e.cg.Poincare.with.rhs.grad.applied is proved with its first conditional input named hcg:

  besov ≤ Ccg · (√lamInv · gradLoc) + Ccg · (lamInv · dataLoc) .

Here exists_stepSevenCgPoincareInput produces the hcg shape verbatim, and composing it with hlambda gives the display's first inequality. hcg is therefore no longer a conditional input of the Step-7d chain.

The carrier match, binder by binder #

  scaleNormalizedNegativeBesovVectorNorm Q s (.finite 2) (∇u)
    ≤ C s^{-3/2} λ_{s/2,2}^{-1/2}(Q;a) ‖∇u‖_{energy}
      + C s^{-3} λ_{s/2,2}^{-1}(Q;a) [𝐠]_{B^s_{2,2}(Q)} ,

which is the printed e.cg.Poincare.with.rhs.grad character for character: the s^{-3/2} λ^{-1/2} / s^{-3} λ^{-1} pair, the note-normalized 3^{-sm}‖∇u‖_{B^{-s}_{2,2}} on the left, and 3^{sm}[𝐠]_{H^s} on the right.

besov ⇝ scaleNormalizedNegativeBesovVectorNorm Q s (.finite 2) (∇u).
lamInv ⇝ stepSevenCgLamInv Q a s = λ_{s/2,2}^{-1}(Q;𝐚), defined here as the rpow-(-1) power of Ch02.lambdaSq, i.e. literally the second leg's own ellipticity factor. sqrt_stepSevenCgLamInv_eq proves that its square root is literally the first leg's poincareLowerEllipticityFactor, so the two legs are weighted by one object — the object a future Step-7b theorem (e.lambda.stability.applied) must bound by C σ_{m'}^{-1}. This is the carrier that the Step-7c and Step-7d hlambda slots both consume, so one Step-7b theorem discharges both.
dataLoc ⇝ scaleNormalizedPositiveBesovVectorSeminormTwo Q s g.
Ccg ⇝ C · s^{-3}: the two printed s-powers are collapsed to the larger one, which is legitimate exactly because s ≤ 1 (rpow_neg_three_halves_le_rpow_neg_three). Nothing else is enlarged.

Off-grid: the §4.4 window `z'+□_{m'-1}` #

z'+□_{m'-1} is not a TriadicCube — z' is the clamped, off-lattice centre. The instantiation route is the convention translate the sample, never the cube: the theorems below are applied at Q := originCube d (m'-1), which is a TriadicCube, with the translated sample

  a ↦ 𝐚_{L,m'}(z'+·) ,   u ↦ u(z'+·) ,   g ↦ 𝐠(z'+·) ,

whose forced-equation binder is the isForcedEquation_fluxCorrectedCoeffFamily_of_isDirichletSolutionOn route and whose L² carriers transport by normalizedL2SqOnSet_translateSet / normalizedSetAverage_translateSet. No new analysis is used and no statement is transported here: the §4.4 scalars are the translated-frame objects, exactly as the Step-7c matching leaves its own carrier bridge to the caller.

References #

ABK26, l.coarse.graining.RHS.
ABK26, e.cg.Poincare.with.rhs.grad.applied.
CoarseGraining, Homogenization/Book/Ch03/Theorems/CoarsePoincare.lean.

1. The ellipticity carrier shared by the two legs #

source

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenCgLamInv {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (s : ℝ) :

ℝ

The coarse-grained ellipticity weight of l.coarse.graining.RHS: λ_{s/2,2}^{-1}(Q;𝐚), the object the printed display carries with a square root on the gradient leg and in full on the data leg. This is the lamInv slot's hcg, and the object e.lambda.stability.applied must bound by C σ^{-1}. It is coarse-grained: no bare ellipticity of 𝐚 occurs.

Equations

Algsuperdiff.Section4.Provider.Regularity.stepSevenCgLamInv Q a s = (HCPolySupport.Book.Ch02.lambdaSq Q (s / 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a).rpow (-1)

Instances For

source

theorem Algsuperdiff.Section4.Provider.Regularity.sqrt_stepSevenCgLamInv_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {s : ℝ} (hs : 0 < s) :

√(stepSevenCgLamInv Q a s) = HCPolySupport.Book.Ch03.poincareLowerEllipticityFactor Q a (s / 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2)

The two legs carry ONE ellipticity object. The gradient leg's poincareLowerEllipticityFactor Q a (s/2) (.finite 2) = λ_{s/2,2}^{-1/2} is the square root of the data leg's stepSevenCgLamInv Q a s = λ_{s/2,2}^{-1}. This is what lets's hlambda be a SINGLE scalar inequality.

2. The `s`-power collapse #

source

theorem Algsuperdiff.Section4.Provider.Regularity.rpow_neg_three_halves_le_rpow_neg_three {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) :

s.rpow (-(3 / 2)) ≤ s.rpow (-3)

s^{-3/2} ≤ s^{-3} for 0 < s ≤ 1: the two printed prefactors of l.coarse.graining.RHS collapse to the larger one, which is what lets the hcg slot carry a single Ccg.

source

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenCgPoincareInput (d : ℕ) [NeZero d] :

l.coarse.graining.RHS, matched to the hcg slot.

For every triadic cube Q, every coefficient family 𝐚, every exponent s ∈ (0,1), every forcing 𝐠 ∈ H^s(Q) and every H¹(Q) solution of -∇·𝐚∇u = ∇·𝐠,

  3^{-sm}‖∇u‖_{B^{-s}_{2,2}(Q)}
    ≤ (C s^{-3})·(√(λ_{s/2,2}^{-1})·‖∇u‖_{energy})
      + (C s^{-3})·(λ_{s/2,2}^{-1}·3^{sm}[𝐠]_{H^s(Q)}) ,

which is stepSevenCgPoincareApplied's hcg hypothesis verbatim at Ccg = C s^{-3} and lamInv = stepSevenCgLamInv Q a s. Unconditional beyond the printed lemma's own binders.

source

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenCgS :

ℝ

The coarse-graining exponent matched to the first regularity step.

Equations