condExpL1CLM_smul — Mathlib

English

If x ≥ 0 in E, then condExpInd is nonnegative: condExpInd E hm μ s x ≥ 0.

Русский

Если x ≥ 0, то condExpInd неотрицательно.

LaTeX

$$$ 0 \leq condExpInd\; E\; hm\; μ\; s\; x, \quad x \ge 0,$$

Lean4

theorem condExpL1CLM_smul (c : 𝕜) (f : α →₁[μ] F') : condExpL1CLM F' hm μ (c • f) = c • condExpL1CLM F' hm μ f :=
  by
  refine L1.setToL1_smul (dominatedFinMeasAdditive_condExpInd F' hm μ) ?_ c f
  exact fun c s x => condExpInd_smul' c x

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