Cauchy–Schwarz for a positive functional

theorem Orthogonalization.norm_map_star_mul_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) (x y : H →L[ℂ] H) : ‖φ (star x * y)‖ ≤ √(φ (star x * x)).re * √(φ (star y * y)).re

Cauchy–Schwarz inequality for a positive linear functional, in the form |φ (x* y)| ≤ ‖x‖_φ ‖y‖_φ.

The proof is Mathlib's GNS construction: φ becomes a PositiveLinearMap and x, y ↦ φ (star x * y) is then the (semi-definite) inner product of PositiveLinearMap.PreGNS, whose Cauchy–Schwarz inequality is norm_inner_le_norm.

theorem Orthogonalization.sq_norm_map_star_mul_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) (x y : H →L[ℂ] H) : ‖φ (star x * y)‖ ^ 2 ≤ (φ (star x * x)).re * (φ (star y * y)).re

Cauchy–Schwarz inequality for a positive linear functional, squared form: |φ (x* y)|² ≤ φ (x* x) φ (y* y) (real parts; the values on x* x are real by positivity, see Orthogonalization.im_eq_zero_of_nonneg).

theorem Orthogonalization.re_map_star_mul_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) (x y : H →L[ℂ] H) : (φ (star x * y)).re ≤ √(φ (star x * x)).re * √(φ (star y * y)).re

The real part of φ (x* y) is bounded by ‖x‖_φ ‖y‖_φ.

The squared seminorm of a tuple

noncomputable def Orthogonalization.phiNormSq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) {ι : Type u_2} [Fintype ι] (b : ι → H →L[ℂ] H) : ℝ

The square of the seminorm ‖(b_i)‖_φ = √(∑ i, φ (b_i* b_i)) of a tuple of operators, as a real number (the values φ (b_i* b_i) are real by positivity of φ; no positivity hypothesis is needed for the definition since we take real parts).

Equations

• Orthogonalization.phiNormSq φ b = ∑ i : ι, (φ (star (b i) * b i)).re

theorem Orthogonalization.phiNormSq_def {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} {ι : Type u_2} [Fintype ι] (b : ι → H →L[ℂ] H) : phiNormSq φ b = ∑ i : ι, (φ (star (b i) * b i)).re

Unfolding lemma for phiNormSq.

theorem Orthogonalization.phiNormSq_eq_re_map_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} {ι : Type u_2} [Fintype ι] (b : ι → H →L[ℂ] H) : phiNormSq φ b = (φ (∑ i : ι, star (b i) * b i)).re

phiNormSq is the real part of φ applied to the single operator ∑ i, b_i* b_i; this is the form in which the conclusion of Theorem 1.2 is stated.

@[simp]

theorem Orthogonalization.phiNormSq_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} {ι : Type u_2} [Fintype ι] : phiNormSq φ 0 = 0

theorem Orthogonalization.phiNormSq_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} {ι : Type u_2} [Fintype ι] (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) (b : ι → H →L[ℂ] H) : 0 ≤ phiNormSq φ b

The squared seminorm of a tuple is nonnegative.

theorem Orthogonalization.re_map_star_add_mul_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} {ι : Type u_2} (b c : ι → H →L[ℂ] H) (i : ι) : (φ (star ((b + c) i) * (b + c) i)).re = (φ (star (b i) * b i)).re + (φ (star (b i) * c i)).re + (φ (star (c i) * b i)).re + (φ (star (c i) * c i)).re

Expansion of the squared seminorm of a sum, coordinatewise.

theorem Orthogonalization.phiNormSq_add_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} {ι : Type u_2} [Fintype ι] (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) (b c : ι → H →L[ℂ] H) : √(phiNormSq φ (b + c)) ≤ √(phiNormSq φ b) + √(phiNormSq φ c)

Triangle inequality for the seminorm ‖·‖_φ of tuples: ‖b + c‖_φ ≤ ‖b‖_φ + ‖c‖_φ.

The proof expands ‖b + c‖_φ², bounds each cross term by Cauchy–Schwarz for φ and then sums with the discrete Cauchy–Schwarz inequality Real.sum_sqrt_mul_sqrt_le.

theorem Orthogonalization.phiNormSq_add_le_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} {ι : Type u_2} [Fintype ι] (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) {b c : ι → H →L[ℂ] H} {ε : ℝ} (hb : phiNormSq φ b ≤ ε) (hc : phiNormSq φ c ≤ ε) : phiNormSq φ (b + c) ≤ 4 * ε

The triangle inequality in the form used downstream: if each of b and c has squared seminorm at most ε, then b + c has squared seminorm at most 4 ε.

theorem Orthogonalization.phiNormSq_add_add_lt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} {ι : Type u_2} [Fintype ι] (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) {b c d : ι → H →L[ℂ] H} {ε : ℝ} (hε : 0 < ε) (hb : phiNormSq φ b ≤ ε) (hc : phiNormSq φ c ≤ ε) (hd : phiNormSq φ d < ε) : phiNormSq φ (b + c + d) < 9 * ε

The three-term estimate. If b and c have squared seminorm at most ε and d has squared seminorm strictly less than ε, then b + c + d has squared seminorm strictly less than 9 ε. This is exactly how the constant 9 of Theorem 1.2 arises from three applications of the triangle inequality.