PositiveMassGerm.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform positive chance of early mass, together with the Brownian germ law, gives mass before every positive time. The scaling estimate needed to apply this lemma is kept explicit.

lemma OAI.SLEExactGauge.earlyMassGerm_tail line 16

theorem OAI.SLEExactGauge.positive_mass_all_times_of_uniform_probability line 29

Source documentation

This is the zero-one step of the canonical mass positivity argument. The lower bound will come from scaling a single nonzero compact mean.

theorem positive_mass_all_times_of_uniform_probability
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P) (hm : ∀ t, Measurable (B t))
    (hc : ∀ ω, Continuous (fun t => B t ω)) (h0 : ∀ ω, B 0 ω=0)
    (Z : ℝ≥0 → Ω → ℝ≥0∞)
    (hZ : Adapted (Filtration.natural B (fun t => (hm t).stronglyMeasurable)) Z)
    (hmono : ∀ᵐ ω ∂P, Monotone (fun t => Z t ω))
    (ε : ℕ → ℝ≥0) (hεanti : Antitone ε) (hε : Tendsto ε atTop (𝓝 0))
    (p : ℝ≥0∞) (hp : 0<p) (hprob : ∀ n, p ≤ P {ω | 0<Z (ε n) ω}) :
    ∀ᵐ ω ∂P, ∀ t : ℝ≥0, 0<t → 0<Z t ω := by
…