Young's inequality for inner products #
In an inner product space over 𝕜 = ℝ or ℂ, for every weight ε > 0,
2 re ⟪x, y⟫ ≤ ε ‖x‖² + ε⁻¹ ‖y‖².
This is the inner-product form of Mathlib's weighted Young inequality two_mul_le_add_mul_sq,
obtained from it through the Cauchy-Schwarz inequality re ⟪x, y⟫ ≤ ‖x‖ ‖y‖. It is the form used
to absorb a cross term into a positive quadratic term, as in energy estimates for elliptic
equations with first-order terms.
Main declarations #
TauCeti.two_mul_re_inner_le_add_mul_norm_sq: the weighted Young inequality above.
theorem
TauCeti.two_mul_re_inner_le_add_mul_norm_sq
{𝕜 : Type u_1}
{F : Type u_2}
[RCLike 𝕜]
[SeminormedAddCommGroup F]
[InnerProductSpace 𝕜 F]
(x y : F)
{ε : ℝ}
(hε : 0 < ε)
:
Young's inequality for inner products: for every weight ε > 0,
2 re ⟪x, y⟫ ≤ ε ‖x‖² + ε⁻¹ ‖y‖².