memLp_re_im_iff — Mathlib

English

For K-valued functions, f ∈ L^p iff both Re f and Im f lie in L^p; the same holds in the real form.

Русский

Для функций, значение которых лежит в K, f ∈ L^p тогда и только тогда, когда Re f и Im f лежат в L^p.

LaTeX

$$$\\MemLp(f,p,\\mu) \\iff (\\MemLp(\\operatorname{Re}f,p,\\mu) \\land \\MemLp(\\operatorname{Im}f,p,\\mu)).$$$

Lean4

theorem _root_.MeasureTheory.memLp_re_im_iff {f : α → K} :
    MemLp (fun x ↦ RCLike.re (f x)) p μ ∧ MemLp (fun x ↦ RCLike.im (f x)) p μ ↔ MemLp f p μ :=
  by
  refine ⟨?_, fun hf => ⟨hf.re, hf.im⟩⟩
  rintro ⟨hre, him⟩
  convert MeasureTheory.MemLp.add (ε := K) hre.ofReal (him.ofReal.const_mul RCLike.I)
  ext1 x
  rw [Pi.add_apply, mul_comm, RCLike.re_add_im]

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