add_smul — Mathlib

English

Smulgation in MeasureTheory.Lp expresses the product of an Lp function with an Lp function as an Lp function.

Русский

Определение умножения функций в Lp выражает произведение двух функций в Lp как новую функцию в Lp.

LaTeX

$$$f ∈ L^p, g ∈ L^q \\Rightarrow f • g ∈ L^r.$$$

Lean4

protected theorem add_smul (f : Lp 𝕜 p μ) (g₁ g₂ : Lp E q μ) : f • (g₁ + g₂) = f • g₁ + f • g₂ :=
  by
  simp only [smul_def, ← MemLp.toLp_add]
  apply MemLp.toLp_congr _ _ ?_
  filter_upwards [AEEqFun.coeFn_add g₁.val g₂.val] with x hx
  simp [hx, smul_add]

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