English
If f = g μ-almost everywhere, then condExpL1 hm μ f = condExpL1 hm μ g.
Русский
Если f = g μ-почти везде, тогда condExpL1 hm μ f = condExpL1 hm μ g.
LaTeX
$$$f =_{a.e.\ μ} g \Rightarrow condExpL1 hm μ f = condExpL1 hm μ g$$$
Lean4
theorem condExpL1_mono {E} [NormedAddCommGroup E] [PartialOrder E] [OrderClosedTopology E] [IsOrderedAddMonoid E]
[CompleteSpace E] [NormedSpace ℝ E] [IsOrderedModule ℝ E] {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ)
(hfg : f ≤ᵐ[μ] g) : condExpL1 hm μ f ≤ᵐ[μ] condExpL1 hm μ g :=
by
rw [coeFn_le]
have h_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x : E, 0 ≤ x → 0 ≤ condExpInd E hm μ s x := fun s hs hμs x hx =>
condExpInd_nonneg hs hμs.ne x hx
exact setToFun_mono (dominatedFinMeasAdditive_condExpInd E hm μ) h_nonneg hf hg hfg