PrincipalResponseMomentsCompose #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: sub-step (iv) of the principal response, composing the two moments #
This module supplies the interface between the two moment displays and the
Hoelder/budget chain of PrincipalResponseLegsHolder and
PrincipalResponseLegsBudget. Nothing new is estimated: what is supplied is
the pointwise domination X <= B . V^2 in the exact shape the chain
consumes, with B the operator norm and V the normalized load length.
Main results #
sq_sqrt_annealedSqrtNormSq-- the square undoes the square root of the Hoelder split.blockVecDot_coarseBlockMatrix_le_operatorEnvelope-- the pointwise domination itself.
The load length #
theorem
Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sq_sqrt_annealedSqrtNormSq
{d : ℕ}
(sigma : Observable.PositiveScalar)
(Y : HCPolySupport.BlockVec d)
:
| bfAhom^{1/2} P | squared is | bfAhom^{1/2} P |^2: the square root taken
is undone by the square of the Hoelder split.
theorem
Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_coarseBlockMatrix_le_operatorEnvelope
{d : ℕ}
[NeZero d]
(sigma : Observable.PositiveScalar)
(R : HCPolySupport.TriadicCube d)
(a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d)
{s : ℝ}
{q : HCPolySupport.Book.Ch02.MultiscaleExponent}
(hs : 0 < s)
(hq : q.IsAdmissible)
(Y : HCPolySupport.BlockVec d)
:
HCPolySupport.blockVecDot Y
(HCPolySupport.blockMatVecMul
(HCPolySupport.Book.Ch02.coarseBlockMatrix (HCPolySupport.Book.Ch02.cubeDomain R) (a.coeffOn R)) Y) ≤ 2 * ((↑sigma)⁻¹ * HCPolySupport.Book.Ch02.LambdaSq R s q a + ↑sigma * (HCPolySupport.Book.Ch02.lambdaSq R s q a)⁻¹) * √(annealedSqrtNormSq sigma Y) ^ 2
The pointwise domination, in the shape the Hoelder split consumes. With
V := | bfAhom^{1/2} Y |, the normalized load length,