re — Mathlib · SciLib

English

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

Русский

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

LaTeX

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

Lean4

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

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