setToL1_mono — Mathlib

English

If hTT' holds pointwise and sets are finite, then for all simple f the inequality setToL1 hT f ≤ setToL1 hT' f holds.

Русский

Если по каждой точке T ≤ T', то для всех простых функций f выполняется неравенство setToL1 hT f ≤ setToL1 hT' f.

LaTeX

$$$setToL1\, h_T\, f \leq setToL1\, h_T'\, f,$$$

Lean4

theorem setToL1_mono [IsOrderedAddMonoid G'] {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) :
    setToL1 hT f ≤ setToL1 hT g := by
  rw [← sub_nonneg] at hfg ⊢
  rw [← (setToL1 hT).map_sub]
  exact setToL1_nonneg hT hT_nonneg hfg

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