PrincipalResponseDisplayTwoMoment #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.
Provider: the expectation and the measure transport behind display 2 #
Display 2 of leg (iv) of l.approximate.recurrence.formula takes an
expectation of a fourth power. The pathwise input, e.nablaw.in.L.eight,
controls the corrector energies by a deterministic head plus a Gamma_1
fluctuation, so the expectation that has to be evaluated is the second
moment of a shifted one-lane weak-Orlicz variable. That engine is the proved
integral_rpow_two_le_of_shift_add_one_orlicz; this module supplies the three
pieces of plumbing that stand between it and the display.
1. Two lanes into one #
The fourth-power display carries two fluctuation lanes, not one: the
Calderon-Zygmund lane of e.nablaw.in.L.eight and, separately, the lane of the
forcing shom^{-1} (k_m - k_{m-h}) e' that the Neumann slot of e.Pz.def
adds to grad w_N. isBigOWith_gammaSigma_one_add merges them: at the
manuscript's exponent sigma = 1 the sum of two lanes is again a single lane,
at twice the sum of the amplitudes. The doubling is exactly what pays for the
union bound, since 2 exp(-2t) <= exp(-t) for t >= 1.
2. From the shell law to the cutoff-sample law #
e.nablaw.in.L.eight is stated on the canonical shell-sequence law
M.P.toMeasure; the displays of Step 3 live on the lower-tail-good carrier
Cutoff.CutoffSample d with its induced law Cutoff.cutoffSampleLaw M.
isBigOWith_cutoffSampleLaw_of_isBigOWith transports a weak-Orlicz upper tail
along Subtype.val. The transport is one-sided by design and needs no
measurability of the lane: the upper-tail event of the composite is the
preimage of the upper-tail event of the original, and
MeasureTheory.Measure.le_map_apply bounds the measure of a preimage by the
pushforward of any set, measurable or not, which
Cutoff.map_cutoffSampleLaw_val identifies with the shell law.
3. The expectation, with no measurability assumed of the lane #
The lane witnesses produced by e.nablaw.in.L.eight and by e.km.kn.Lp are
existential and carry no measurability. integral_le_of_le_shift_add_kappa_sq
is stated so that none is needed: the only measurable object is the display's
own integrand X, and the proof runs the moment engine on the measurable
proxy sqrt(max(X - B, 0) / kappa), which is pointwise below the true energy
and therefore inherits its tail by IsBigOWith.of_le. This is the same device
by which the proved engines handle non-negative parts, applied one level up.
Portability #
Section 1 and section 3 mention no ABK26 object and would move to CoarseGraining unchanged; section 2 is about this repository's cutoff carrier and stays here.
Main results #
Merging two Gamma_1 lanes #
Two Gamma_1 lanes are one Gamma_1 lane. At the manuscript's
exponent sigma = 1 the sum of two one-sided stretched-exponential variables is
again one, with amplitude twice the sum of the two amplitudes: the union bound
costs a factor 2, and 2 exp(-2t) <= exp(-t) for t >= 1 pays for it.
Transport to the cutoff-sample law #
A weak-Orlicz tail transports to the cutoff-sample carrier. If a
variable on the canonical shell-sequence law is O_Psi(A), then its restriction
to the lower-tail-good carrier is O_Psi(A) for the induced law. No
measurability of the variable is used.
The expectation of a fourth power under a shifted one-lane bound #
The expectation of display 2, from a shifted one-lane energy bound.
Let X be a non-negative measurable observable dominated by a deterministic
shift B plus kappa times the square of an energy W, and let W itself be
dominated by a deterministic shift b plus a single one-sided
stretched-exponential lane Y of amplitude A. Then
E[X] <= B + kappa (2 (b + c(sigma) A))^2 ,
with c = orliczSecondMomentScale the class constant of the proved engine
integral_rpow_two_le_of_shift_add_one_orlicz.
Neither W nor Y is assumed measurable: the engine is run on the measurable
proxy sqrt(max(X - B, 0)/kappa), which is pointwise below W and therefore
inherits the lane by IsBigOWith.of_le.