norm_setToSimpleFunc_le_sum_mul_norm

English

If f is integrable and T s has a bound by C μ.real(s), then the norm bound holds for f in the integrable setting.

Русский

Если f интегрируема и T s имеет верхнюю грань по C μ.real(s), тогда выполняется требование нормы в интегрируемом случае.

LaTeX

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

Lean4

theorem norm_setToSimpleFunc_le_sum_mul_norm (T : Set α → F →L[ℝ] F') {C : ℝ}
    (hT_norm : ∀ s, MeasurableSet s → ‖T s‖ ≤ C * μ.real s) (f : α →ₛ 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
      gcongr
      exact hT_norm _ <| SimpleFunc.measurableSet_fiber _ _
    _ ≤ C * ∑ x ∈ f.range, μ.real (f ⁻¹' { x }) * ‖x‖ := by simp_rw [mul_sum, ← mul_assoc]; rfl

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