English
For f ∈ Lp and any scalar c, restricting c·f to s and coeFn commute with the Lp structure: the restricted Lp of c·f equals c times the restricted Lp of f.
Русский
Для f ∈ Lp и любого скаляра c ограничение c·f до s и копирование коFn сохранены: ограниченная Lp-функция c·f равна c умноженному ограничению f.
LaTeX
$$$$((Lp.memLp (c \\cdot f)).restrict s).toLp (\\,c \\cdot f) = c \\cdot ((Lp.memLp f).restrict s).toLp f$$$$
Lean4
theorem simpleFunc_mul (g : SimpleFunc X ℝ) (hf : Integrable f μ) : Integrable (⇑g * f) μ :=
by
refine
SimpleFunc.induction (fun c s hs => ?_)
(fun g₁ g₂ _ h_int₁ h_int₂ => (h_int₁.add h_int₂).congr (by rw [SimpleFunc.coe_add, add_mul])) g
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero,
Set.piecewise_eq_indicator]
have : Set.indicator s (Function.const X c) * f = s.indicator (c • f) :=
by
ext1 x
by_cases hx : x ∈ s
· simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul, ← Function.const_def]
· simp only [hx, Pi.mul_apply, Set.indicator_of_notMem, not_false_iff, zero_mul]
rw [this, integrable_indicator_iff hs]
exact (hf.smul c).integrableOn
