CombineBadEvent

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

The observation-scale bad-event estimate

The two source displays

With delta_1 = 10^9 E^2 gamma, this module proves, at the observation scale m and for every cutoff L < m,

• P[B_m] <= C(d) delta_1^2, and
• E[J(cu_{m-1}, p, q; a_L) 1_{B_m}] <= C(d) delta_1^2,

where B_m is the complement of the good event e.goodevent.combine, read at the halved discount and exponent q = 2 (see below).

Route

The heart of the argument -- the observation-scale fourth-moment transport of the preceding-error clause, i.e. the weighted-depth split at scale L, the coarse descendant averages controlled by the generalized Gamma_{1/4} triangle inequality, the finite-maximum cost C(1 + log N)^4, and the geometrically summable fine tail -- is already proved as observationScaleFiniteCover_sq_isBigOWith_gammaQuarter, which transports the lower clause from the cutoff cube at discount 1/16 to the observation cube at discount 1/8 with a dimension-only constant. This module

• collapses the resulting two-term amplitude to the single scale C(d) E^2 gamma using the regime fact gamma <= E^{-10} (the rare amplitude exp(-2 E^{-3} gamma^{-1}) is dominated by E^2 gamma; see exp_neg_sq_le_of_regime);
• converts that Gamma_{1/4} control into the fourth moment E[mathcal E_{1/8, infinity, 2}(cu_m; a_L, sigmabar_L)^4] <= C(d) (E^2 gamma)^2;
• concludes both displays by Markov's inequality and the a.e. directional domination J <= mathcal E^2 of ResponseCommonDomination.lean.

The good event carried here

observationScaleBadEvent is the complement of e.goodevent.combine at the printed discount s = 1/4 and printed exponent q = 1, written in the Section 3 inverse convention on the proved measurable observables:

B_m = {sigmabar_L^{-1} Lambda_{1/4,1}(cu_m; a_L) <= 2 and sigmabar_L lambda_{1/4,1}^{-1}(cu_m; a_L) <= 2}^c.

mem_observationScaleBadEvent_iff certifies that this is, at every sample point, the complement of the printed three-clause event {sigmabar_L / 2 <= lambda_{1/4,1} <= Lambda_{1/4,1} <= 2 sigmabar_L}: the middle clause is a theorem (lambdaSq_le_LambdaSq_oneCube), and the outer two transpose because the lower multiscale ellipticity of the actual cutoff is strictly positive (Ch02.lambdaSq_finite_pos), so Lean's 0⁻¹ = 0 convention cannot separate the two readings.

The half-discount comparison used to reach the q = 2 envelope is sharp -- constant 1 -- because the two geometric weight families literally coincide: geometricWeight s q n = (1 - 3^{-s q}) 3^{-s q n} depends on (s, q) only through s q. It is therefore Jensen's inequality for the geometric probability weights, whose Jensen half is already inside CoarseGraining.

References

• ABK26, Step 4 of p.combine.under.S, and the good event e.goodevent.combine.

Elementary arithmetic

theorem Algsuperdiff.Section3.Provider.Homogenization.eighth_pos : 0 < 1 / 8

The halved discount t = s / 2 = 1/8 is positive. It is public so that consumers can spell the same observables as observationScaleBadEvent.

theorem Algsuperdiff.Section3.Provider.Homogenization.quarter_pos : 0 < 1 / 4

The printed discount s = 1/4 is positive.

The q = 1 to q = 2 half-discount comparison

Lambda_{s,1} <= Lambda_{s/2,2} and lambda_{s,1}^{-1} <= lambda_{s/2,2}^{-1},

is already proved as ErrorComparison.LambdaSq_finite_one_le_half_two and ErrorComparison.lambdaSq_finite_one_inv_le_half_two (Provider/ErrorComparison/HalfScaleExponentBridge.lean); it is consumed here, not re-derived.

The observation-scale bad event

def Algsuperdiff.Section3.Provider.Homogenization.exponentOne : CoarseEllipticityExponent

The admissible exponent q = 1, at which e.goodevent.combine is printed.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.exponentOne = Algsuperdiff.Section3.CoarseEllipticityExponent.finite ⟨1, Algsuperdiff.Section3.Provider.Homogenization.exponentOne._proof_1⟩

def Algsuperdiff.Section3.Provider.Homogenization.observationScaleBadEvent {d : ℕ} (M : ABKModel d) (L m : ℤ) : Set (Cutoff.CutoffSample d)

The observation-scale bad event B_m of Step 4: the complement of the good event e.goodevent.combine at the printed discount s = 1/4 and printed exponent q = 1, on the genuine cutoff family and in the Section 3 inverse convention.

mem_observationScaleBadEvent_iff certifies that this is exactly the complement of the printed three-clause event {sigmabar_L / 2 <= lambda_{1/4,1} <= Lambda_{1/4,1} <= 2 sigmabar_L}.

Equations

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

theorem Algsuperdiff.Section3.Provider.Homogenization.measurableSet_observationScaleBadEvent {d : ℕ} (M : ABKModel d) (L m : ℤ) : MeasurableSet (observationScaleBadEvent M L m)

The observation-scale bad event is measurable: both multiscale ellipticity observables are genuinely measurable.

theorem Algsuperdiff.Section3.Provider.Homogenization.mem_observationScaleBadEvent_iff {d : ℕ} [NeZero d] (M : ABKModel d) (L m : ℤ) (omega : Cutoff.CutoffSample d) : omega ∈ observationScaleBadEvent M L m ↔ ¬(↑(Annealed.sigmaBar M L) / 2 ≤ HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d m) (1 / 4) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) ∧ HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d m) (1 / 4) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) ≤ HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d m) (1 / 4) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) ∧ HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d m) (1 / 4) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 1) (Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) ≤ 2 * ↑(Annealed.sigmaBar M L))

Faithfulness certificate. The measurable carrier observationScaleBadEvent is exactly the complement of the literal printed good event e.goodevent.combine at s = 1/4, q = 1, evaluated on the genuine cutoff family. The two readings agree at every sample point because the lower multiscale ellipticity of the actual cutoff is strictly positive.

theorem Algsuperdiff.Section3.Provider.Homogenization.ae_error_ge_of_mem_observationScaleBadEvent {d : ℕ} [NeZero d] (M : ABKModel d) (L m : ℤ) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), omega ∈ observationScaleBadEvent M L m → 1 / 5 ≤ Observable.cutoffHomogenizationErrorRepresentative M L m (1 / 8) (Annealed.sigmaBar M L) omega

The bad-event inclusion. Almost surely, the observation-scale bad event is contained in the threshold event {mathcal E_{1/8, infinity, 2}(cu_m; a_L, sigmabar_L) >= 1/5}.

This is the upper half of l.mathcal.E.to.Lambdas at q = 2 together with the quadratic ellipticity gate; the threshold 1/5 is legitimate because the exact positive root is (sqrt 10 - sqrt 2) / 4 > 1/5.

The observation-scale fourth moment

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.badEventMomentConst : ℝ

The dimension-free moment constant of the second-moment extraction from Gamma_{1/4} control.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.badEventMomentConst = (HCPolySupport.IndependentSums.gammaMomentConst (1 / 4) * 2 ^ (1 / 4)⁻¹) ^ 2

Pure-real cores of the probabilistic steps

Each of these keeps the heavy measurable carriers out of the arithmetic tactics; they are applied to the observation-scale error by exact.

Step 4

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_relativeCutoff_observationScale_badEvent_bound (d : ℕ) : ∃ (Chom : ℝ) (Cbad : ℝ), 64 ≤ Chom ∧ 1 ≤ Cbad ∧ ∀ (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 → ∀ L ≤ m - 2, have delta1 := 10 ^ 9 * ↑E ^ 2 * M.gamma; (↑(Cutoff.cutoffSampleLaw M)).real (observationScaleBadEvent M L m) ≤ Cbad * delta1 ^ 2 ∧ ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → ∫ (omega : Cutoff.CutoffSample d) in observationScaleBadEvent M L m, Observable.cutoffResponseJ M (m - 1) L e omega ∂↑(Cutoff.cutoffSampleLaw M) ≤ Cbad * delta1 ^ 2

With delta_1 = 10 ^ 9 * E ^ 2 * gamma, uniformly over the separation L <= m - 2 (which the frozen corridor L <= m - Chom |log epsilon| implies with roughly thirty scales of slack):

• the observation-scale bad event has probability at most C(d) delta_1 ^ 2;
• its response contribution E[J(cu_{m-1}, sigmabar_L^{-1/2} e, sigmabar_L^{1/2} e; a_L) 1_{B_m}] is at most C(d) delta_1 ^ 2, in every unit direction.

Both constants depend only on d. Finite-range concentration is not used.

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