English
For a finite measure μ and Submartingale f with respect to ℱ, Doob's upcrossing inequality in integrated form yields
Русский
Для конечной меры μ и субмартингейла f относительно ℱ справедливо интегральное неравенство Доуба для апк upcrossings.
LaTeX
$$ENNReal.ofReal (b - a) * ∫^{−}_{ω} upcrossings(a,b,f,ω) dμ ≤ ⨆ N, ∫^{−}_{ω} ENNReal.ofReal((f(N,ω) - a)^{+}) dμ$$
Lean4
@[simp]
theorem centralMoment_one [IsZeroOrProbabilityMeasure μ] : centralMoment X 1 μ = 0 :=
by
rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
· simp [centralMoment]
by_cases h_int : Integrable X μ
· rw [centralMoment_one' h_int]
simp
· simp only [centralMoment, Pi.sub_apply, pow_one]
have : ¬Integrable (fun x => X x - integral μ X) μ :=
by
refine fun h_sub => h_int ?_
have h_add : X = (fun x => X x - integral μ X) + fun _ => integral μ X := by ext1 x; simp
rw [h_add]
fun_prop
rw [integral_undef this]
