LowerFamily

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

One-sided lower-index-family weak-Orlicz bounds

This is the literal witness scope of the lower coarse-ellipticity estimate: one measurable random witness controls every integer cutoff at or above a specified lower index. It is not a collection of separately chosen tails.

References

• ABK26.
• ABK26.

structure Algsuperdiff.Section3.Probability.IsLowerIntegerFamilyOrliczWithWitness {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Ψ : ℝ → ℝ) (X : ℤ → Ω → ℝ) (L0 : ℤ) (b : ℝ) (Y : Ω → ℝ) (A : ℝ) : Prop

A single measurable witness for a lower-indexed family of one-sided bounds.

The deterministic shift appears before the witness, and the witness is chosen before every integer index. Thus the relation is the source supremum bound, not a family of unrelated estimates. Every member of the controlled index range is required to be a measurable random variable.

• admissible : IsAdmissibleTail Ψ
• scale_pos : 0 < A
• measurable_observable (L : ℤ) : L0 ≤ L → Measurable (X L)
• measurable_witness : Measurable Y
• dominates (ω : Ω) (L : ℤ) : L0 ≤ L → X L ω ≤ b + Y ω
• tail : HCPolySupport.IndependentSums.IsBigOWith μ Ψ Y A

def Algsuperdiff.Section3.Probability.IsLowerIntegerFamilyOrlicz {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Ψ : ℝ → ℝ) (X : ℤ → Ω → ℝ) (L0 : ℤ) (b A : ℝ) : Prop

A lower-indexed source supremum bound with one common measurable witness.

Equations

• Algsuperdiff.Section3.Probability.IsLowerIntegerFamilyOrlicz μ Ψ X L0 b A = ∃ (Y : Ω → ℝ), Algsuperdiff.Section3.Probability.IsLowerIntegerFamilyOrliczWithWitness μ Ψ X L0 b Y A