setToL1_indicatorConstLp — Mathlib

English

If hT and hT' are dominated, and T ≤ T' pointwise on sets of finite measure, then setToL1 hT f ≤ setToL1 hT' f for all f ∈ L1.

Русский

Если hT и hT' доминируются и T s x ≤ T' s x для всех s, x и μ заданной меры, тогда для любого f ∈ L1 выполняется setToL1 hT f ≤ setToL1 hT' f.

LaTeX

$$$T \le T' \text{ pointwise; } f \in L^1(μ;E) \Rightarrow setToL1\, h_T\, f \le setToL1\, h_T'\, f.$$$

Lean4

theorem setToL1_indicatorConstLp (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s)
    (hμs : μ s ≠ ∞) (x : E) : setToL1 hT (indicatorConstLp 1 hs hμs x) = T s x :=
  by
  rw [← Lp.simpleFunc.coe_indicatorConst hs hμs x]
  exact setToL1_simpleFunc_indicatorConst hT hs hμs.lt_top x

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