StepThreeBadSet

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

t.regularity Step 3: the bad-scale set 𝓑_z, as a Finset

The target

𝓑_z := { j ∈ [n, m-1] ∩ ℤ  :  𝒢(j, z; ⅛s, ⅛ s δ^{1/2}) is not valid } .

Contents

• stepThreeGoodEvent — the Step-3 good event, named once so that the identification with the producer's own event is a rfl (stepThreeGoodEvent_eq_goodEventAt).
• stepThreeBadSet — 𝓑_z as a Finset ℤ, the Finset.filter of Finset.Icc n (m-1).
• mem_stepThreeBadSet_iff, stepThreeBadSet_subset_Icc — membership, and the inclusion into the counting window [n, m] of e.bad.scale.proportion.bound (whose sum runs to m, one scale beyond the set).
• measurableSet_mem_stepThreeBadSet, measurable_stepThreeBadSet_card — the measurability story: each scale's membership event is the complement of a measurable good event, and the cardinality is the corresponding finite sum of indicators, hence measurable. (: all downstream use is a.e., so no pointwise finiteness is claimed anywhere.)
• stepThreeBadSet_card_eq_sum, stepThreeBadSet_card_le_sum_Icc — the cardinality as the ℝ≥0∞ indicator sum, and its domination by the sum over the full counting window, which is the left half of e.bad.scale.proportion.bound.

References

• ABK26, t.regularity Step 3.
• ABK26, d.good.event.for.lambda.

1. The Step-3 good event

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepThreeGoodEvent {d : ℕ} (M : Section3.ABKModel d) (delta : ℝ) (j : ℤ) (z : HCPolySupport.Vec d) : Set (Section3.Cutoff.CutoffSample d)

The translated good event at the parameters of the third regularity step.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.stepThreeGoodEvent_eq_goodEventAt {d : ℕ} (M : Section3.ABKModel d) (delta : ℝ) (j : ℤ) (z : HCPolySupport.Vec d) : stepThreeGoodEvent M delta j z = Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) j z ⟨stepOneSEighth, stepOneSEighth_pos⟩ (stepOneSEighth * √delta)

The Step-3 good event IS the event of the frozen p.minimal.scale.separation.sec4 clause at the Step-1 parameters: the same goodEventAt at the same index s/8 and the same threshold (s/8)·δ^{1/2}.

2. The bad-scale set

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepThreeBadSet {d : ℕ} (M : Section3.ABKModel d) (delta : ℝ) (n m : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : Finset ℤ

The bad-scale set 𝓑_z: the scales of the window [n, m-1] at which the Step-3 good event fails.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepThreeBadSet M delta n m z omega = {j ∈ Finset.Icc n (m - 1) | omega ∉ Algsuperdiff.Section4.Provider.Regularity.stepThreeGoodEvent M delta j z}

theorem Algsuperdiff.Section4.Provider.Regularity.mem_stepThreeBadSet_iff {d : ℕ} (M : Section3.ABKModel d) (delta : ℝ) (n m : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (j : ℤ) : j ∈ stepThreeBadSet M delta n m z omega ↔ (n ≤ j ∧ j ≤ m - 1) ∧ omega ∉ stepThreeGoodEvent M delta j z

Membership in 𝓑_z.

theorem Algsuperdiff.Section4.Provider.Regularity.stepThreeBadSet_subset {d : ℕ} (M : Section3.ABKModel d) (delta : ℝ) (n m : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : stepThreeBadSet M delta n m z omega ⊆ Finset.Icc n (m - 1)

𝓑_z ⊆ [n, m-1].

theorem Algsuperdiff.Section4.Provider.Regularity.stepThreeBadSet_subset_Icc {d : ℕ} (M : Section3.ABKModel d) (delta : ℝ) (n m : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : stepThreeBadSet M delta n m z omega ⊆ Finset.Icc n m

𝓑_z ⊆ [n, m], the counting window of e.bad.scale.proportion.bound, and the form the iteration lemma's binder B ⊆ Finset.Icc n m wants.

4. The cardinality as an indicator sum

theorem Algsuperdiff.Section4.Provider.Regularity.stepThreeBadSet_card_eq_sum {d : ℕ} (M : Section3.ABKModel d) (delta : ℝ) (n m : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : ↑(stepThreeBadSet M delta n m z omega).card = ∑ j ∈ Finset.Icc n (m - 1), (stepThreeGoodEvent M delta j z)ᶜ.indicator (fun (x : Section3.Cutoff.CutoffSample d) => 1) omega

|𝓑_z| as the indicator sum over the window [n, m-1], in ℝ≥0∞ — the shape the frozen p.minimal.scale.separation.sec4 density clause carries.

theorem Algsuperdiff.Section4.Provider.Regularity.stepThreeBadSet_card_le_sum_Icc {d : ℕ} (M : Section3.ABKModel d) (delta : ℝ) (n m : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : ↑(stepThreeBadSet M delta n m z omega).card ≤ ∑ j ∈ Finset.Icc n m, (stepThreeGoodEvent M delta j z)ᶜ.indicator (fun (x : Section3.Cutoff.CutoffSample d) => 1) omega

The left half of e.bad.scale.proportion.bound: |𝓑_z| is at most the count of failures over the counting window [n, m] — the sum the frozen producer's density clause bounds.