Api #

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

The consumption A of the frozen good event `𝒢(m, y; s, ε)` #

Algsuperdiff.Frozen.Section4.goodEventAt (d.good.event.for.lambda) is a final frozen definition: the translated good event is the Cutoff.translateCutoffSample y preimage of the Section 4 support layer's goodEventBase. This module supplies the operations on it used below:

measure it — measurableSet_goodEventAt;
compare two of them — monotonicity in the coarse-ellipticity constant Ccg and in the threshold ε (and hence in the 𝒢₁ threshold s ε c⋆^{1/2} γ^{-1/2}, which is increasing in ε).

What is not here #

Monotonicity in the scale m is not stated, and none is claimed in either direction. 𝒢₀(m) weights the k-supremum by 3^{-γ(m-k)/4} and ranges z over the annulus □_m ∖ □_k; 𝒢₁'s second condition weights by 3^{-s(m-n)/4} and its first condition sums from k = m; 𝒢₂'s double sum is over j ≤ m. Changing m moves the weights and the index sets at once, so nothing here is a set inclusion in m; any m-comparison a lane needs is a per-display estimate, to be produced where it is used.

References #

ABK26, d.good.event.for.lambda; e.lambda.good.events.

1. The `𝒢₁` threshold of `e.lambda.good.events` #

goodEventBase instantiates 𝒢₁'s threshold at T = s ε √c⋆ (√γ)⁻¹. Its two sign facts are used by every monotonicity statement below, so they are isolated once.

source

noncomputable def Algsuperdiff.Section4.Provider.GoodEvents.goodEventThreshold {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (ep : ℝ) :

ℝ

The 𝒢₁ threshold s ε √c⋆ (√γ)⁻¹ of e.lambda.good.events.

Equations

Algsuperdiff.Section4.Provider.GoodEvents.goodEventThreshold M s ep = ↑s * ep * √(Algsuperdiff.Section3.Disorder.cstar M) * (√M.gamma)⁻¹

Instances For

source

theorem Algsuperdiff.Section4.Provider.GoodEvents.goodEventThreshold_nonneg {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {ep : ℝ} (hep : 0 ≤ ep) :

0 ≤ goodEventThreshold M s ep

The threshold is nonnegative as soon as the printed ε is.

source

theorem Algsuperdiff.Section4.Provider.GoodEvents.goodEventThreshold_mono {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {ep ep' : ℝ} (h : ep ≤ ep') :

goodEventThreshold M s ep ≤ goodEventThreshold M s ep'

The threshold is monotone in ε.

2. Membership and measurability #

source

theorem Algsuperdiff.Section4.Provider.GoodEvents.goodEventAt_eq_preimage {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) (y : HCPolySupport.Vec d) (s : { s : ℝ // 0 < s }) (ep : ℝ) :

Frozen.Section4.goodEventAt M Ccg m y s ep = Section3.Cutoff.translateCutoffSample y ⁻¹' Support.goodEventBase M Ccg m s ep

The frozen event is a translate preimage, by definition.

source

theorem Algsuperdiff.Section4.Provider.GoodEvents.measurableSet_goodEventAt {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (m : ℤ) (y : HCPolySupport.Vec d) (s : { s : ℝ // 0 < s }) (ep : ℝ) :

MeasurableSet (Frozen.Section4.goodEventAt M Ccg m y s ep)

The translated event is measurable. The support layer's measurability transported through the proved measurability of translateCutoffSample.

4. Monotonicity in the two displayed parameters #

source

theorem Algsuperdiff.Section4.Provider.GoodEvents.goodEventBase_subset_of_le {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) {Ccg Ccg' ep ep' : ℝ} (hC : Ccg ≤ Ccg') (hep : 0 ≤ ep) (heple : ep ≤ ep') :

Support.goodEventBase M Ccg m s ep ⊆ Support.goodEventBase M Ccg' m s ep'

Monotonicity of the untranslated event. Raising the coarse-ellipticity constant lowers 𝒢₀'s positive parts, and raising ε raises both 𝒢₁'s threshold and 𝒢₂'s.

source