English
If f is integrable with respect to μ and hf supplies a relationship on the complement of s, then the auxiliary identity relates the restricted expectation of s.indicator f to s.indicator of μ[f|m].
Русский
Если f интегрируем по μ и выполняется зависимость на дополнение к s, то вспомогательное тождество устанавливает связь между CondExp для s.indicator f и s.indicator CondExp f.
LaTeX
$$$$ \\mu[\\,s.\\mathrm{indicator} f|m\\] =_{μ} s.indicator (\\mu[f|m]) $$$$
Lean4
theorem condExpIndSMul_nonneg {E} [NormedAddCommGroup E] [PartialOrder E] [NormedSpace ℝ E] [IsOrderedModule ℝ E]
[SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E) (hx : 0 ≤ x) :
(0 : α → E) ≤ᵐ[μ] condExpIndSMul hm hs hμs x :=
by
refine EventuallyLE.trans_eq ?_ (condExpIndSMul_ae_eq_smul hm hs hμs x).symm
filter_upwards [condExpL2_indicator_nonneg hm hs hμs] with a ha
exact smul_nonneg ha hx
