add_compLp — Mathlib

English

The operator of composing with L distributes over addition: (L+L') ∘ f = (L ∘ f) + (L' ∘ f) in L^p.

Русский

Операция композиции с L распределена по сложению: (L+L')∘f = (L∘f) + (L'∘f) в L^p.

LaTeX

$$$ (L+L')\\circ f = (L\\circ f) + (L'\\circ f) \\quad \\text{in } L^p(E,p,\\mu) \\text{ for } f\\in L^p(E,p,\\mu).$$$

Lean4

theorem add_compLp (L L' : E →SL[σ] F) (f : Lp E p μ) : (L + L').compLp f = L.compLp f + L'.compLp f :=
  by
  ext1
  grw [Lp.coeFn_add, coeFn_compLp']
  refine EventuallyEq.trans ?_ (EventuallyEq.fun_add (L.coeFn_compLp' f).symm (L'.coeFn_compLp' f).symm)
  filter_upwards with x
  rw [coe_add', Pi.add_def]

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