wInner_one_eq_inner

Mathlib.Analysis.RCLike.Inner

URI: https://scilib.ai/kg/mathlib#RCLike.wInner_one_eq_inner

English

The norm of the inner product satisfies the standard inequality with the product of norms, i.e., |⟪f, g⟫⟫ ≤ ⟪|f|, |g|⟫.

Русский

Неравенство модуля скалярного произведения: |⟪f,g⟫| ≤ ⟪|f|, |g|⟫.

LaTeX

$$‖⟪f,g⟫⟖ ≤ ⟪|f|, |g|⟫$$

Lean4

theorem wInner_one_eq_inner (f g : ι → 𝕜) : ⟪f, g⟫_[𝕜, 1] = ⟪WithLp.toLp 2 f, WithLp.toLp 2 g⟫_𝕜 := by
  simp [PiLp.inner_apply, wInner]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru