inner_const — Mathlib

English

If f is MemLp and c is a fixed vector, then x ↦ ⟪f x, c⟫ is MemLp with the same p and μ.

Русский

Если f ∈ MemLp и фиксирован вектор c, то x ↦ ⟪f x, c⟫ ∈ MemLp с тем же p и μ.

LaTeX

$$$ \\operatorname{MemLp} f p \\mu \\Rightarrow \\operatorname{MemLp}(x \\mapsto \\langle f(x), c\\rangle) p \\mu$$$

Lean4

theorem inner_const {f : α → E} (hf : MemLp f p μ) (c : E) : MemLp (fun a => ⟪f a, c⟫) p μ :=
  hf.of_le_mul (c := ‖c‖) (AEStronglyMeasurable.inner hf.1 aestronglyMeasurable_const)
    (Eventually.of_forall fun x => by rw [mul_comm]; exact norm_inner_le_norm _ _)

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