UnionConcentration

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

Finite-range concentration for cube-local families at the genuine cutoff law

ABK26 states, immediately after Proposition p.concentration, the spatial corollary used in the proof of Proposition p.homogenization.step: if the family {X_z}_{z ∈ 3^n ℤ^d ∩ □_m} is centered, each member is O_{Γ_σ}(K), and two members are independent whenever the corresponding subcubes do not touch, then the average over the grid is O_{Γ_σ}(^{-d(m-n)/2} K).

This module proves a strengthened-hypothesis form of that corollary on the genuine cutoff sample law Cutoff.cutoffSampleLaw M, for families whose members read only the integral-local information of their own cube tree. Three steps:

1. Finite range. Cutoff.indep_cutoffSampleLocalSigma_of_indep_completion together with Cutoff.indep_lowerShellLocalCompletion_of_cutoff_separation already give the two-set independence of the cutoff-sample local σ-fields of two Euclidean-separated regions. IndepChain's statements are tied to Percolation.siteSigma, which is generated by set-valued events and cannot express these comap σ-fields, so the induction is repeated here rather than reused; see also Percolation.ColoredConcentration, which Section Concentration mirrors for the same reason.

2. Colouring. Section Concentration runs the residue colouring of Percolation.Coloring at range 3 ^ sepShift d, applies CoarseGraining's centered independent-sum inequality inside each colour class, and recombines the classes with CoarseGraining's finite-average triangle inequality. This mirrors Percolation.ColoredConcentration, whose σ-fields are generated by set-valued bad events and therefore cannot carry a real-valued functional of the coefficient field.

3. Grid form. Section Grid specializes the site set to the lattice points Percolation.cubeFinset (m - n) of □_m at spacing 3 ^ n, i.e. to 3^n ℤ^d ∩ □_m, where the recombined amplitude is literally C(d, σ) · 3 ^ (-d(m-n)/2) · K, and assembles two lanes into the Probability.IsTwoTermBigOWith shape used by the Section 3.5 frozen statements.

References

• ABK26, Proposition p.concentration and its spatial corollary.
• ABK26, Proposition p.homogenization.step.

Independence

theorem Algsuperdiff.Section3.Provider.Homogenization.siteRegion_mono {d : ℕ} (base : ℤ) {S T : Set (Fin d → ℤ)} (hST : S ⊆ T) : Percolation.siteRegion base S ⊆ Percolation.siteRegion base T

The observation region of a site family is monotone in the site set.

theorem Algsuperdiff.Section3.Provider.Homogenization.indep_cutoffSampleLocalSigma_siteRegion_of_latDist_sep {d : ℕ} (M : ABKModel d) {L n : ℤ} (hLn : L ≤ n) (S T : Set (Fin d → ℤ)) (hsep : ∀ u ∈ S, ∀ v ∈ T, 3 ^ Percolation.sepShift d < Percolation.latDist u v) : ProbabilityTheory.Indep (Cutoff.cutoffSampleLocalSigma M L (Percolation.siteRegion n S)) (Cutoff.cutoffSampleLocalSigma M L (Percolation.siteRegion n T)) ↑(Cutoff.cutoffSampleLaw M)

The two-set finite-range input at the genuine cutoff law.

Two site families at sup-lattice separation more than 3 ^ sepShift d, read at cube scale n, generate integral-local information of the cutoff a_L on two regions whose Euclidean separation is at least the literal cutoff range √d · 3 ^ L, provided L ≤ n. The proved cutoff range theorem then supplies the independence. Nothing is assumed beyond the standing model.

theorem Algsuperdiff.Section3.Provider.Homogenization.iIndepFun_of_measurable_cutoffSampleLocalSigma_siteRegion {d : ℕ} (M : ABKModel d) {L n : ℤ} (hLn : L ≤ n) {ι : Type u_1} {z : ι → Fin d → ℤ} {X : ι → Cutoff.CutoffSample d → ℝ} (hsep : ∀ (i j : ι), i ≠ j → 3 ^ Percolation.sepShift d < Percolation.latDist (z i) (z j)) (hX : ∀ (i : ι), Measurable (X i)) : ProbabilityTheory.iIndepFun X ↑(Cutoff.cutoffSampleLaw M)

The iIndepFun form. Random variables on the genuine cutoff sample space that read only the integral-local information of the cutoff a_L on the cube tree of their own site are mutually independent as soon as the sites are pairwise separated at range 3 ^ sepShift d. This is the hypothesis format consumed by the ABK26 concentration inequality.

Concentration

theorem Algsuperdiff.Section3.Provider.Homogenization.isBigO_gammaSigma_siteSum_of_cubeLocal_centered {d : ℕ} (M : ABKModel d) {L n : ℤ} (hLn : L ≤ n) {S : Finset (Fin d → ℤ)} {sig K : ℝ} (hsep : ∀ u ∈ S, ∀ v ∈ S, u ≠ v → 3 ^ Percolation.sepShift d < Percolation.latDist u v) (hS : S.Nonempty) (hsig0 : 0 < sig) (hsig2 : sig ≤ 2) (hK : 0 < K) {X : (Fin d → ℤ) → Cutoff.CutoffSample d → ℝ} (hXloc : ∀ u ∈ S, Measurable (X u)) (hXmeas : ∀ (u : Fin d → ℤ), Measurable (X u)) (hXtail : ∀ u ∈ S, HCPolySupport.IndependentSums.IsBigO (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sig) (X u) K) (hXmean : ∀ u ∈ S, ∫ (omega : Cutoff.CutoffSample d), X u omega ∂↑(Cutoff.cutoffSampleLaw M) = 0) : HCPolySupport.IndependentSums.IsBigO (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sig) (fun (omega : Cutoff.CutoffSample d) => ∑ u ∈ S, X u omega) (HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst sig * √↑S.card * K)

Concentration on a pairwise separated family of cube sites.

For centered random variables that read only the integral-local information of the cutoff a_L on their own cube tree, and whose sites are pairwise separated in the lattice at range 3 ^ sepShift d, the finite-range property of the genuine cutoff upgrades to mutual independence and ABK26's Proposition p.concentration applies verbatim.

theorem Algsuperdiff.Section3.Provider.Homogenization.isBigO_gammaSigma_siteAverage_of_cubeLocal_centered {d : ℕ} (M : ABKModel d) {L n : ℤ} (hLn : L ≤ n) {S : Finset (Fin d → ℤ)} {sig K : ℝ} (hS : S.Nonempty) (hsig0 : 0 < sig) (hsig2 : sig ≤ 2) (hK : 0 < K) {X : (Fin d → ℤ) → Cutoff.CutoffSample d → ℝ} (hXloc : ∀ u ∈ S, Measurable (X u)) (hXmeas : ∀ (u : Fin d → ℤ), Measurable (X u)) (hXtail : ∀ u ∈ S, HCPolySupport.IndependentSums.IsBigO (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sig) (X u) K) (hXmean : ∀ u ∈ S, ∫ (omega : Cutoff.CutoffSample d), X u omega ∂↑(Cutoff.cutoffSampleLaw M) = 0) : HCPolySupport.IndependentSums.IsBigO (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sig) (fun (omega : Cutoff.CutoffSample d) => (↑S.card)⁻¹ * ∑ u ∈ S, X u omega) (HCPolySupport.IndependentSums.gammaTriangleConst sig * HCPolySupport.Book.Ch04.gammaSigmaIndependentSumConst sig * (√(min ↑((3 ^ Percolation.sepShift d + 1) ^ d) ↑S.card) * (√↑S.card / ↑S.card)) * K)

The colouring corollary at the genuine cutoff law, in averaged form.

This is ABK26's spatial corollary of Proposition p.concentration for the actual cutoff coefficient field: the average over a finite family of cube sites of centered cube-local O_{Γ_σ}(K) variables is O_{Γ_σ} at the scale C(σ) √(colourCount) (√(#S) / #S) K. The colour count is min ((3 ^ sepShift d + 1) ^ d) (#S), so the estimate degrades gracefully to the deterministic triangle inequality on small site families.

Grid

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.gridConcentrationConst (d : ℕ) (sig : ℝ) : ℝ

The dimensional constant of the grid concentration estimate: the colouring cost √((3 ^ sepShift d + 1) ^ d) times CoarseGraining's triangle and independent-sum constants.

The choice sepShift d = d inherited from Percolation.SiteFamilyBridge makes the colour count (3 ^ d + 1) ^ d (100 at d = 2, 21952 at d = 3). ABK26's corollary writes C(σ); the d-dependence is intrinsic to any colouring realization of that corollary.

Equations

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

theorem Algsuperdiff.Section3.Provider.Homogenization.gridConcentrationConst_pos {d : ℕ} {sig : ℝ} (hsig : 0 < sig) : 0 < gridConcentrationConst d sig

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.gridDecay (d k : ℕ) : ℝ

The manuscript's grid gain 3 ^ (-d k / 2) at relative depth k.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.gridDecay d k = 3 ^ (-↑(d * k) / 2)

theorem Algsuperdiff.Section3.Provider.Homogenization.gridDecay_pos (d k : ℕ) : 0 < gridDecay d k

theorem Algsuperdiff.Section3.Provider.Homogenization.sqrt_card_div_card_cubeFinset {d : ℕ} (k : ℕ) : √↑(Percolation.cubeFinset k).card / ↑(Percolation.cubeFinset k).card = gridDecay d k

The lattice points of □_m at spacing 3 ^ n, i.e. ABK26's index set 3 ^ n ℤ^d ∩ □_m written at relative depth k = m - n, carry the exact grid gain √(#S) / #S = 3 ^ (-d k / 2).

theorem Algsuperdiff.Section3.Provider.Homogenization.isBigO_gammaSigma_gridAverage_of_cubeLocal_centered {d : ℕ} (M : ABKModel d) {L n : ℤ} (hLn : L ≤ n) (k : ℕ) {sig K : ℝ} (hsig0 : 0 < sig) (hsig2 : sig ≤ 2) (hK : 0 < K) {X : (Fin d → ℤ) → Cutoff.CutoffSample d → ℝ} (hXloc : ∀ u ∈ Percolation.cubeFinset k, Measurable (X u)) (hXmeas : ∀ (u : Fin d → ℤ), Measurable (X u)) (hXtail : ∀ u ∈ Percolation.cubeFinset k, HCPolySupport.IndependentSums.IsBigO (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sig) (X u) K) (hXmean : ∀ u ∈ Percolation.cubeFinset k, ∫ (omega : Cutoff.CutoffSample d), X u omega ∂↑(Cutoff.cutoffSampleLaw M) = 0) : HCPolySupport.IndependentSums.IsBigO (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sig) (fun (omega : Cutoff.CutoffSample d) => (↑(Percolation.cubeFinset k).card)⁻¹ * ∑ u ∈ Percolation.cubeFinset k, X u omega) (gridConcentrationConst d sig * K * gridDecay d k)

The Section 3.5 grid concentration estimate at the genuine cutoff law.

For every unit-free family indexed by the grid 3 ^ n ℤ^d ∩ □_m whose members are centered, cube-local for the cutoff a_L, and O_{Γ_σ}(K), the grid average is O_{Γ_σ}(C(d, σ) K 3 ^ (-d(m-n)/2)).

theorem Algsuperdiff.Section3.Provider.Homogenization.isTwoTermBigOWith_gridAverage_of_twoLane {d : ℕ} (M : ABKModel d) {L n : ℤ} (hLn : L ≤ n) (k : ℕ) {K₁ K₄ : ℝ} (hK₁ : 0 < K₁) (hK₄ : 0 < K₄) {X Y Z : (Fin d → ℤ) → Cutoff.CutoffSample d → ℝ} (hsplit : ∀ u ∈ Percolation.cubeFinset k, ∀ (omega : Cutoff.CutoffSample d), X u omega = Y u omega + Z u omega) (hYloc : ∀ u ∈ Percolation.cubeFinset k, Measurable (Y u)) (hYmeas : ∀ (u : Fin d → ℤ), Measurable (Y u)) (hYtail : ∀ u ∈ Percolation.cubeFinset k, HCPolySupport.IndependentSums.IsBigO (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (Y u) K₁) (hYmean : ∀ u ∈ Percolation.cubeFinset k, ∫ (omega : Cutoff.CutoffSample d), Y u omega ∂↑(Cutoff.cutoffSampleLaw M) = 0) (hZloc : ∀ u ∈ Percolation.cubeFinset k, Measurable (Z u)) (hZmeas : ∀ (u : Fin d → ℤ), Measurable (Z u)) (hZtail : ∀ u ∈ Percolation.cubeFinset k, HCPolySupport.IndependentSums.IsBigO (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (Z u) K₄) (hZmean : ∀ u ∈ Percolation.cubeFinset k, ∫ (omega : Cutoff.CutoffSample d), Z u omega ∂↑(Cutoff.cutoffSampleLaw M) = 0) : Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (fun (omega : Cutoff.CutoffSample d) => |(↑(Percolation.cubeFinset k).card)⁻¹ * ∑ u ∈ Percolation.cubeFinset k, X u omega|) (gridConcentrationConst d 1 * K₁ * gridDecay d k) (gridConcentrationConst d (1 / 4) * K₄ * gridDecay d k)

The two-lane grid display.

If the grid family splits pointwise into a Γ_1 lane and a Γ_{1/4} lane, each centered and cube-local for the cutoff a_L, then the absolute grid average satisfies the one-sided two-term weak-Orlicz relation of the ABK26 Appendix at the two amplitudes C(d,1) K₁ 3 ^ (-d k / 2) and C(d,1/4) K₄ 3 ^ (-d k / 2).