setToL1SCLM_mono — Mathlib

English

If T ≤ T' pointwise, then the L1-transfer is monotone with respect to the simple function order.

Русский

Если T ≤ T' по точным значениям, то преобразование L1 монотонно по отношению к порядку простых функций.

LaTeX

$$$setToL1SCLM\;α\;E\;μ\;hT f ≤ setToL1SCLM\;α\;E\;μ\;hT' f$$$

Lean4

theorem setToL1SCLM_mono {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 : α →₁ₛ[μ] G'} (hfg : f ≤ g) :
    setToL1SCLM α G' μ hT f ≤ setToL1SCLM α G' μ hT g :=
  setToL1S_mono (fun _ => hT.eq_zero_of_measure_zero) hT.1 hT_nonneg hfg

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