LocalizationAssembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the localization assembly l.localization.mathcalE #
Here the per-cube estimate is averaged over the printed grid, summed over the scales and composed into the printed five-term display.
Contents #
- §4 — the grid reindexing.
injOn_triadicCubeShift_descendantsAtScaleandindicator_average_image_eqmove the printed⨍_{z ∈ 3^l ℤ^d ∩ □_m}average of the bad-event indicator between the development's descendant index set and theVec d-indexed grid at which the frozengoodLocalEventAt— and thereforee.local.bad.events.summed— is stated. - §5 — the bad lane.
- §7 —
localization_mathcalE_estimate_ae, the endpoint.
The five terms, and what each costs #
Writing Cinj(Ccg) = 324·Cresp(d)·(16Ccg + 8Ccg²), the delivered display is
𝓔_{s,∞,2}(□_m; a_m, σ_m)²
≤ 12 c_{2s} Σ_l 3^{-s(m-l)} (⨍_z legA(z+□_l; a_{l-h}, σ_{l-h})^{d/s})^{s/d}
+ 12 c_{2s} Σ_l 3^{-s(m-l)} (⨍_z legB(z+□_l; a_{l-h}, σ_{l-h})^{d/s})^{s/d}
+ 32 Cinj(Ccg) c⋆⁻¹ γ · waveSizesTotalW2(m, h, s)
+ 8 (max_l 3^{-s(m-l)/2}(⨍_z 1_{¬𝒬(l,l-h,z)})^{s/d}) · 𝓔_{s/4,∞,2}(□_m; a_m, σ_m)²
+ 1024 Cs·48Ccg · γ² (h² + s^{-2} + E⁴|log γ|⁴) .
against the printed 6 / 6 / C c⋆⁻¹γs / C / Cγ². The delivered leading
numeral is 12 at the leg carrier. Measured at the printed max_{|e|=1}
carrier it is 24 against the printed 6 — a factor-4 loss — because each
leg is twice that maximum and legScaleAverage is degree-one homogeneous,
while the left-hand side 𝓔² of this display carries no doubling at all.
(The doubling sits on both sides only for the breakdown identity and for the
per-(l,z) endpoint, where both sides are legs.) The factor-4
reading is the conservative one and is what both module headers record. The
numeral is 8 × 3 / 2. Writing C (or 12, or 24) in place of the printed
explicit 6 changes nothing downstream. The remaining three printed constants
are C's, and the delivered 32 Cinj c⋆⁻¹γ, 8 and 1024 Cs·48Ccg are
explicit admissible values of them.
The scale gate on m0 #
The landmark premise carried by the endpoint below is mStarStar M < m0,
not the printed m0 in (mstar, infty) cap Z: l.shom.continuity's
hypothesis is corrected to m0 in (mstarstar, infty) cap Z, and its whole
downstream chain is re-gated the same way. Nothing else moved: the premise is
forwarded verbatim to the proved producers consumed here, no proof step here
consumes it, and no frozen statement changes.
The h-window #
The printed h ∈ ℕ₀ ∩ [0, γ⁻¹] window is one point too large:
e.local.bad.events.summed needs 1 ≤ h, because at h = 0 its fourth-term
lane would demand the frozen bad-event estimate at the induction level itself.
Carried, not closed #
The printed grid 3^l ℤ^d ∩ □_m is read as
triadicCubeShift '' descendantsAtScale (□_m) l. §4 proves only the
injectivity that reindexing an average needs; the identity of the image with
the printed lattice is NOT proved here and remains a convention.
4. The grid reindexing of the printed z-average #
The printed average runs over the lattice points z ∈ 3^l ℤ^d ∩ □_m; every
proved carrier of this development runs over descendantsAtScale (□_m) l. The
identification of the two index sets is the development's standing grid
convention ((i) / -017 (ii) / -027 (iii)) and is NOT closed here: what is
proved below is only that triadicCubeShift is injective on a descendant
family, which is all the reindexing of an average needs. Whether its image
is literally 3^l ℤ^d ∩ □_m remains the open half of that convention.
triadicCubeShift is injective on a descendant family. All members
have the same scale, and at a fixed scale the shift determines the index.
The printed z-average of the bad-event indicator, reindexed. The
descendant-indexed average of 1_{¬𝒬(l,l-h,z)} equals the average over the
image grid F j = triadicCubeShift '' (descendants at depth j), at the frozen
goodLocalEventAt spelling that e.local.bad.events.summed consumes. The
bridge from the cube-indexed to the centred event is the proved
BadEvents.goodLocalEventAt_triadicCubeShift.
5. The bad lane #
Printed step 1 (BadEventPreCeiling.preCeiling_average_le) extracts the grid
maximum out of the L^{d/s} average; the proved max engine
(BadEventMaxSplit.tsum_badMax_le_four_mul_homogenizationErrorOnCube_sq) then
pays the whole l-sum once against 𝓔²_{s/4}. This is the fourth term of the
printed display, at its max_l 3^{-s(m-l)/2}(⨍_z 1_{¬𝒬})^{s/d} shape
and the pure constant 4 per leg.
The printed bad-event factor at depth j, (⨍_{z ∈ 3^{m-j} ℤ^d ∩ □_m} 1_{¬𝒬(m-j, m-j-h, z)})^{s/d}, at the frozen goodLocalEventAt spelling and at
the grid F j obtained by shifting the scale-(m-j) descendants of □_m (the
development's grid convention (i)). badGridAverage_eq records that this is a
definitional abbreviation, not a new object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The printed bad-event factor is [0,1]-valued ([P]). The ceiling is NOT
re-derived here: it is the proved
MultiscaleEstimate.weightedIndicatorAverage_rpow_mem_Icc
(BadEventCeiling.lean) at the trivial weight w := 1.
8 · max_{l ≤ m} 3^{-s(m-l)/2} (⨍_z 1_{¬𝒬(l,l-h,z)})^{s/d} · 𝓔²_{s/4,∞,2}(□_m; a, a₀) .
Printed step 1 is the proved BadEventPreCeiling.preCeiling_average_le; the
l-sum is paid once by the proved BadEventMaxSplit max engine at its pure
constant 4, and the extra 2 is the frame doubling of the leg.
6. The good/bad split of the printed left-hand side and the wave series #
The indicator split of e.mathcal.E.breakdown's leg sum. The printed
left-hand side splits into its good and bad parts with constant 1: the
indicator of the manuscript's 𝒬(l,l-h,z) and its complement add to 1, and
the per-scale power mean is subadditive (Breakdown.legScaleAverage_le_add, the
d/s ≥ 1 Minkowski step).
7. The endpoint: l.localization.mathcalE at the printed five-term display #
For the multiscale root's own regime, every gap h ∈ ℕ₀ with γ h ≤ 1 and
every s ∈ [8γ, 1], almost surely:
𝓔_{s,∞,2}(□_m; a_m, σ_m)²
≤ 12 c_{2s} Σ_{l ≤ m} 3^{-s(m-l)} (⨍_z legA(z+□_l; a_{l-h}, σ_{l-h})^{d/s})^{s/d}
+ 12 c_{2s} Σ_{l ≤ m} 3^{-s(m-l)} (⨍_z legB(z+□_l; a_{l-h}, σ_{l-h})^{d/s})^{s/d}
+ 32 Cinj(Ccg) c⋆⁻¹ γ · [a majorant of] s Σ_{l ≤ m} 3^{-s(m-l)} (⨍_z
(3^{(2-γ)l}‖k_m-k_{l-h}‖_{W^{2,∞}})^{2d/s})^{s/d}
+ 8 max_{l ≤ m} 3^{-s(m-l)/2} (⨍_z 1_{¬𝒬(l,l-h,z)})^{s/d} · 𝓔_{s/4,∞,2}(□_m; a_m, σ_m)²
+ 1024 Cs 48Ccg γ² (h² + s^{-2} + E⁴|log γ|⁴) .
The five summands are the five printed terms in order. Term-by-term against the print:
- first two — the printed
6 c_{2s} Σ_l 3^{-s(m-l)}(⨍_z max_e J(·;a_{l-h}))^{s/d}and its adjoint, at the development's frame-sup carriersbreakdownLeg{A,B}, each of which is twice the printedmax_{|e|=1}object. The resulting factor is dimension-free and is absorbed downstream bye.what.homogenization.gives's ownC. - The delivered term is therefore a majorant of the printed one, which is the admissible direction here; it is not an equality and must not be read as one.
- Its
𝓔²_{s/4}factor is stated at CoarseGraining'sCh02.HomogenizationErrorOnCube (□_m) (s/4) ∞ 2 a_m (isotropic σ_m)rather than atObservable.cutoffHomogenizationError M m ⟨s/4, _⟩, which is where the left-hand side sits. This is a deliberate carrier choice, not an obstruction, and the consumer's bridge is one line:BadEventSummed.ae_sq_cutoffHomogenizationError_eq_homogenizationErrorOnCube_sq. - fifth — the remainder at the proved absolute constant
1024, in the correctedmin{γ²Δ²,1}3^{2γΔ}shape.
The hypotheses are 0 < Ccg (the manuscript's good-event constant is a free
parameter here, so that the consumer may thread the same Cbad into this
display and into e.local.bad.events.summed) and the two Summable
premises on the deep lanes (a_{l-h}, σ_{l-h}, one per leg). There is no
wave-lane premise: it is discharged in §6 by ae_summable_wave_scale_series.
The good lane's own summability is discharged internally from the proved
uniform descendant bound.