condExpL1_mono — Mathlib

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

Похожие утверждения