RandomHsepAllLWaveEnvelope

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

One random-hsep wave event for every upper cutoff

The fixed-cutoff wave estimate cannot be union-bounded over all cutoff indices after selecting the random separation profile: doing that would charge the same hsep tail infinitely many times. This file performs the operations in the opposite order. For each deterministic separation profile it aggregates the wave failures at L₀ + r using the growing amplitude t + r; only then does it select the sample-dependent hsep profile through the existing finite random-index decomposition.

The resulting event controls every integer cutoff L ≥ L₀, has an explicit Gamma₂ price, and transports exactly under cutoff-sample stationarity. The common hsep tail occurs once in randomHsepAllLWavePrice.

def Algsuperdiff.Section3.Provider.Multiscale.allLWaveAmplitude (t : ℝ) (r : ℕ) : ℝ

The wave-envelope amplitude at cutoff depth r. Its linear growth makes the resulting Gamma₂ failure probabilities summable over r.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.allLWaveAmplitude t r = t + ↑r

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.allLWavePrice (t : ℝ) : ℝ

The geometric sum of the fixed-profile wave prices generated by allLWaveAmplitude.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.allLWavePrice t = 2 * (HCPolySupport.IndependentSums.gammaSigma 2 t)⁻¹ * (1 - Real.exp (-1))⁻¹

theorem Algsuperdiff.Section3.Provider.Multiscale.measureReal_exists_allLCubeSupBound_gt_le {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (hn : ℕ → ℕ) {L₀ : ℤ} (hnL₀ : n ≤ L₀) {t : ℝ} (ht : 1 ≤ t) : (↑(Cutoff.cutoffSampleLaw M)).real {omega : Cutoff.CutoffSample d | ∃ (r : ℕ) (k : ℕ), ∃ Q ∈ Whitney.whitneyLayer n hn k, whitneyWaveLayerScale M n hn k (L₀ + ↑r) * allLWaveAmplitude t r < Stream.cubeSupBound Q Q.scale (L₀ + ↑r) ↑omega} ≤ allLWavePrice t

For a deterministic Whitney profile, the probability of violating some wave envelope at some cutoff L₀ + r is at most allLWavePrice t.

def Algsuperdiff.Section3.Provider.Multiscale.randomHsepAllLWaveEnvelope {d : ℕ} (M : ABKModel d) (n : ℤ) (E b : ℝ) (k₀ : ℕ) (L₀ : ℤ) (t : ℝ) (omega : Cutoff.CutoffSample d) : Prop

The one-event literal wave envelope on every cutoff index L₀ + r, with amplitudes whose resulting failure prices are summable in r.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.randomHsepAllLWavePrice (sigma b : ℝ) (H : ℕ) (t : ℝ) : ℝ

The explicit price of the random-profile all-cutoff wave event. The separation tail is charged once, after all cutoff depths have been summed for each deterministic profile.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.measureReal_lt_hsep_le_of_gates {d : ℕ} (M : ABKModel d) {m : ℤ} {E sigma b : ℝ} (hd : 2 ≤ d) (hE : 1 ≤ E) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hEexp : Real.exp (Percolation.badClustersConst d / sigma) ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : Percolation.badClustersConst d / b ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) {H : ℕ} (hH : 1 ≤ H) : (↑(Cutoff.cutoffSampleLaw M)).real {omega : Cutoff.CutoffSample d | H < Percolation.hsep M m E b omega} ≤ Percolation.hsepTailConst sigma b * Real.exp (-3 ^ ((1 - sigma) * b * ↑H))

The tail of hsep with the four direct preliminary probability gates exposed, rather than the stronger packaged admissibility consequence used by the compatibility A.

theorem Algsuperdiff.Section3.Provider.Multiscale.measureReal_not_randomHsepAllLWaveEnvelope_le {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {n : ℤ} {E sigma b : ℝ} (hE : 1 ≤ E) (hS : Frozen.Section3.inductionState M (n - 1) ⟨E, hE⟩) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hEexp : Real.exp (Percolation.badClustersConst d / sigma) ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : Percolation.badClustersConst d / b ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) (k₀ : ℕ) {L₀ : ℤ} (hnL₀ : n ≤ L₀) {H : ℕ} (hH : 1 ≤ H) {t : ℝ} (ht : 1 ≤ t) : (↑(Cutoff.cutoffSampleLaw M)).real {omega : Cutoff.CutoffSample d | ¬randomHsepAllLWaveEnvelope M n E b k₀ L₀ t omega} ≤ randomHsepAllLWavePrice sigma b H t

The random-profile all-cutoff failure price. The wave failures are first summed over the cutoff depth for each deterministic profile, and the common hsep tail is then charged exactly once.

theorem Algsuperdiff.Section3.Provider.Multiscale.measurableSet_randomHsepAllLWaveEnvelope {d : ℕ} (M : ABKModel d) (n : ℤ) (E b : ℝ) (k₀ : ℕ) (L₀ : ℤ) (t : ℝ) : MeasurableSet {omega : Cutoff.CutoffSample d | randomHsepAllLWaveEnvelope M n E b k₀ L₀ t omega}

The all-cutoff random-profile wave event is measurable, so stationarity can transport its exact probability rather than only an outer bound.