im — Mathlib · SciLib

English

If f ∈ MemLp, then its imaginary part lies in MemLp.

Русский

Если f ∈ MemLp, то мнимая часть f принадлежит MemLp.

LaTeX

$$$$\\text{MemLp}(f, p, μ) \\Rightarrow \\text{MemLp}(\\operatorname{Im} f, p, μ).$$$$

Lean4

theorem im (hf : MemLp f p μ) : MemLp (fun x => RCLike.im (f x)) p μ :=
  by
  have : ∀ x, ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖ := by
    intro x
    rw [one_mul]
    exact RCLike.norm_im_le_norm (f x)
  refine hf.of_le_mul ?_ (Eventually.of_forall this)
  exact RCLike.continuous_im.comp_aestronglyMeasurable hf.1

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