UnionAggregation

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

Aggregation of the Section 3.5 grid displays over the cutoff family

ABK26 (proof of p.homogenization.step) fixes two integer separations k1 and k2, puts k = k1 + k2 and n = L + k1, and then sums the per-cutoff grid concentration display over the infinite family

{L in Z : L <= m - k}

to obtain e.union.bound.fluct. This module performs that aggregation on the genuine cutoff sample law and packages it in the shape the Section 3.5 statement uses for its supremum, namely one pair of measurable envelopes dominating the whole indexed family on a single event of probability one.

Its abstract measure-theoretic part --- the A of the common-event two-term carrier, which refers to nothing in Section 3.5 --- is Provider/Orlicz/CommonEventAggregation.lean, and the finite direction net that the Section 3.5 statement needs in order to pass from one direction to the uncountable Euclidean unit sphere is Provider/Homogenization/UnionDirectionNet.lean.

What is aggregated

For each j : N the member of the family is the recentred grid average of ABK26 at the cutoff L_j = m - k1 - k2 - j and the observation scale n_j = L_j + k1 = m - k2 - j, written at relative depth m - n_j = k2 + j. The proved grid display isTwoTermBigOWith_gridAverage_siteCenteredResponseJ gives each member a one-sided two-term (Gamma_1, Gamma_{1/4}) bound whose two amplitudes carry the factor 3 ^ (-d (k2 + j) / 2). Both amplitudes are therefore summable in j with a geometric ratio 3 ^ (-d/2) < 1, and their sums carry the single extra factor (1 - 3 ^ (-d/2))^{-1}, a constant depending only on d.

The measure-theoretic reading of the supremum

That is exactly the content of Algsuperdiff.Section3.Probability.IsCommonEventTwoTermBigOWith, and the aggregation below produces it through the abstract engine of Provider/Orlicz/CommonEventAggregation.lean. The two Orlicz terms stay separate and one-sided throughout: the two lanes are never merged.

The direction net

In the source the maximization is over one Euclidean unit vector, and convexity reduces it to a finite net at a dimensional cost. The reduction against this repository's carrier is in the companion module Provider/Homogenization/UnionDirectionNet.lean: on one probability-one event, simultaneously for every cutoff scale and every unit direction, the Section 3.5 response is at most 2 ^ d times the sum of its values at the d coordinate directions, hence at most 2 ^ d * d times one of them. The two deliberate deviations from that reduction --- the coordinate net in place of the sign vertices, and the cost 2 ^ d (or 2 ^ d * d) in place of d --- are recorded in that module's docstring, together with the two places inside the printed budget k = k1 + k2 <= C(d) |log epsilon| where the extra factor is absorbed: the fluctuation lanes by enlarging k2 (see exists_gridDecay_mul_le below), and the deterministic mean by running the finite-corridor iteration at epsilon / (2 ^ d * d). Enlarging k2 alone does not suffice: the direction net multiplies the mean term as well.

References

• ABK26, Proposition p.homogenization.step.
• ABK26, Appendix, the weak-Orlicz notation and the Gamma_sigma triangle inequality.

The geometry of the cutoff family

The grid gain 3 ^ (-d k / 2) of the concentration display is geometric in the relative depth k, which is what makes the infinite cutoff family summable.

theorem Algsuperdiff.Section3.Provider.Homogenization.gridDecay_add (d k j : ℕ) : gridDecay d (k + j) = gridDecay d k * gridDecay d j

The grid gain is multiplicative in the relative depth.

theorem Algsuperdiff.Section3.Provider.Homogenization.gridDecay_eq_pow (d j : ℕ) : gridDecay d j = gridDecay d 1 ^ j

The grid gain is the geometric sequence of ratio 3 ^ (-d/2).

theorem Algsuperdiff.Section3.Provider.Homogenization.gridDecay_le_one (d k : ℕ) : gridDecay d k ≤ 1

The grid gain never exceeds one.

theorem Algsuperdiff.Section3.Provider.Homogenization.gridDecay_lt_one {d : ℕ} (hd : 0 < d) : gridDecay d 1 < 1

In every genuine dimension the geometric ratio is strictly below one.

theorem Algsuperdiff.Section3.Provider.Homogenization.summable_const_mul_gridDecay_add {d : ℕ} (hd : 0 < d) (k : ℕ) (c : ℝ) : Summable fun (j : ℕ) => c * gridDecay d (k + j)

The shifted grid gains are summable.

theorem Algsuperdiff.Section3.Provider.Homogenization.tsum_const_mul_gridDecay_add {d : ℕ} (hd : 0 < d) (k : ℕ) (c : ℝ) : ∑' (j : ℕ), c * gridDecay d (k + j) = c * gridDecay d k * (1 - gridDecay d 1)⁻¹

The exact geometric sum of the shifted grid gains. This is the single extra dimensional factor (1 - 3 ^ (-d/2))^{-1} paid by the infinite cutoff family.

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_gridDecay_mul_le {d : ℕ} (hd : 0 < d) {c epsilon : ℝ} (hc : 0 < c) (hepsilon : 0 < epsilon) : ∃ (k : ℕ), c * gridDecay d k ≤ epsilon ∧ ↑k ≤ 1 + |2 * Real.log (c / epsilon) / (↑d * Real.log 3)|

The separation selection of ABK26. For every positive target epsilon there is an integer separation k making the grid gain absorb any prescribed positive constant, and the separation may be chosen of the printed logarithmic size k <= 1 + |2 log(c / epsilon) / (d log 3)|.

The manuscript writes this as k2 = ceil(log_3(10 epsilon^{-1})) and then records k = k1 + k2 <= C |log epsilon| in the last sentence of the proof.

The cutoff family of ABK26

def Algsuperdiff.Section3.Provider.Homogenization.unionCutoffScale (m : ℤ) (k1 k2 j : ℕ) : ℤ

The cutoff scale L_j = m - k1 - k2 - j of the j-th member of the family summed at ABK26: the printed range is L <= m - k with k = k1 + k2.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.unionCutoffScale m k1 k2 j = m - ↑k1 - ↑k2 - ↑j

def Algsuperdiff.Section3.Provider.Homogenization.unionObservationScale (m : ℤ) (k2 j : ℕ) : ℤ

The observation scale n_j = L_j + k1 chosen in ABK26, at which the grid 3 ^ n Z^d cap square_m is taken.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.unionObservationScale m k2 j = m - ↑k2 - ↑j

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.unionGridAverage {d : ℕ} (M : ABKModel d) (m : ℤ) (k1 k2 j : ℕ) (e : HCPolySupport.Vec d) : Cutoff.CutoffSample d → ℝ

The j-th member of the family aggregated at ABK26: the absolute recentred grid average over 3 ^ (n_j) Z^d cap square_m, written at the relative depth m - n_j = k2 + j.

Equations

• One or more equations did not get rendered due to their size.

The aggregated display

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_unionGridAverageCommonEnvelope (d : ℕ) : ∃ (Cunion : ℝ), 0 < Cunion ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), (∀ k ≤ m - 1, ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M k ⟨s, ⋯⟩) (↑E * s⁻¹ * √M.gamma) (s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹)))) → 1 / 16 ∈ Set.Icc (8 * M.gamma) 1 → ∀ (k1 k2 : ℕ), 1 ≤ k1 + k2 → ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → Probability.IsCommonEventTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (fun (j : ℕ) => unionGridAverage M m k1 k2 j e) (Cunion * (↑E ^ 2 * M.gamma) * gridDecay d k2) (Cunion * Real.exp (-(2 * (↑E)⁻¹ ^ 3 * M.gamma⁻¹)) * gridDecay d k2)

The Section 3.5 cutoff-union display on one common event.

Fix a unit direction e, as ABK26 does throughout, and two integer separations k1 and k2 with 1 <= k1 + k2. From the preceding-error clause of the Section 3.5 statement, the recentred grid averages of ABK26, taken at the cutoffs L_j = m - k1 - k2 - j and the observation scales n_j = L_j + k1, admit one pair of measurable envelopes dominating every member of the infinite family on a single event of probability one, with a Gamma_1 amplitude proportional to E^2 gamma and a Gamma_{1/4} amplitude proportional to exp(-2 E^{-3} gamma^{-1}), both carrying the separation gain 3 ^ (-d k2 / 2). The proportionality constant depends only on d.

The Gamma_{1/4} amplitude carries the exponent 2 where print exp(-E^{-3} gamma^{-1}). The frozen Section 3.5 conclusion asks for exactly this amplitude.

The gain 3 ^ (-d k2 / 2) is where the factor epsilon of the printed right-hand side comes from: it is made as small as desired by enlarging k2, which is the printed choice k2 = ceil(log_3(10 epsilon^{-1})).

The two-lane transport, the per-site producers, the grid concentration engine and the countable envelope selection are all consumed, not re-derived. This is a Provider endpoint and carries no source-node status by itself.