MultiscaleAbsorptionCore #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the absorption calculus of p.multiscale.estimate #
It carries nothing about the buckle's five terms; it carries only the three calculi the final absorption runs on.
1. The two-lane envelope calculus #
TwoLaneEnvelope mu X A1 A2 says that the nonnegative observable X is
dominated almost surely by a sum U + V of two nonnegative measurable
observables carrying the squared-display Orlicz profiles Gamma_1 and
Gamma_{1/4} at the scales A1, A2. It is the shape in which every one of
the buckle's five terms arrives, and the shape in which they add.
The two nonnegativity fields are carried by choice, not by necessity. This
module adds through Provider.Orlicz.isBigOWith_gammaSigma_add, whose
hypotheses include nonnegativity and measurability of both summands, and
carrying them in the package is cheaper than re-deriving them at each of the
five terms. The fields are inert downstream, but they are what force
isBigOWith_max_zero, the max-truncations of of_envelope /
of_isTwoTermBigOWith, and the hU0/hV0 plumbing.
The real obstruction to using Probability.IsTwoTermBigOWith as the carrier is
a.e. versus pointwise domination — that relation demands Measurable X and
forall omega, X omega <= Y omega + Z omega, while the buckle's five terms
dominate only almost surely — and not nonnegativity.
The calculus is closed under: weakening of both scales (mono_scales),
almost-sure domination (of_ae_le), addition (add), multiplication by a
nonnegative constant (const_mul), and it is generated by a single Gamma_1
tail (of_isBigOWith_gammaOne), by a deterministic constant (of_le_const),
by a raw measurable-and-tailed dominating pair (of_envelope) and by any
proved Probability.IsTwoTermBigOWith at the squared profiles
(of_isTwoTermBigOWith).
2. The square-root buckle's two amplitude identities #
sqrt_ordinaryLaneAmplitude and sqrt_rareLaneAmplitude evaluate the square
roots of the two normal forms
A1 = K1 . (s^{-1})^2 . (eps^2 E^2 cgamma) ,
A2 = K2 . (s^{-1})^4 . (eps^2 exp(-2 E^{-3} cgamma^{-1}))
in closed form. Under the eps^2 normalization of the squared display these
are exactly the two frozen amplitudes of
Frozen/Section3/MultiscaleEstimate.lean at Cms := sqrt K, and — this
is the point of the eps^2 normalization — the refinement clause is free:
sqrt A1 = sqrt K1 . eps . E . s^{-1} . sqrt cgamma already has the refinement
amplitude's shape, so no s <= Cms eps hypothesis is ever consumed. The two
comparisons are sqrtOrdinaryLane_le_frozen (main lane) and
sqrtOrdinaryLane_le_refinement (the second conjunct); the rare lane's is
sqrtRareLane_le_frozen.
Nearby statements elsewhere carry only the special cases K = 1,
s^{-1} = 1, or fix the lane constants homLaneOrdinaryConst /
homLaneRareConst. Since the assembled display needs the free constant
throughout, this module proves the free-constant versions and routes the lanes
through them.
3. The absorption calculus #
Three lemmas absorb the buckle's two non-lane tail families into the two
normal forms, using only the frozen root's own window binders cstar^{-1} eps^{-Cms} <= E and cgamma <= (E^{-1})^{10} and the freedom to choose Cms
after every dimensional constant:
absorb_window_poly— the polynomial laneQ cstar^{-1} cgamma eps^{-p} (s^{-1})^2 <= K1. (s^{-1})^2 (eps^2 E^2 cgamma)whenever2 + p <= CmsandQ <= K1 E. This is the shape of the wave term and of the bad lane's3^{5h} cgammasummand (the exponentpthere being10 Chom log 3 + 8, which is exactly the web conjunct10 Chom log 3 + 8 <= Cmsplus the two units ofepsthat theeps^2normalization costs).absorb_window_exp— the exponentially small laneQ exp(-(a E^{-2} cgamma^{-1})) <= K1 (eps^2 E^2 cgamma), by the elementaryx^2 exp(-x) <= 2atx = a E^{-2} cgamma^{-1}followed by the window.absorb_window_exp_rare— itsGamma_{1/4}counterpart, where the printed rateexp(-(Ccg^{-1} E^{-2} cgamma^{-1}))must clear the frozen root's ownexp(-(2 E^{-3} cgamma^{-1})); the gap is the single inequality4/a <= E, and what remains is again the elementary two-factorial bound.window_inv_pow_leis the single window utility they all share:(E^{-1})^n <= (3/2)^n eps^kwheneverk <= n Cms.
The deterministic remainder has NO absorption lemma of its own in this module.
Its three summands cgamma^2 h^2, cgamma^2 s^{-2} and cgamma^2 E^4 |log cgamma|^4 are absorbed in the consumer, by remainderGap_le,
remainderScale_le and remainderLog_le of MultiscaleAbsorptionArith. What
this module supplies them is three window facts: gamma_le_epsSq (cgamma <= (3/2)^{10} eps^2, consumed by the first two), sqrt_gamma_mul_sq_le (sqrt cgamma . E^2 <= (3/2)^3 eps^2) and sqrt_mul_abs_log_pow_four_le (sqrt x . |log x|^4 <= 384, the k = 4 case of the elementary x^k e^{-x} <= k!), the
last two consumed by remainderLog_le.
Finally, le_rpow_neg_fifth turns the frozen root's
cgamma <= (E^{-1})^{10} into the bad-event producer's fifth-root gate
E <= cgamma^{-1/5}. Countable-series measurability in the consumer uses
Mathlib's Measurable.tsum, without nonnegativity or summability premises.
1. The two-lane envelope calculus #
The squared display's envelope package. X is almost surely dominated
by U + V with U, V nonnegative, measurable, and carrying the squared
profiles Gamma_1 at scale A1 and Gamma_{1/4} at scale A2.
Probability.IsCommonEventTwoTermBigOWith is the closest existing shape — two
witnesses, two profiles, one almost-sure domination event — but it is indexed
over a family, which these five terms are not. Probability.IsTwoTermBigOWith
cannot serve as the carrier either, because it demands Measurable X and
X omega <= Y omega + Z omega pointwise, whereas the buckle's terms dominate
only almost surely; nonnegativity is not the obstruction (see §1 of the module
docstring).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A constant observable below a nonnegative scale has that scale.
Provider.Tail.isBigOWith_gammaSigma_const is the same statement with the two
hypotheses in the other order, but it is not in this module's import closure,
so the three-line fact is proved here rather than imported.
The zero observable has every nonnegative scale. This spelling delegates to the common zero-tail lemma used by the envelope constructors.
The max (Y omega) 0 compatibility spelling of the common positive-part
tail estimate.
The envelope calculus is monotone in both scales.
An almost-sure minorant inherits the envelope.
The envelope calculus is closed under addition, at the two Orlicz triangle constants of the squared display.
The envelope calculus is closed under multiplication by a nonnegative constant.
A single Gamma_1 tail on a nonnegative measurable observable is an
envelope, with an empty rare lane.
A deterministic bound is an envelope.
A raw envelope pair — measurable, tailed, almost surely dominating — is an envelope package: truncating both members at zero costs nothing, because both scales are positive.
Every proved two-term bound at the squared display's profiles is an envelope: its witnesses are truncated at zero, which costs nothing because both scales are positive.
2. The square-root buckle's amplitude normal forms #
The frozen root's refinement amplitude, reached from the SAME normal
form — this is what the eps^2 normalization buys: the second conjunct costs
nothing.
3. The absorption calculus #
The elementary x^k e^{-x} <= k!. The only other copy here,
HomogenizationLanes.pow_mul_exp_neg_le, is private; the derivation from
mathlib's Real.pow_div_factorial_le_exp is the same.
The quadratic decay of the exponential, in the form the two exponential lanes consume.
The other copies of exp(-x) <= 2/x^2 (both named exp_neg_le_two_div_sq, at
the 2 / x^2 spelling) are private, so the fact is re-derived here.
The window utility. Under the frozen root's own window binder, every
negative power of E is a power of eps, as soon as Cms has been chosen
large enough.
The polynomial absorption. A dimensional constant Q times the
window's own cstar^{-1} and any negative power eps^{-p} is absorbed into
K1 eps^2 E^2 as soon as 2 + p <= Cms and Q <= K1 E.
The exponential absorption, ordinary lane. The bad lane's printed rate
exp(-(c E^{-2} cgamma^{-1})) is polynomially smaller than the frozen root's
own eps^2 E^2 cgamma.
The exponential absorption, rare lane. The bad lane's Gamma_{2/7}
rate exp(-(Ccg^{-1} E^{-2} cgamma^{-1})) clears the frozen root's own
exp(-(2 E^{-3} cgamma^{-1})) as soon as 4/a <= E.
sqrt cgamma . E^2 is below eps^2 on the window: this is the remainder
term's E^4 |log cgamma|^4 summand's home.
Two re-derived siblings #
The frozen root's smallness gate implies the bad-event producer's own
fifth-root gate. The sibling
Provider.BadEvents.le_rpow_neg_fifth_of_gamma_le_inv_pow_ten is private, so
the same derivation is repeated here.