UnionCompletion

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

Completion of the Section 3.5 cutoff union

This module performs the last two steps of the cutoff-union argument of ABK26 (proof of p.homogenization.step): the passage from one fixed direction to all directions, and the final fold of constants into the shape of the Section 3.5 conclusion.

The proved endpoint exists_unionGridAverageCommonEnvelope (Provider/Homogenization/UnionAggregation.lean) aggregates the grid displays over the infinite cutoff family at one unit direction. The proved pointwise reduction ae_forall_cutoffResponseJ_le_directionNet (Provider/Homogenization/UnionDirectionNet.lean) reduces an arbitrary unit direction to the d coordinate directions at the cost 2 ^ d * d. What was missing between them is a countable family carrying all d coordinate directions at once, and the arithmetic that turns the two amplitudes into the printed epsilon E^2 gamma and epsilon exp(-2 E^{-3} gamma^{-1}).

The direction wiring, and the route chosen

The two admissible routes are: re-index the family by ℕ × Fin d, or replace each member by the finite sum over the d directions through the finite Gamma_sigma triangle. The route taken here is the re-indexing by ℕ × Fin d, realized without a Denumerable transport and without re-deriving the aggregation: the proved one-direction endpoint is consumed d times, once at each Pi.single i (1 : ℝ), and the d resulting common-event bounds are merged by the new abstract combinator isCommonEventTwoTermBigOWith_prod_of_fintype, whose two envelopes are the finite Finset.sup' of the given ones.

This keeps Probability.IsCommonEventTwoTermBigOWith exact --- one pair of measurable envelopes, one event of probability one, two separate one-sided tails, lanes never merged --- and the amplitudes C(d)-clean: the only price is one factor (3 max(1, log d))^{1/sigma} per lane, supplied by the proved finite-maximum estimate Orlicz.isBigOWith_gammaSigma_finset_sup'_of_nonempty, which is a constant depending on d alone and is absorbed into the module's Cunion. The alternative finite-sum route was not taken because it would pay a gammaTriangleConst per direction inside the countable aggregation and would require rebuilding the per-member two-term display.

The fold

exists_gridDecay_mul_le (UnionAggregation.lean) chooses the separation k2 so that the grid gain 3 ^ (-d k2 / 2) beats epsilon / 2 after the direction cost; k2 is then enlarged by one so that the printed corridor condition 1 <= k1 + k2 holds. epsilon is split in half between the two fluctuation lanes and the deterministic mean. Because the direction net multiplies the mean as well, the iteration is run at the shrunken tolerance epsilon / (2 ^ d * d), which is the second of the two absorption places recorded in the direction-net module. The deterministic mean is absorbed by isCommonEventTwoTermBigOWith_add_const and the amplitudes are relaxed to the printed ones by isCommonEventTwoTermBigOWith_mono_scale. The printed budget k = k1 + k2 <= C(d) |log epsilon| is discharged in union_budget_bound, against |log epsilon| >= log 2 >= 1/2, which is where epsilon <= 1/2 is used.

The constant Chom produced here is max 64 (max (Citer * 2^d d) (Citer + 1 + 2 Q)) with Q built from log(2 ^ d d), log Cunion and log 2; it is chosen before the model, the scale, the tolerance and the direction, and it unfolds to d, Cunion and the iteration's own constant only. All three occurrences of Chom in the Section 3.5 statement point the same way: enlarging it strengthens the smallness binder, shrinks the index set, and relaxes 1 <= Chom.

What fixes k1

ABK26 sets k1 := ceil(alpha^{-1} log_3(4 epsilon^{-1} C)) where alpha(d) and C(d) are the exponent and constant of the iterated recurrence e.iter.post. Neither alpha nor that C exists in this repository --- they are outputs of the separate node p.homogenization.step#iterate --- so k1 is not derived here. It is bound existentially, together with its budget, inside the single conditional A obligation below, in exactly the shape the iteration delivers.

Scope facts, inherited and disclosed

• The direction cost is 2 ^ d * d rather than the printed d: the coordinate net replaces the sign vertices. Both are C(d).
• The cutoff family deliberately omits the printed n <= m - 1: at k2 = j = 0 its observation scale is n = m. This strengthening is inherited from the proved two-lane transport.
• The two-sided IsBigO of the consumed envelope engine where the printed statement is one-sided, the (3 ^ d + 1) ^ d colour stride, the CoarseGraining gammaTriangleConst centering constant, and the numerals 1/16 and 1/8 are all inherited from the consumed statements, not introduced here.

The data are M : ABKModel d, together with d, m, E, k1, k2, epsilon, Chom, the abstract carriers of the two combinators, and the meanBound slot of the domination lemma. The only numerals fixed by hand are the two numerals already fixed by the proved transport.

References

• ABK26, Proposition p.homogenization.step, proof; in particular the choices k1, k2, k = k1 + k2 and n = L + k1, the post-iteration display e.iter.post.new, the union bound e.union.bound.fluct, the subadditivity and final absorption, and the budget.
• ABK26, Appendix.

Two further pieces of the common-event two-term A

theorem Algsuperdiff.Section3.Provider.Homogenization.isCommonEventTwoTermBigOWith_const_mul {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {I : Type u_2} {Psi1 Psi2 : ℝ → ℝ} {X : I → Omega → ℝ} {A1 A2 c : ℝ} (hc : 0 < c) (hX : Probability.IsCommonEventTwoTermBigOWith mu Psi1 Psi2 X A1 A2) : Probability.IsCommonEventTwoTermBigOWith mu Psi1 Psi2 (fun (i : I) (omega : Omega) => c * X i omega) (c * A1) (c * A2)

A common-event two-term bound scales by a positive constant: both amplitudes are multiplied by it, and the two envelopes are multiplied by it as well, so the single domination event is unchanged.

theorem Algsuperdiff.Section3.Provider.Homogenization.isCommonEventTwoTermBigOWith_prod_of_fintype {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {I : Type u_2} {J : Type u_3} [MeasureTheory.IsFiniteMeasure mu] [Fintype J] [Nonempty J] {sigmaOne sigmaTwo : ℝ} (hsigmaOne : 0 < sigmaOne) (hsigmaTwo : 0 < sigmaTwo) {W : J → I → Omega → ℝ} {A1 A2 : ℝ} (hW : ∀ (b : J), Probability.IsCommonEventTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigmaOne) (HCPolySupport.IndependentSums.gammaSigma sigmaTwo) (W b) A1 A2) : Probability.IsCommonEventTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigmaOne) (HCPolySupport.IndependentSums.gammaSigma sigmaTwo) (fun (p : I × J) => W p.2 p.1) ((3 * max 1 (Real.log ↑(Fintype.card J))) ^ sigmaOne⁻¹ * A1) ((3 * max 1 (Real.log ↑(Fintype.card J))) ^ sigmaTwo⁻¹ * A2)

Merging finitely many common-event two-term bounds.

Given one common-event two-term bound for each member of a finite nonempty family, at one common pair of amplitudes, the whole product family carries a single common-event two-term bound. The two envelopes are the finite maxima of the given ones, and the amplitudes pay the finite-maximum weak-Orlicz cost (3 max(1, log N))^{1/sigma} of Provider/Orlicz/Maximum.lean.

Only one further null set is spent, namely the finite intersection of the given domination events; the index of the inner family stays inside the event.

The union family carrying all d coordinate directions

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_unionGridAverageAllDirectionsCommonEnvelope (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 → Probability.IsCommonEventTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (fun (p : ℕ × Fin d) => unionGridAverage M m k1 k2 p.1 (Pi.single p.2 1)) (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, at all d coordinate directions at once.

The proved endpoint exists_unionGridAverageCommonEnvelope holds one unit direction fixed. Applying it at each of the d coordinate directions and merging the d resulting common-event bounds by isCommonEventTwoTermBigOWith_prod_of_fintype re-indexes the family by ℕ × Fin d, at the cost of one factor (3 max(1, log d))^{1/sigma} on each lane, which is a constant depending only on d and is absorbed into Cunion.

Nothing in the proved endpoint is re-derived: it is consumed d times.

The pointwise domination of the Section 3.5 response family

theorem Algsuperdiff.Section3.Provider.Homogenization.ae_forall_cutoffResponseJ_le_unionGridAverageAllDirections {d : ℕ} (M : ABKModel d) (m : ℤ) (k1 k2 : ℕ) (hsep : 1 ≤ k1 + k2) (Chom epsilon meanBound : ℝ) (hbudget : ↑k1 + ↑k2 ≤ Chom * |Real.log epsilon|) (hmean : ∀ L ≤ m - 1, L + ↑k1 ≤ m → ∀ (b : Fin d), ∫ (omega : Cutoff.CutoffSample d), Observable.cutoffResponseJ M (L + ↑k1) L (Pi.single b 1) omega ∂↑(Cutoff.cutoffSampleLaw M) ≤ meanBound) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (i : { p : ℤ × { v : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm v = 1 } // ↑p.1 ≤ ↑m - Chom * |Real.log epsilon| }), ∃ (p : ℕ × Fin d), Observable.cutoffResponseJ M m (↑i).1 (↑(↑i).2) omega ≤ 2 ^ d * ↑d * unionGridAverage M m k1 k2 p.1 (Pi.single p.2 1) omega + 2 ^ d * ↑d * meanBound

The composed pointwise domination.

On one probability-one event, simultaneously for every admissible cutoff scale L and every Euclidean unit direction, the Section 3.5 response at the parent cube square_m is bounded by 2 ^ d * d times one member of the all-directions union family, shifted by 2 ^ d * d times the mean bound.

The budget hypothesis hbudget is what converts the printed separation `L <= m

• kwithk = k1 + k2into the frozen statement's own restrictionL <= m - Chom |log epsilon|`.

Two null sets are spent beyond those of the consumed statements: the direction net's single event, and the countable intersection over ℤ × Fin d of the recentred subadditivity events. The uncountable direction quantifier stays inside the event.

The constant fold

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_isCommonEventTwoTermBigOWith_cutoffResponseJ_of_iterateMeanBound (d : ℕ) (hIter : ∃ (Citer : ℝ), 1 ≤ Citer ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), 15 * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → (∀ 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⁻¹)))) → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), M.gamma ≤ Citer⁻¹ * (↑E)⁻¹ ^ 2 * epsilon → ∃ (k1 : ℕ), ↑k1 ≤ Citer * |Real.log epsilon| ∧ ∀ (n L : ℤ), L ≤ m - 1 → L + ↑k1 ≤ n → n ≤ m → ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → ∫ (omega : Cutoff.CutoffSample d), Observable.cutoffResponseJ M n L e omega ∂↑(Cutoff.cutoffSampleLaw M) ≤ 2⁻¹ * epsilon * ↑E ^ 2 * M.gamma) : ∃ (Chom : ℝ), 1 ≤ Chom ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), 15 * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → (∀ 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⁻¹)))) → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), M.gamma ≤ Chom⁻¹ * (↑E)⁻¹ ^ 2 * epsilon → Probability.IsCommonEventTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (fun (i : { p : ℤ × { e : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm e = 1 } // ↑p.1 ≤ ↑m - Chom * |Real.log epsilon| }) => Observable.cutoffResponseJ M m (↑i).1 ↑(↑i).2) (epsilon * ↑E ^ 2 * M.gamma) (epsilon * Real.exp (-(2 * (↑E)⁻¹ ^ 3 * M.gamma⁻¹)))

The Section 3.5 cutoff-union conclusion, conditional on the iterate mean bound.

The fold is the last paragraph of the printed proof. The separation k2 is chosen by exists_gridDecay_mul_le so that the grid gain 3 ^ (-d k2 / 2) beats one half of epsilon; epsilon is split evenly between the two fluctuation lanes and the deterministic mean; the mean is absorbed by isCommonEventTwoTermBigOWith_add_const and the amplitudes are relaxed by isCommonEventTwoTermBigOWith_mono_scale. The direction cost 2 ^ d d of the net multiplies the mean as well, which is why the iteration is run at epsilon / (2 ^ d d); both increments stay inside the printed budget k1 + k2 <= Chom |log epsilon|, which is discharged here by union_budget_bound.

The window evaluation 1/16 in [8 gamma, 1] required by the proved transport is derived, not assumed: the frozen smallness binder gamma <= Chom^{-1} E^{-2} epsilon with Chom >= 64, E >= 1 and epsilon <= 1/2 gives gamma <= 1/128. The manuscript's own route (a lower bound on E from 15 c_star^{-1} <= E together with an upper bound on c_star, whence 8 gamma < 1/16) is available here — the proved Provider.Disorder.cstar_le_three_halves gives E >= 10 and 8 gamma <= 8 * 10^{-10} < 1/16; only the literal c_star <= 1 is absent. The derivation from the smallness binder is taken instead because it needs no new import; the two regime binders 15 c_star^{-1} <= E and gamma <= E^{-10} are passed unchanged to hIter, which is where the printed proof uses them.

This is a Provider result and carries no source-node status by itself.