ofReal — Mathlib

English

For a function f: α → K with K a complex-like field, f ∈ L^p if and only if its real and imaginary parts are in L^p.

Русский

Для функции f: α → K, где K является комплексоподобным полем, f ∈ L^p тогда и только тогда, когда вещественная и мнимая части принадлежат L^p.

LaTeX

$$$f \\in L^p \\iff (\\operatorname{Re} f) \\in L^p \\ \\land \\ (\\operatorname{Im} f) \\in L^p.$$$

Lean4

theorem _root_.MeasureTheory.MemLp.ofReal {f : α → ℝ} (hf : MemLp f p μ) : MemLp (fun x => (f x : K)) p μ :=
  (@RCLike.ofRealCLM K _).comp_memLp' hf

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