English
If T is a bound-operator with respect to μ real, then the norm bound for integrable f holds in the displayed form.
Русский
Если T ограниченное по μ real, то выполняется представленная граница нормы для интегрируемого f.
LaTeX
$$$ \|setToSimpleFunc T f\| \le \text{(bound)} \cdot \sum_{x \in f.range} \mu.real(f^{-1}({x})) \cdot \|x\| $$$
Lean4
theorem norm_setToSimpleFunc_le_sum_mul_norm_of_integrable (T : Set α → E →L[ℝ] F') {C : ℝ}
(hT_norm : ∀ s, MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s) (f : α →ₛ E) (hf : Integrable f μ) :
‖f.setToSimpleFunc T‖ ≤ C * ∑ x ∈ f.range, μ.real (f ⁻¹' { x }) * ‖x‖ :=
calc
‖f.setToSimpleFunc T‖ ≤ ∑ x ∈ f.range, ‖T (f ⁻¹' { x })‖ * ‖x‖ := norm_setToSimpleFunc_le_sum_opNorm T f
_ ≤ ∑ x ∈ f.range, C * μ.real (f ⁻¹' { x }) * ‖x‖ :=
by
refine Finset.sum_le_sum fun b hb => ?_
obtain rfl | hb := eq_or_ne b 0
· simp
gcongr
exact hT_norm _ (SimpleFunc.measurableSet_fiber _ _) <| SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hb
_ ≤ C * ∑ x ∈ f.range, μ.real (f ⁻¹' { x }) * ‖x‖ := by simp_rw [mul_sum, ← mul_assoc]; rfl
