Theorems · Theorem · probability
MeasureTheory.upcrossingsBefore_lt_of_exists_upcrossing
∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω},
a < b →
∀ {N₁ N₂ : ℕ},
N ≤ N₁ →
f N₁ ω < a →
N₁ ≤ N₂ →
b < f N₂ ω → MeasureTheory.upcrossingsBefore a b f N ω < MeasureTheory.upcrossingsBefore a b f (N₂ + 1) ω- Cited by
- 1 results in Mathlib
- Foundations
- Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- LE.le.transproof · cited by 3,151
- LT.lt.leproof · cited by 2,189
- le_reflproof · cited by 2,061
- le_rflproof · cited by 1,558
- le_transproof · cited by 985
- lt_of_lt_of_leproof · cited by 438
- Set.mem_ofPred_eqproof · cited by 122
- bot_eq_zero'proof · cited by 92
- le_csSupproof · cited by 66
- MeasureTheory.upperCrossingTimeproof · cited by 42
- MeasureTheory.upcrossingsBeforestatement and proof · cited by 22
Cited by1
Results whose statement or proof uses this declaration.
- MeasureTheory.not_frequently_of_upcrossings_lt_topproof · cited by 2