Theorems · Theorem · probability

MeasureTheory.stoppedValue_sub_eq_sum

∀ {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ π : Ω → ℕ∞} [inst : AddCommGroup β],
  τ ≤ π →
    (∀ (ω : Ω), ↑(π ω) ≠ ⊤) →
      MeasureTheory.stoppedValue u π - MeasureTheory.stoppedValue u τ = fun ω =>
        (∑ i ∈ Finset.Ico (WithTop.untopA (τ ω)) (WithTop.untopA (π ω)), (u (i + 1) - u i)) ω

Defined in: Mathlib.Probability.Process.Stopping
Cited by: 1 results in Mathlib
Foundations: Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites14

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

AddCommGroupstatement and proof · cited by 12,871
ENNRealstatement · cited by 9,879
Top.topstatement and proof · cited by 9,680
Finset.sumstatement and proof · cited by 5,195
ENatstatement and proof · cited by 4,985
Finset.rangeproof · cited by 1,341
Finset.Icostatement · cited by 450
ENat.toENNRealstatement and proof · cited by 103
MeasureTheory.stoppedValuestatement and proof · cited by 51
WithTop.untopAstatement and proof · cited by 37
sub_sub_sub_cancel_rightproof · cited by 34
Finset.sum_range_subproof · cited by 15

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.stoppedValue_sub_eq_sum'proof · cited by 1