const_inner — Mathlib

English

For a linear equivalence L, integrability of φ is equivalent to integrability of L(φ).

Русский

Для линейного эквивалента L интегрируемость φ эквивалентна интегрируемости L(φ).

LaTeX

$$$ \\operatorname{Integrable}(\\phi,\\mu) \\iff \\operatorname{Integrable}(x \\mapsto L(\\phi(x)),\\mu)$$$

Lean4

theorem const_inner (c : E) {f : α → E} (hf : MemLp f p μ) : MemLp (fun a => ⟪c, f a⟫) p μ :=
  hf.of_le_mul (AEStronglyMeasurable.inner aestronglyMeasurable_const hf.1)
    (Eventually.of_forall fun _ => norm_inner_le_norm _ _)

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