smul_neg

Mathlib.MeasureTheory.Function.Holder

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.smul_neg

English

Negating both factors leaves the Holder product unchanged: (-f)•(-g) = f•g.

Русский

Отрицание обоих факторов не меняет произведение Холдэра: (-f)•(-g) = f•g.

LaTeX

$$$(-f) \\cdot (-g) = f \\cdot g$ in Lp sense.$$

Lean4

@[simp]
protected theorem smul_neg (f : Lp 𝕜 p μ) (g : Lp E q μ) : f • -g = -(f • g) := by
  simp [eq_neg_iff_add_eq_zero, ← Lp.add_smul]

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

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

Разделы

Аффилиация

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