HomogenizationLanes #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: the lane aggregation and corridor consumption of `e.what.homogenization.gives` #

ABK26, §3.6.

s * sum_{l = -infty}^{m} 3^{-s(m-l)}
      ( avsum_{z in 3^l Z^d cap cu_m}
          max_{|e| = 1} J(z + cu_l, shom_{l-h}^{-1/2} e, shom_{l-h}^{1/2} e; a_{l-h})^{d/s}
      )^{s/d}
  <= O_{Gamma_1}(C s^{-1} eps E^2 cgamma)
   + O_{Gamma_{1/4}}(C eps exp(-E^{-3} cgamma^{-1})) ,

proved in the manuscript in one sentence: "an immediate consequence of Proposition p.homogenization.step, the triangle inequality e.Gamma.sigma.triangle and the fact that s >= 8 cgamma, provided that h:= C |log eps| for C large enough".

This module is the other half: the (l, z) aggregation, the corridor bookkeeping, and the a.e.-to-pointwise bridge.

The route #

Fix a depth j, write l = m - j, and let N_j = 3^{dj} be the depth-j grid cardinality.

The grid maximum. The per-cube inputs at depth j share one amplitude pair, so the maximum over the N_j cubes is Gamma_sigma at (3 max{1, log N_j})^{1/sigma} A --- the manuscript's own l.maximums.Gamma.s, in the proved singleton-safe form Orlicz.isBigOWith_gammaSigma_finset_sup'_of_nonempty.
The power-mean ceiling. A power mean is below the maximum of its arguments, so the printed (avsum_z (.)^{d/s})^{s/d} is below that grid maximum. This is the proved Breakdown.legScaleAverage_le_const; it costs nothing.
The depth sum. The per-depth amplitudes 3^{-sj} (3 max{1, d j log 3})^{1/sigma} A are summable, with the closed forms of sections 3 and 4 below: 45 d s^{-2} A_1 on the Gamma_1 lane and 12000000 d^4 s^{-5} A_2 on the Gamma_{1/4} lane. The countable Gamma_sigma triangle inequality (Orlicz.isBigOWith_gammaSigma_tsum_of_tsum_le, constant gammaTriangleConst sigma) then produces one envelope per lane.

After the printed normalization by s the amplitudes are C(d) s^{-1} A_1 and C(d) s^{-4} A_2. So this module delivers the best profile the manuscript's own proof supports.

A divergence of route. The printed one-line proof attributes the z-aggregation to e.Gamma.sigma.triangle. That route is not taken here, for a formalization reason: the available gammaTriangleConst sigma = 4 gammaGrowthConst sigma ^ 12 is not the sharp M_sigma ~ sigma^{-1/sigma}, and at the index sigma s/d it inflates s^{-4} to s^{-48}. This module therefore routes through the Appendix's own l.maximums.Gamma.s per depth and the triangle inequality across depths, where the index is fixed at 1 and 1/4 and the constant is absolute. Same displays, same exponents, different mechanism.

The amplitudes, and how they meet the frozen root #

At eps' := eps^2 the per-cube input carries A_1 = eps^2 E^2 cgamma and A_2 = eps^2 exp(-2 E^{-3} cgamma^{-1}) (the sharp rate). The two lanes therefore read, after the printed normalization by s,

Gamma_1      :  C_ord(d) s^{-1} eps^2 E^2 cgamma ,
Gamma_{1/4}  :  C_rare(d) s^{-4} eps^2 exp(-2 E^{-3} cgamma^{-1}) .

The first is below the printed C s^{-1} eps E^2 cgamma a fortiori (eps <= 1/2).

Deliverables #

** the lane aggregation** --- exists_envelope_gridScaleSeries_of_perCube (abstract) and exists_envelope_gridScaleSeries_homogenizationInput (at the development's carriers, on the proved GoodEventAggregation.gridScaleSeries). The domination is ONE almost-sure statement with the depth and cube quantifiers inside the event, so the per-cube input's common-event structure survives in the statement. The concrete proof does take the countable intersection --- the per-cube producer emits one a.e. statement per (j, R) and section 8 collects them by MeasureTheory.ae_all_iff over depths and Filter.eventually_all_finset over each depth's finite grid --- which is harmless (countable intersection of full-measure sets) and exactly why the strong form is provable.
(c) the pointwise endpoint --- exists_witnesses_of_envelope. The device is the web's unconditional exists_witnesses_ae_eq_of_ae_le: the returned witnesses are almost everywhere equal to the envelopes, so a further tail of those envelopes transfers and the frozen conclusion's second conjunct survives on the same Y.

geometricDiscount_two_mul_le_of_nonneg is the seam to e.localization.mathcalE.estimate's own normalization: c_{2s} <= 4 s at the localization side's own carrier from Provider.Localization.geometricDiscount_two_le_four_mul, so the s-normalized display dominates the localization lemma's first term at an absolute cost.

Named gaps, with owners #

The max_e carrier and the measurability of the display are items 1 and 2 above.

Sources #

ABK26: the avsum average; e.what.homogenization.gives (its one-line proof and the cutoff h := C|log eps|); p.multiscale.estimate and e.param.conditions.in.main; the Appendix's weak-Orlicz notation and l.maximums.Gamma.s, whose amplitude (3 log N)^{1/sigma} A is exactly the proved Provider/Orlicz/Maximum.lean engine's.

HomogenizationLanes #

Provider: the lane aggregation and corridor consumption of e.what.homogenization.gives #

The route #

The amplitudes, and how they meet the frozen root #

Deliverables #

Named gaps, with owners #

Sources #

1. The depth series #

2. The polynomial factor of the grid maximum #

3. The two depth-series amplitudes #

4. Summability of the two depth series #

5. The abstract lane aggregation #

6. The lane aggregation #

8. The lane aggregation at the development's carriers #

9. The two normalizations, the printed one and the localization one #

10. The printed normalization and the pointwise endpoint #

Provider: the lane aggregation and corridor consumption of `e.what.homogenization.gives` #