norm_setToSimpleFunc_le_sum_opNorm

English

If there is a bound on the operator norm of T(s) by a constant C times μ.real(s), then the norm of f.setToSimpleFunc T is bounded by C times the sum of μ.real(f^{-1}({x}))·||x|| over x in the range of f.

Русский

Если существует предел нормы оператора T(s) ≤ C μ реального( s ), тогда норма f.setToSimpleFunc T ограничена суммой C μ.real(f^{-1}({x}))·||x||.

LaTeX

$$$\|f.setToSimpleFunc T\| \le \sum_{x\in f.range} C \cdot μ.real(f^{-1}(\{x\})) \cdot \|x\|$$$

Lean4

theorem norm_setToSimpleFunc_le_sum_opNorm {m : MeasurableSpace α} (T : Set α → F' →L[ℝ] F) (f : α →ₛ F') :
    ‖f.setToSimpleFunc T‖ ≤ ∑ x ∈ f.range, ‖T (f ⁻¹' { x })‖ * ‖x‖ :=
  calc
    ‖∑ x ∈ f.range, T (f ⁻¹' { x }) x‖ ≤ ∑ x ∈ f.range, ‖T (f ⁻¹' { x }) x‖ := norm_sum_le _ _
    _ ≤ ∑ x ∈ f.range, ‖T (f ⁻¹' { x })‖ * ‖x‖ := by refine Finset.sum_le_sum fun b _ => ?_;
      simp_rw [ContinuousLinearMap.le_opNorm]

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