setToSimpleFunc_smul_left' — Mathlib

English

A variant of smul-left: for any c, setToSimpleFunc (c • T) f = c • setToSimpleFunc T f.

Русский

Вариант слева от умножения на скаляр: setToSimpleFunc (c • T) f = c • setToSimpleFunc T f.

LaTeX

$$$ setToSimpleFunc (T) f = c \cdot setToSimpleFunc T f $$$

Lean4

theorem setToSimpleFunc_smul_left' (T T' : Set α → E →L[ℝ] F') (c : ℝ)
    (h_smul : ∀ s, MeasurableSet s → μ s < ∞ → T' s = c • T s) {f : α →ₛ E} (hf : Integrable f μ) :
    setToSimpleFunc T' f = c • setToSimpleFunc T f := by
  classical
  simp_rw [setToSimpleFunc_eq_sum_filter]
  suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (f ⁻¹' { x }) = c • T (f ⁻¹' { x })
    by
    rw [smul_sum]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx, ContinuousLinearMap.smul_apply]
  intro x hx
  refine h_smul (f ⁻¹' { x }) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
  rw [mem_filter] at hx
  exact hx.2

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