setToL1SCLM_nonneg — Mathlib

English

If T maps nonnegative inputs to nonnegative outputs (on finite μ), then applying setToL1SCLM to a nonnegative simple function yields a nonnegative result.

Русский

Если T сохраняет неотрицательность, то для неотрицательного простого f результат неотрицателен.

LaTeX

$$$0 \le f \Rightarrow 0 \le setToL1SCLM\; α\; G'\; μ\; hT\; f$$$

Lean4

theorem setToL1SCLM_nonneg {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C)
    (hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) {f : α →₁ₛ[μ] G'} (hf : 0 ≤ f) :
    0 ≤ setToL1SCLM α G' μ hT f :=
  setToL1S_nonneg (fun _ => hT.eq_zero_of_measure_zero) hT.1 hT_nonneg hf

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