English
A complex polarization identity relating the inner product of Ty and x to a linear combination of inner products of T applied to linear combinations of x and y.
Русский
Комплексная поляризационная формула, связывающая скалярное произведение ⟪T y, x⟫ с линейной комбинацией скалярных произведений T примененного к линейным сочетаниям x и y.
LaTeX
$$$ \langle T y, x \rangle = \frac{\langle T(x+y), x+y \rangle - \langle T(x-y), x-y \rangle + i\langle T(x+i\,y), x+i\,y \rangle - i\langle T(x - i\,y), x - i\,y \rangle}{4}. $$$
Lean4
theorem bounded_below (coercive : IsCoercive B) : ∃ C, 0 < C ∧ ∀ v, C * ‖v‖ ≤ ‖B♯ v‖ :=
by
rcases coercive with ⟨C, C_ge_0, coercivity⟩
refine ⟨C, C_ge_0, ?_⟩
intro v
by_cases h : 0 < ‖v‖
· refine (mul_le_mul_iff_left₀ h).mp ?_
calc
C * ‖v‖ * ‖v‖ ≤ B v v := coercivity v
_ = ⟪B♯ v, v⟫_ℝ := (continuousLinearMapOfBilin_apply B v v).symm
_ ≤ ‖B♯ v‖ * ‖v‖ := real_inner_le_norm (B♯ v) v
· have : v = 0 := by simpa using h
simp [this]
