condExpInd_nonneg — Mathlib

English

On the empty set, condExpInd is the zero map.

Русский

На пустом множестве condExpInd — тождественный нулю отображатель.

LaTeX

$$$ condExpInd\; G\; hm\; μ\; \varnothing = 0,$$

Lean4

theorem condExpInd_nonneg {E} [NormedAddCommGroup E] [PartialOrder E] [NormedSpace ℝ E] [IsOrderedModule ℝ E]
    (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E) (hx : 0 ≤ x) : 0 ≤ condExpInd E hm μ s x :=
  by
  rw [← coeFn_le]
  refine EventuallyLE.trans_eq ?_ (condExpInd_ae_eq_condExpIndSMul hm hs hμs x).symm
  exact (coeFn_zero E 1 μ).trans_le (condExpIndSMul_nonneg hs hμs x hx)

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