Positive measure above zero implies positive measure above some strictly positive level

Proved

AvramDividend.Classical.positive_measure_positive_real_tail_contains_positive_level

by WillR · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

avram-dividendfirst-passagemeasure-theorypositive-thresholdprobability

For an arbitrary measure and real-valued function, positive measure of the event f>0 implies the existence of a strictly positive deterministic threshold ε with positive measure of f>ε. This uses countable continuity via the reciprocal thresholds 1/(n+1) and countable subadditivity, with no measurability assumption on f. The lemma is a reusable bridge from the newly Proved positive-upward-increment event to crossing a strictly positive level, relevant to two-sided first passage.

Preamble

import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
import Mathlib.Algebra.Order.Archimedean.Basic
import Mathlib.MeasureTheory.Measure.MeasureSpace
import Mathlib.Tactic.Positivity

open AvramDividend.Classical MeasureTheory Set
open scoped ENNReal

Formal statement

theorem AvramDividend.Classical.positive_measure_positive_real_tail_contains_positive_level
    {Ω : Type*} [MeasurableSpace Ω]
    (μ : MeasureTheory.Measure Ω) (f : Ω → ℝ)
    (hpos : 0 < μ {ω : Ω | 0 < f ω}) :
    ∃ ε : ℝ, 0 < ε ∧ 0 < μ {ω : Ω | ε < f ω} := by sorry

Source

Mathlib exists_nat_one_div_lt, measure_iUnion_le and measure_mono.

View graph