LambdaGridBridge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The on-grid lambdaSq bridge: Lambda_{s,q} as a weighted grid series #
Provider/CoarseEllipticity/ScaleSummation.lean and
Provider/CoarseEllipticity/LowerLeg.lean each retain the same conditional
analytic input, an explicit binder called hgrid: the domination of the
coarse-grained ellipticity constant by a weighted series of the per-scale
triadic grid maxima. This module supplies the deterministic content of that
binder and pins, with machine-checked negative controls, exactly which part of
it can and cannot be transported to this repository's Section 3 observables.
The two seams, and what happens to each #
(i) The index/pole seam. ABK26 defines
Lambda_{s,q}(cu_m;a) = ( c_{sq} sum_{k<=m} 3^{-sq(m-k)}
max_{z in 3^k Zd cap cu_m} |b(z+cu_k;a)|^{q/2} )^{2/q}
and CoarseGraining's Ch02.LambdaSqFinite is literally this, with c_{sq} = Ch02.geometricDiscount s q = 1 - 3^{-sq} and gap index n = m - k.
CoarseGraining's own bridge to a linear grid series exists only at q = 1
and delivers the pole s, whereas the consumers need the summation performed
at the q/2-power level, before the outer 2/q root. That is what
tsum_weighted_rpow_root_le does, by countable subadditivity of the concave
power x |-> x^{2/q} at q >= 2; the resulting weight arithmetic is
geometricWeight_rpow_succ:
(c_{sq} 3^{-sq(k+1)})^{2/q} = gridSumConst s q * gridWeight (2 s) k
so the pole is 2s for every q >= 2, not sq, and the collar absorption
gridWeight_mul_rpow of GridWeights.lean then moves it to the printed (2s - gamma) (geometricWeight_rpow_succ_collar). This settles the
weight-convention question flagged, and the "s-times-gridWeight (2s-gamma)"
reading of the printed deterministic pole is recovered, not assumed, through
gridSumConst_two_le (gridSumConst s 2 = 1 - 3^{-2s} <= 4 s). At the ruled
exponent q = 2 the two exponents q/2 and 2/q are both 1, the
subadditivity step is vacuous, and the bridge is an equality
(LambdaSqFinite_two_eq_top_add_gridSum) needing no summability binder at all.
The gap-0 term is carried explicitly. gridWeight covers gaps >= 1
only (GridWeights.lean); the source series has a gap-0 summand, the
one-cube quantity |b(cu_m;a)| at the top scale. Every statement below
displays it as a separate summand gridSumConst s q * (top-scale maximum);
nothing is silently dropped.
A.mk is Classical.choose of an existential and carries no pointwise
information about the literal observable, so the bridge proved here held
pathwise for the literal observables
(cutoffUpperEllipticityLiteral_two_eq_top_add_gridSum and its lower twin;
names corrected; the current conditional/A inventory describes the headline
families) and only almost everywhere for the representatives
(cutoffUpperEllipticity_ae_le_top_add_gridSum). The route suggested by the
genuine centered-cube rfl between the two exported observables did not
extend: that equality identified two representatives, not a representative
with a literal, and two negative controls confirmed it (cutoffUpperEllipticity = cutoffUpperEllipticityLiteral was not a definitional equality; neither was
cubeUpperEllipticity M Q L ... = cutoffUpperEllipticity M m L ... at an
arbitrary cube Q).
How it was removed. Exactly that change was made. On the source range 0 < s the clamp is inert (Observable.cutoffLowerEllipticityInv_eq_literal,
Observable.cutoffUpperEllipticity_eq_literal), so every pathwise statement
of this module descends to the exported observables at every sample point.
Both negative controls above are now vacuous: the first equality holds (not by
rfl, but by max_eq_right at 0 < s), and the second holds whenever Q = originCube d m.
The a.e. shadows below remain true, remain the statements the current consumers are written against, and are now provable in one line from the pointwise forms.
The leg-by-leg consequence, restated.
- Upper leg. Its payload's three witnesses are existential and its index
set is a single scale, so even under the old bodies the null set could be
absorbed inside the witness:
exists_pointwise_of_ae_threeTermSplittakes the three-term bound only almost everywhere and returns a domination valid at every sample point, with everywhere-defined measurable witnesses. No a.e. witness is produced or consumed anywhere;IsBigOWithis unchanged because it only sees the a.e. class (Provider.Tail.isBigOWith_of_ae_eq). That absorption is now optional rather than necessary. - Lower leg. Its payload needs one witness
Ydominating the whole family{X L}_{L >= m-1}at every sample point. Under the old bodies this was unreachable: on the null set the valuesX L omega = max 0 (mk_L omega)were uncontrolled for countably manyLat once andsup_L X L omegawas not known to be finite there, which is the obstruction recorded inLowerLeg.lean(point 1 of its module docstring) and inProvider/Tail/TailSqrt.lean(F-1). That obstruction is gone: the deterministic content of the lower leg'shgridconjunct is now available with the quantifier order∀ omega, ∀ L. The analytic content ofhgridremains an input of the historical consumers (ScaleSummation.lean,LowerLeg.lean). The concrete downstream theoremsuperposedFlux_coarse_ellipticity_lower_legsupplies the lower leg through a different finite-qpre-split route, so this conditional seam is no longer the global lower-leg status. The separate downstream theoremsuperposedFlux_coarse_ellipticity_upper_legsupplies the upper leg.
Main results #
tsum_rpow_le_tsum_rpow,tsum_weighted_rpow_root_le--- seam (i): the weightedell^{q/2}aggregate that definesLambda_{s,q}is dominated by the linear series with the reweighted coefficientsw^{2/q}, forq >= 2.gridSumConst,geometricWeight_rpow_zero,geometricWeight_rpow_succ--- the weight arithmetic of the2/qroot: the gap-0weight becomes the bare constant, and the gap-(k+1)weight becomesgridSumConst s q * gridWeight (2 * s) k, so the pole is2suniformly inq.lambdaSqFinite_inv_eq_rpow---lambda_{s,q}^{-1}unfolded as the positive2/qroot of the source's weighted series, at every coefficient family and with no positivity side condition.cutoffUpperEllipticityLiteral_eq_coeffField,cutoffLowerEllipticityInvLiteral_eq_coeffField--- the bridge at the Section 3 literal observables: at the centered cube they are the Chapter 4 ambient coefficient-field observables at the cutoff field.exists_pointwise_of_ae_threeTermSplit--- the pointwise-valid upgrade: an almost-everywhere three-term domination with a deterministic first slot becomes a domination valid at every sample point, with everywhere-defined measurable witnesses.
References #
- ABK26, coarse-grained ellipticity constants, (the definition and the
normalizer
c_{sq}). - ABK26,
p.cg.ellipticity.boundsfromp.bfA.multiscalebound. Provider/CoarseEllipticity/GridWeights.lean(gridWeight,gridSupAbs,maxDescendantBMatrixNormAtScale_eq_gridSupAbs),.../ScaleSummation.leanand.../LowerLeg.lean(the twohgridconsumers),Provider/BadEvents/CubeEllipticity.lean(the centered-cube literal identities),Provider/BadEvents/ObservableSwapPayoff.lean(the pointwise upgrades of the a.e. shadows below, and the off-centre transport).
1. The q/2-power level summation #
Countable subadditivity of the concave power. For 0 < theta <= 1 and a
nonnegative summable b whose theta-powers are also summable,
(sum b)^theta <= sum b^theta.
This is the step the printed proof performs silently when it sums the per-scale
displays inside the q/2-power and only then takes the 2/q root.
The q/2-power level summation (seam (i)). The weighted ell^{q/2}
aggregate that defines Lambda_{s,q} is dominated by the linear series with
the reweighted coefficients w^{2/q}, for every q >= 2.
2. The weight arithmetic of the 2/q root #
The k-independent constant produced by the 2/q root of the source's
normalizer: c_{sq}^{2/q} = (1 - 3^{-sq})^{2/q}.
Equations
Instances For
The gap-0 weight, after the 2/q root, is the bare constant.
The index/pole identity of seam (i). After the 2/q root the source's
gap-(k+1) weight is the grid weight at pole 2s, uniformly in q. This is
why the printed poles are (2s - gamma)-type and not (sq - gamma)-type.
3. The pathwise bridge at CoarseGraining's deterministic carriers #
lambda_{s,q}^{-1} unfolded: the negative root of the source's series is
inverted to the positive root, at every coefficient family and with no
positivity side condition.
7. The bridge at the Section 3 observables #
The Section 3 literal upper observable is the Chapter 4 ambient
observable at the cutoff field. NeZero d is a Prop class, so the instance
carried inside the observable's definition and the one supplied here are
definitionally equal.
The Section 3 literal lower observable is the inverse of the Chapter 4 ambient observable at the cutoff field.
8. The pointwise-valid upgrade, and the upper leg's summation #
The pointwise-valid null-set upgrade. An almost-everywhere three-term domination with a deterministic first slot upgrades to a domination valid at every sample point, by moving the defect into the ordinary lane on a measurable null set.
Nothing produced here is an almost-everywhere witness: U1' is an
everywhere-defined measurable function, the domination is forall omega, and
the Gamma tail is unchanged because IsBigOWith only sees the
almost-everywhere class (Provider.Tail.isBigOWith_of_ae_eq). This upgrade is
available to the upper leg only; the lower leg's single witness must
majorize a whole L-indexed family at once, and on the null set that supremum
is not known to be finite (see the module docstring).