GoodEventAggregation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Part 1 --- the v-uniform injection endpoint #
The three steps (i), bottom up.
Step A --- the response-J sensitivity switch, v-uniform #
BadEvents.responseJ_sensitivity_of_mem_goodLocalEvent_ae binds (p, q)
outside its ∀ᵐ, but its whole proof is one filter_upwards on the v-
BadEvents.lambda_transfer_ae, applied to the pointwise public
…_of_lambdaTransfer. Moving ∀ p q inside the event is therefore free.
The response-J sensitivity switch on the good event, uniformly in the
loads. On ONE probability-one event (the one of
BadEvents.lambda_transfer_ae), simultaneously for every pair of loading
vectors (p, q), the coefficient switch of ABK26 holds in the form used.
This is BadEvents.responseJ_sensitivity_of_mem_goodLocalEvent_ae with the two
loading binders moved INSIDE the almost-sure quantifier; the statement is
otherwise character-identical.
Conditional on the caller-supplied omega ∈ goodLocalEvent M Ccg Q n, the
manuscript's own indicator, inherited verbatim.
Step B --- the composed delta = 1 endpoint, v-uniform #
The second a.e. input of the composed delta = 1 sensitivity display, namely
BadEvents.gradientW1Infinity_incrementUnitCube₂_le_responseGate_ae, is
already v-free, and every remaining ingredient of that proof is deterministic.
The composition below is the proved one, re-threaded with ∀ p q inside.
The composed delta = 1 sensitivity endpoint, uniformly in the loads.
The composed delta = 1 sensitivity display of SensitivityBridges, with the
two loading binders moved INSIDE the almost-sure quantifier. The event is the
intersection of the two v-free events already used there.
The deterministic ingredients are consumed unchanged: the response gate
(BadEvents.gradientW1Infinity_incrementUnitCube₂_le_responseGate_ae), the
3^{4l} fingerprints
(SensitivityBridges.w1Infinity_sq_incrementUnitCube₂_le,
…gradientW1Infinity_sq_incrementUnitCube₂_le), the reciprocal gauge
conversions (SensitivityBridges.inv_unitCubeLambda_le_inv_lambdaSq_oneEighth
and its square), the rescale companion
(SensitivityBridges.responseJ_cutoffFamily_eq_unitRescaledCutoffCoeff), and
CoarseGraining's Ch02.responseJ_nonneg.
Conditional on omega ∈ goodLocalEvent M Ccg Q n, inherited verbatim.
Step C --- the priced injection endpoint, v-uniform #
The per-(l,z) priced injection display, uniformly in the loads.
The priced injection display of LambdaGateChain with ∀ v, vecNormSq v ≤ 2
moved INSIDE the almost-sure quantifier: on ONE probability-one event,
simultaneously for every loading direction, the printed display holds. The
premise list, the witness C (the l.shom.continuity constant) and the four
explicit constants 3, 324, 16 Ccg + 8 Ccg², c⋆^{-1} γ 3^{4l-2γl} are
inherited character-for-character; nothing is weakened and nothing is added.
This is the form the composed switch endpoints
SwitchNormalization.breakdownLeg{A,B}_le_of_shom_switch need for their
hdeep binder, which quantifies over the loading ball at a fixed sample.
Conditional on omega ∈ goodLocalEvent M Ccg Q (Q.scale - hgap), 0 < Ccg and
the displayed scale premises, all inherited verbatim.
Step D --- one null set for the whole grid #
The previous endpoint still produces ONE null set per (Q, hgap, L). Part 2's
consumer entry point geometricDiscount_mul_gridScaleSeries_good_le fixes
omega and demands the per-(j, R) estimate for descendant cube, so the
z-aggregation needs the cube/gap/scale-uniform form as well. It is available
at zero mathematical cost: TriadicCube d is countable, so three
MeasureTheory.ae_all_iff rewrites move ∀ Q hgap L outside the almost-sure
quantifier, and the three scale premises are discharged by case analysis (when
one of them fails the conclusion is vacuous).
The priced injection display on ONE null set, uniformly in the cube, the gap, the coefficient scale AND the load (as read by the z-aggregation).
responseJ_injection_priced_ae_forall_loads with ∀ Q hgap L and their three
scale premises ALSO moved inside the ∀ᵐ: on one probability-one event,
simultaneously for every triadic cube, every gap, every coefficient scale and
every loading direction, the printed display holds. Nothing is weakened: the
premise list, the witness C and the four constants are those of the endpoint
above, and instantiating this form at a fixed (Q, hgap, L) recovers it.
This is what the grid aggregation needs, because
geometricDiscount_mul_gridScaleSeries_good_le's hstep binder quantifies
over all descendants at a fixed sample.
Conditional on omega ∈ goodLocalEvent M Ccg Q (Q.scale - hgap) and 0 < Ccg,
both inherited verbatim.
Part 2 --- the good-event grid aggregation engine #
Everything below is gauge-free and carrier-free: no diffusivity, no threshold,
no coefficient family occurs. The only development-specific object is the
remainder carrier AggregationRemainder.switchRemainder, at which the remainder
collapse is consumed.
The per-scale step (grid Minkowski) #
Breakdown.legScaleAverage Q k s leg is the printed
(⨍_{z ∈ 3^k ℤ^d ∩ Q} leg(z+□_k)^{d/s})^{s/d}. For s ≤ 1 ≤ d the inner
exponent d/s is at least one, so the power mean is subadditive; it is also
degree-one homogeneous, and the power mean of a constant is at most that
constant (with equality off the empty grid).
The three-term reinjection at one scale. A per-cube estimate
leg(z+□_k) ≤ c · deep(z+□_k) + b · wave(z+□_k) + rem
valid on the whole grid passes through the printed L^{d/s} average with
unchanged multiplicative constants and an unchanged additive remainder. Two applications of
Minkowski, two of homogeneity, one constant lane.
This is the printed "summing over z ∈ 3^l ℤ^d ∩ □_m and applying the
triangle inequality", at one localization scale. The grid's cardinality
enters only through the average's own normalization.
The printed spelling of the good part. The manuscript writes the indicator
INSIDE the d/s-th power, (⨍_z (max_e J)^{d/s} 1_{𝒬(l,l-h,z)})^{s/d}; the
statements above truncate the leg first. No sign hypothesis on the leg is
needed.
The l-sum #
Breakdown.breakdownLegSum carries ONE leg for all scales, which is what the
printed left-hand side needs (a_m and σ_m do not move). The right-hand
sides of the good-event aggregation are genuinely scale-indexed --- a_{l-h},
σ_{l-h} and 3^{4l-2γl}‖k_m-k_{l-h}‖² all move with l --- so the sum
below is taken over a per-scale of legs. On a constant family the two agree by
rfl.
The printed weighted grid sum Σ_{l ≤ m} 3^{-s(m-l)} (⨍_z leg_l(z+□_l)^{d/s})^{s/d}
of a per-scale leg family, reindexed by the depth j = m - l ∈ ℕ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A weighted grid sum of a nonnegative leg family is nonnegative.
The named producer of the Summable caller obligations below. A
uniform descendant bound D on the whole leg family makes the weighted grid
series summable, by domination against the bare geometric series.
This is the per-scale-family analogue of the proved
Breakdown.summable_breakdownLegSum_terms, and it carries the same [NeZero d] binder, which the consumers themselves do not.
The three-term reinjection of the whole l-sum. The per-scale estimate
of legScaleAverage_le_three_term, summed against the printed weights
3^{-s(m-l)}.
A: the four Summable binders are caller obligations (a divergent tsum is
0 in Lean); the producer of the first three is
summable_gridScaleSeries_terms.
The composed good-event aggregation #
The remainder lane is routed into the proved remainder collapse at the sibling's
own switchRemainder carrier, so that the cross-file seam
(AggregationRemainder.switchRemainder_eq_of_int_gap) is the ONLY place where
the σ-switch remainder is reshaped.
The good-event aggregation at the printed weights. With the per-(l,z)
reinjection estimate available at every depth, at a per-cube remainder dominated
by C_rem · the corrected σ-switch remainder, the whole printed left-hand
side collapses to
c · (c_{2s} Σ_l 3^{-s(m-l)} (⨍_z deep^{d/s})^{s/d})
+ b · (c_{2s} Σ_l 3^{-s(m-l)} (⨍_z wave^{d/s})^{s/d})
+ 1024 C_rem γ² (h² + s^{-2} + E⁴|log γ|⁴) .
The last summand is the fifth term of e.localization.mathcalE.estimate; its
1024 is the proved absolute constant of
AggregationRemainder.localization_remainder_series_le_of_termwise, and the
caller's own C_rem passes through multiplicatively.
A: the three Summable binders, as above. The remainder lane's summability is
discharged internally.
The consumer entry point of the good lane. The composed aggregation with
the manuscript's indicator in place: the per-(l,z) estimate is assumed only ON
the good event 𝒬(l,l-h,z), and the left-hand side is the printed good part.
Together with legScaleAverage_indicator_eq (which puts the indicator back
inside the d/s-th power) this is the printed display at the abstract legs;
the assembly supplies the legs, the constants c, b, C_rem and the
per-(l,z) estimate.