GridDominationEndpoint #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
hgrid at the endpoint q = infinity: the direct, pole-free route #
The frozen display Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds
quantifies over every admissible exponent, and its deterministic lower profile
at the endpoint is the bare constant
(LowerLegProfile.lowerEllipticityProfile_infinity: lowerEllipticityProfile C gamma s infinity = C) --- no pole. That is not an accident of the print:
at q = infinity the coarse-grained ellipticity constant is a supremum, not
a series (e.coarse.grained.ellipticity.infty),
lambda_{s,infinity}(cu_m;a)^{-1} = sup_{n >= 0} 3^{-2 s n} max_{z in 3^{m-n} Zd cap cu_m}
|sigma_*^{-1}(z + cu_{m-n}; a)| ,
and a supremum of Cdet + (lane at gap n) is at most Cdet + sup_n (lane):
the deterministic constant is not multiplied by the number of scales. This
module proves that endpoint at this repository's carriers.
Why this is not the finite-q statement with q sent to infinity #
Provider/CoarseEllipticity/GridDomination.lean (at q = 2) and
.../GridDominationAllQ.lean (at finite q >= 2) both end in the consumers'
series shape X <= sum_k mass * gridWeight rho k * G k, whose deterministic slot
is Cdet * (mass * rho^{-1}). Routing the endpoint through that shape is
possible --- the supremum is bounded by the series, since every term of the
series is nonnegative --- but it is lossy in exactly the wrong place: it
reintroduces the factor (2s)^{-1} that the endpoint profile does not have.
The theorems below therefore do not go through gridWeight at all. What
they deliver is the endpoint's own domination
lambda_{s,infinity}^{-1}(cu_m; a_L) * scaling <= V(omega) for every omega, every L >= L0,
from a caller-supplied majorant V of the individual weighted grid maxima.
Fed with V = Cdet + (summed lane), this is precisely the two-slot family
split that LowerLeg.isLowerIntegerFamilyOrlicz_of_familySplit consumes, with
the deterministic slot equal to Cdet --- the frozen endpoint profile, with no
pole and no fold.
What is proved here #
lambdaSqCoeffField_inv_infinity_eq_sSup,LambdaSqCoeffField_infinity_eq_sSup--- the endpoint constants at the Chapter 4 ambient coefficient field are the source's suprema, non-elliptic branch included (there the supremum is that of{0}).lambdaSqCoeffField_inv_infinity_le_of_foralland the two scaled formslambdaSqCoeffField_inv_infinity_mul_le_of_forall,LambdaSqCoeffField_infinity_mul_le_of_forall--- the endpoint domination from a majorant of the individual weighted maxima.cutoffLowerEllipticityInvLiteral_infinity_mul_le_of_forall,cutoffUpperEllipticityLiteral_infinity_mul_le_of_forall--- the same at the Section 3 literal observables.cutoffLowerEllipticityInv_infinity_mul_forall_le,cutoffUpperEllipticity_infinity_mul_le--- the same at the exported observables, at every sample point (the body swap), in the two legs' own shapes:forall omega, forall L >= L0for the lower family andforall omegaat the single cutoff index for the upper.
What is not claimed here #
No block estimate, no e.maxy.bound lift, no base case; nothing below asserts
that either leg's payload is satisfiable. In particular the majorant V is the
caller's: this module does not construct it, and the per-scale split that would
produce it (p.bfA.multiscalebound at the endpoint) is untouched.
References #
- ABK26,
e.coarse.grained.ellipticity.infty, (the endpoint is the supremum, and is theq -> infinitylimit of the finite definition);p.cg.ellipticity.bounds, statement, proof. Provider/CoarseEllipticity/GridDominationAllQ.lean(the finite branch2 <= q),.../GridDomination.lean(the ruledq = 2),.../LowerLegProfile.lean(lowerEllipticityProfile_infinity),.../LowerLeg.lean(isLowerIntegerFamilyOrlicz_of_familySplit, the endpoint's consumer).- CoarseGraining:
Book.Ch02.lambdaSqInfinity,Book.Ch02.LambdaSqInfinity(the source definitions) andBook.Ch02.lambdaSqInfinity_denominator_valueSet_bddAbove(the boundedness that makes the supremum a real number --- not needed by thecsSup_leroute below, which needs only nonemptiness).
1. A scaled supremum bound #
2. The endpoint constants at the Chapter 4 ambient coefficient field #
The endpoint lower constant is the source's supremum, at the Chapter 4
ambient coefficient field, non-elliptic branch included (there both sides are
the supremum of {0}, i.e. 0). Unconditional in s.
The endpoint upper constant is the source's supremum, at the Chapter 4 ambient coefficient field, non-elliptic branch included.
3. The endpoint domination from a majorant of the individual maxima #
The endpoint lower domination. Any bound on the individual weighted grid
maxima bounds lambda_{s,infinity}^{-1} itself. No summability, no fold, and no
s-pole: the gap-0 scale is one of the elements of the supremum.
The scaled form of lambdaSqCoeffField_inv_infinity_le_of_forall.
The upper endpoint counterpart of
lambdaSqCoeffField_inv_infinity_mul_le_of_forall, in the scaled form.
4. The endpoint at the Section 3 literal observables #
The endpoint lower domination at the Section 3 literal observable, at the centered cube.
The endpoint upper domination at the Section 3 literal observable.
5. The endpoint at the exported observables, in the legs' own shapes #
The lower leg's endpoint domination. Verbatim the hdom binder of
LowerLeg.isLowerIntegerFamilyOrlicz_of_familySplit at
X L omega = cutoffLowerEllipticityInv M m L s hs q omega * scaling, once the
caller takes V omega = Ydet omega + Y omega.
The deterministic slot the caller then gets is whatever V's deterministic part
is: at V = Cdet + (summed lane) it is Cdet itself, which is exactly the
frozen endpoint profile lowerEllipticityProfile Clow gamma s infinity = Clow.
No (2s)^{-1} appears anywhere, because no series is formed.
The upper leg's endpoint domination, at the single cutoff index the upper
leg reads its target at. Verbatim the domination slot of the upper payload once
the caller takes V omega = Udet omega + Uone omega + Utail omega.