CrudeBound #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
A crude uniform bound for the coarse gauge along the perturbation path #
Source: ABK26. The self-referential bootstrap of Provider.Lambda.Bootstrap
runs the ratio engine on a grid whose mesh is chosen from some finite
a-priori bound for the coarse gauge along the segment. This module supplies
such a bound.
The microscopic gauge is confined to the mesh #
The bound produced here involves the microscopic ellipticity constant
a.lam of the base coefficient, times a dimensional factor. By the design of
Provider.Lambda.Bootstrap this quantity enters only through the choice of
the grid mesh and is entirely absent from the conclusions of
le_riccati_of_ratio_engine and le_one_add_four_mul_of_ratio_engine.
The mechanism #
The frozen perturbation perturbCoeffOn U a h t is defined with lam:= a.lam,
uniformly in t, because h is skew and therefore does not change the
symmetric part. CoarseGraining's deterministic uniform bound
maxDescendantSigmaStarInvNormAtScale Q (Q.scale - n) A ≤ 4 d lam⁻¹
therefore holds along the whole segment with a t-independent constant, and
summing the geometric weights (which have total mass one) turns it into a bound
for lambda_{s,q}^{-1}(Q; ·).
Every declaration is an internal helper for the Section 2.4 sensitivity providers.
A compatible family that remembers the root ellipticity constants #
The pointwise representative of a root coefficient is elliptic at every point, with the constants of the coefficient.
The constant CoarseGraining triadic family built from the pointwise
representative of a root coefficient. Unlike the anonymous family produced by
exists_compatibleTriadicCoeffFamily, this one exposes its ellipticity
constants: they are those of the root coefficient itself.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The deterministic uniform one-cube bound #
The uniform descendant bound. For any CoarseGraining triadic family, every
descendant maximum of |sigma_*^{-1}| is bounded by 4 d times the inverse of
the root microscopic ellipticity constant of the family.
Aggregation of a uniform one-cube bound #
Uniform aggregation. A uniform bound on all descendant maxima of
|sigma_*^{-1}| transfers verbatim to lambda_{s,q}^{-1} at every finite
admissible exponent. This mirrors the ratio aggregation of
Multiscale.DescendantRatio, with a constant in place of a ratio.
The crude bound #
The crude uniform path-gauge bound.
Along the whole segment a + t h, t ∈ [0,1], the frozen coarse gauge
lambda_{3/8,2}^{-1} is bounded by the single constant 4 d a.lam⁻¹.
The microscopic constant a.lam appears here and only here; by the design of
Provider.Lambda.Bootstrap it is consumed by the choice of the compounding mesh
and never enters the conclusion.