norm_setToSimpleFunc_le_integral_norm

English

If T bounds a linear map on sets with a uniform bound, then the norm of f.setToSimpleFunc T is controlled by a constant times the integral of the norm of f.

Русский

Если T задаёт ограничение на линейный переходник на множества и существует константа, то нормa f.setToSimpleFunc T ограничена константой, умноженной на интеграл нормы f.

LaTeX

$$$$ \\|f.setToSimpleFunc T\\| \\leq C \\cdot (f.map \\; \\|\\cdot\\|)_{\\text{integral}} μ $$$$

Lean4

theorem norm_setToSimpleFunc_le_integral_norm (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 * (f.map norm).integral μ :=
  calc
    ‖f.setToSimpleFunc T‖ ≤ C * ∑ x ∈ f.range, μ.real (f ⁻¹' { x }) * ‖x‖ :=
      norm_setToSimpleFunc_le_sum_mul_norm_of_integrable T hT_norm f hf
    _ = C * (f.map norm).integral μ := by rw [map_integral f norm hf norm_zero]; simp_rw [smul_eq_mul]

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