Theorems · Theorem · probability

MeasureTheory.mul_upcrossingsBefore_le

∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω},
  a ≤ f N ω →
    a < b →
      (b - a) * ↑(MeasureTheory.upcrossingsBefore a b f N ω) ≤
        ∑ k ∈ Finset.range N, MeasureTheory.upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω

Defined in: Mathlib.Probability.Martingale.Upcrossing
Cited by: 1 results in Mathlib
Foundations: Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites51

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setproof · cited by 53,352
Realstatement and proof · cited by 25,697
Finsetproof · cited by 13,712
Finset.sumstatement and proof · cited by 5,195
one_mulproof · cited by 2,841
Finset.sum_congrproof · cited by 2,323
mul_commproof · cited by 2,262
MulZeroClass.mul_zeroproof · cited by 2,091
le_reflproof · cited by 2,061
Finset.rangestatement and proof · cited by 1,341
sub_selfproof · cited by 996
le_transproof · cited by 985

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.integral_mul_upcrossingsBefore_le_integralproof · cited by 1