wInner_add_left — Mathlib

English

The conjugate of the weighted inner product equals the reverse inner product: conj ⟪f, g⟫ₙ_[𝕜,w] = ⟪g, f⟫ₙ_[𝕜,w].

Русский

Сопряжение взвешенного скалярного произведения равняется обратному скалярному произведению: conj ⟪f,g⟫ = ⟪g,f⟫.

LaTeX

$$$ \\overline{\\langle f, g \\rangle}_{𝕜,[w]} = \\langle g, f \\rangle_{𝕜,[w]} $$$

Lean4

theorem wInner_add_left (w : ι → ℝ) (f₁ f₂ g : ∀ i, E i) : ⟪f₁ + f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] + ⟪f₂, g⟫_[𝕜, w] := by
  simp [wInner, inner_add_left, smul_add, sum_add_distrib]

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