English
A norm bound for setToSimpleFunc: the norm of f.setToSimpleFunc T is bounded by the sum of norms of T(preimage of x) acting on x, over x in the range of f, i.e., ≤ ∑ ||T(preimage {x})||·||x||.
Русский
Граница нормы для setToSimpleFunc: нормa f.setToSimpleFunc T не превышает сумму норм T(preimage {x})·||x|| по x из диапазона f.
LaTeX
$$$\|f.setToSimpleFunc T\| \le \sum_{x \in f.range} \|T(f^{-1}(\{x\}))\| \cdot \|x\|$$$
Lean4
theorem setToSimpleFunc_mono [IsOrderedAddMonoid G'] {T : Set α → G' →L[ℝ] G''} (h_add : FinMeasAdditive μ T)
(hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) {f g : α →ₛ G'} (hfi : Integrable f μ)
(hgi : Integrable g μ) (hfg : f ≤ g) : setToSimpleFunc T f ≤ setToSimpleFunc T g :=
by
rw [← sub_nonneg, ← setToSimpleFunc_sub T h_add hgi hfi]
refine setToSimpleFunc_nonneg' T hT_nonneg _ ?_ (hgi.sub hfi)
intro x
simp only [coe_sub, sub_nonneg, coe_zero, Pi.zero_apply, Pi.sub_apply]
exact hfg x
