TailSummability #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The upper shell series converges almost surely: hTae discharged #
What this module does #
tailLayerSum m k v ω L = Σ_{i ∈ (m, L]} ‖∇ j_i‖_{W^{1,∞}(3^k v + □_k)} ,
and tailLayerSum_le_tailSeriesGauge reduced an L-uniform bound for it to the
Summableity of the layer terms. This module proves that summability -- for
every cube (k, v) simultaneously -- almost surely, and therefore discharges
the hTae binder of
AeMajorantTransport.lintegral_observableSup_rpow_le_tsum_lintegral_lFreeStep3Majorant_of_ae
at the canonical gauge T := tailSeriesGauge m.
The route #
The per-layer display.
Support.shellW1InfGradNorm k jis the maximum of‖∇²j‖_{L∞(□_k)}and3^{-k}‖∇j‖_{L∞(□_k)}, hence at most3^{-k}(‖∇j‖_{L∞(□_k)} + 3^{k}‖∇²j‖_{L∞(□_k)}). For the shellj_iwithk ≤ ithe bracket is exactly the manuscript'se.nabla.jk.Ogauge measured on the smaller cube, i.e. the provedStream.isBigOWith_gammaSigma_shellDerivGauge_cubeat amplitude3^{(γ−1)i}. So the layer term is𝒪_{Γ₂}(3^{-k} 3^{(γ−1)i}), and the amplitudes are summable inibecauseγ ≤ 1/4 < 1.The carriers. The display lives on
Cutoff.ShellSeq dunderM.P; the transfers toCutoff.CutoffSample dunderCutoff.cutoffSampleLaw Mand to the translated cube3^k v + □_kare the provedStream.isBigOWith_cutoffSampleLaw_of_forall_eq_comp_valandStream.isBigOWith_comp_translateCutoffSample-- exactly the pairProportion.G1AtomTailsuses for the𝒢₁atoms. No lattice restriction is used: the statement holds at every real centre, so at every(k, v).The first-moment bridge.
Orlicz.ae_summable_of_isBigOWith_gammaSigma: a summable family of positiveΓ_σscales forces almost sure summability (Tonelli on the first moments). It is indexed byℕ, so theℤ-indexed layer family is re-indexed ati₀ = max (m+1) k-- the finitely many layersi ∈ (m, k), where the cross-scale display is unavailable, are irrelevant to summability and are absorbed bysummable_nat_add_iff.The countable family.
MeasureTheory.ae_all_iffover the countable indexℤ × (Fin d → ℤ).The negated leg., and pointwise: every layer gauge is even (
Annular.shellW1InfGradNorm_negate,Localization.translate_negate), sotailLayerTerm,tailLayerSumandtailSeriesGaugeare all literally invariant underCutoff.negateCutoffSample. The law-level invarianceCutoff.map_negateCutoffSample_cutoffSampleLawis NOT consumed.
References #
- ABK26, (
e.nabla.jk.O); (the gradient slot); (Step 3).
1. The per-layer deterministic domination #
The volume-normalized gradient gauge on □_k is dominated by the
e.nabla.jk.O gauge on the same cube, rescaled by 3^{-k}: the gauge is a
maximum of two nonnegative legs and the bracket is their 3^{k}-weighted sum.
2. The cross-scale Γ₂ tail of one layer gauge #
The layer gauge at a smaller cube, on the shell-sequence law. For k ≤ i
the gauge ‖∇j_i‖_{W^{1,∞}(□_k)} has a Γ₂ upper tail at amplitude 3^{-k} 3^{(γ−1)i}: the manuscript's e.nabla.jk.O measured on □_k and
renormalized. Only proved Section 3 material enters.
The layer gauge at a translated cube, on the cutoff-sample law. The two
proved transfers -- the measurable-embedding transfer to Cutoff.CutoffSample
and the real-translation invariance of the cutoff-sample law -- carry the
display of isBigOWith_gammaSigma_shellW1InfGradNorm_shellSeq to
‖∇j_i‖_{W^{1,∞}(z + □_k)} real centre z, at the same amplitude.
3. The geometric amplitude family #
The common ratio of the layer amplitudes: 3^{γ−1} < 1 because γ ≤ 1/4.
4. Almost sure summability of the layer terms #
The upper shell series converges almost surely, at one cube.
For every scale k and lattice index v, the ℤ-indexed layer family of
ShellSlotBounds.tailLayerTerm is almost surely summable. This is the
probabilistic content of hTae.
The upper shell series converges almost surely, at every cube
simultaneously. The index ℤ × (Fin d → ℤ) is countable, so the null sets of
ae_summable_tailLayerTerm may be unioned.
5. The negated leg, pointwise #
Every layer gauge is even, so the ℤ-indexed layer term is literally
invariant under whole-sequence negation.
The finite layer block is N-invariant.
The canonical tail gauge is N-invariant.
6. hTae, in the exact shape the transport asks for #
hTae discharged at T := tailSeriesGauge m.
Almost surely, the value of the upper shell series dominates every truncated
layer block, at the sample AND at the negated sample. The second conjunct is
free: it is the first one composed with the pointwise N-invariances of §5, so
no law-level symmetry input is consumed.