LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.InnerProductSpace.Basic

`norm_inner_div_norm_mul_norm_eq_one_iff` theorem norm_inner_div_norm_mul_norm_eq_one_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖⟪x, y⟫_𝕜 / (↑‖x‖ * ↑‖y‖)‖ = 1 ↔ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x This theorem states that for any two vectors `x` and `y` in an inner product space over a field `𝕜`, the absolute value of their inner product divided by the product of their norms equals to 1 if and only if `x` is nonzero and there exists a nonzero scalar `r` such that `y` equals `r` multiplied by `x`. This is one version of the equality case for the Cauchy-Schwarz inequality. More concisely: For any inner product space over a field and nonzero vectors `x` and `y`, the equality in the Cauchy-Schwarz inequality, i.e., \|\| = \|‖x‖⋅‖y‖\|, holds if and only if `y` is a scalar multiple of `x`.
`InnerProductSpace.add_left` theorem InnerProductSpace.add_left : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [self : InnerProductSpace 𝕜 E] (x y z : E), ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜 This theorem states that the inner product operation in an inner product space is additive in the first coordinate. More specifically, for any field `𝕜` and for any normed additive commutative group `E` (which together form an inner product space), the inner product of the sum of two elements `x` and `y` with a third element `z`, denoted by `⟪x + y, z⟫_𝕜`, equals the sum of the inner product of `x` with `z` and the inner product of `y` with `z`, denoted by `⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜`. In other words, the inner product preserves the addition operation in the first coordinate. More concisely: In an inner product space, the inner product of the sum of two vectors with a third vector is equal to the sum of the inner products of each vector with the third vector.
`InnerProductSpace.Core.norm_inner_le_norm` theorem InnerProductSpace.Core.norm_inner_le_norm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y : F), ‖⟪x, y⟫_𝕜‖ ≤ ‖x‖ * ‖y‖ This theorem states the Cauchy-Schwarz inequality in the context of an inner product space. Specifically, for any scalar field 𝕜, any type F with the structure of an additive commutative group and a 𝕜-module, and any instance of the InnerProductSpace.Core class for 𝕜 and F, the absolute value of the inner product of any two elements x and y of F (denoted by ‖⟪x, y⟫_𝕜‖) is less than or equal to the product of the norms of x and y (denoted by ‖x‖ * ‖y‖). More concisely: For any inner product space over a scalar field and two of its elements, the absolute value of their inner product is less than or equal to the product of their norms.
`Orthonormal.inner_right_finsupp` theorem Orthonormal.inner_right_finsupp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (l : ι →₀ 𝕜) (i : ι), ⟪v i, (Finsupp.total ι E 𝕜 v) l⟫_𝕜 = l i The theorem `Orthonormal.inner_right_finsupp` states that for a given set of orthonormal vectors `v : ι → E` in an inner product space `E` over a field `𝕜`, and for any linear combination `l : ι →₀ 𝕜` of these vectors, the inner product of the vector `v i` (for any `i`) with the evaluated linear combination `(Finsupp.total ι E 𝕜 v) l` equals the coefficient `l i` of `v i` in the linear combination. Essentially, this theorem claims that taking the inner product with an orthonormal vector picks out the corresponding coefficient in the linear combination. More concisely: For any orthonormal sequence `v : ι → E` in an inner product space `E` over a field `𝕜` and any linear combination `l : ι →₀ 𝕜` of these vectors, the inner product `〈v i, (Finsupp.total ι E 𝕜 v) l〉 = l i` for all `i`.
`norm_sub_mul_self` theorem norm_sub_mul_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖ This theorem is about expanding the square of the norm of the difference between two vectors in an inner product space. Specifically, for any type `𝕜` that satisfies the RCLike structure, and any type `E` that is a normed additive commutative group and an inner product space over `𝕜`, the square of the norm of the difference between two vectors `x` and `y` in `E` is equal to the square of the norm of `x` minus twice the real part of the inner product of `x` and `y` plus the square of the norm of `y`. In other words, it asserts that ‖x - y‖² = ‖x‖² - 2 Re⟨x, y⟩ + ‖y‖². More concisely: In an inner product space over a RCLike field, the square of the norm of the difference between two vectors is equal to the sum of the squares of their norms minus twice the real part of their inner product.
`InnerProductSpace.Core.nonneg_re` theorem InnerProductSpace.Core.nonneg_re : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x : F), 0 ≤ RCLike.re ⟪x, x⟫_𝕜 This is a theorem stating that the inner product is positive semidefinite. In more detail, for any type `𝕜` that has a structure of `RCLike`, any type `F` that has structures of an additive commutative group and a module over `𝕜`, any inner product space core structure on `𝕜` and `F`, and any element `x` of `F`, the real part of the inner product of `x` with itself in the structure `𝕜`, denoted as `⟪x, x⟫_𝕜`, is always nonnegative. This theorem is a fundamental property of inner product spaces in linear algebra. More concisely: For any inner product space over a RCLike type, the real part of the inner product of any vector with itself is nonnegative.
`norm_add_pow_two_real` theorem norm_add_pow_two_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2 The theorem `norm_add_pow_two_real` states that for any normed additive commutative group `F` that also forms an inner product space over the real numbers, the square of the norm of the sum of any two elements `x` and `y` in `F` equals the sum of the square of the norm of `x`, twice the inner product of `x` and `y` in the real number domain, and the square of the norm of `y`. This is an expansion of the square of the norm of the sum of two vectors, similar to the expansion of a binomial squared in algebra. More concisely: For any element `x` and `y` in a real inner product space `F` as a normed additive commutative group, the square of their norm is equal to the sum of the square of the norm of `x`, twice the inner product of `x` and `y`, and the square of the norm of `y`.
`inner_self_ofReal_re` theorem inner_self_ofReal_re : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x : E), ↑(RCLike.re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜 This theorem states that for any type `𝕜` that behaves like a real closed field, and any normed add commutative group `E` that also has an inner product space structure over `𝕜`, the real part of the inner product of any element `x` from `E` with itself is equal to the inner product of `x` with itself. In other words, for any `x` in `E`, the real part of its self-inner product is itself. The real part is obtained using the `RCLike.re` function, and the inner product is denoted by `⟪x, x⟫_𝕜`. More concisely: For any real closed field `𝕜` and normed add commutative group `E` with an inner product space structure over `𝕜`, the real part of the inner product of any `x` in `E` with itself equals the inner product of `x` with `x`. That is, `RCLike.re (⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜`.
`InnerProductSpace.Core.inner_self_nonneg` theorem InnerProductSpace.Core.inner_self_nonneg : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] {x : F}, 0 ≤ RCLike.re ⟪x, x⟫_𝕜 This theorem states that for any type 𝕜 with a RCLike (Real or Complex-like) structure, and any type F which forms an additive commutative group and is also a module over 𝕜, along with an InnerProductSpace.Core structure on 𝕜 and F, the inner product of any vector 'x' with itself (⟪x, x⟫_𝕜) is nonnegative, as returned by the 're' function of the RCLike structure of 𝕜. This captures the common intuition in geometry that the "length" of a vector, represented by taking its inner product with itself, should always be nonnegative. More concisely: For any RCLike structure 𝕜 on a type, and any additive commutative group F with a module structure over 𝕜 and an InnerProductSpace.Core structure, the inner product of any vector 'x' in F with itself is nonnegative (⟪x, x⟫_𝕜 ≥ 0).
`Orthonormal.comp_linearIsometry` theorem Orthonormal.comp_linearIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [inst_3 : NormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] {v : ι → E}, Orthonormal 𝕜 v → ∀ (f : E →ₗᵢ[𝕜] E'), Orthonormal 𝕜 (⇑f ∘ v) The theorem states that a linear isometry preserves the property of being orthonormal. Given a type 𝕜 with an inner product space structure and normed additive commutative group structures on types E and E', if we have a set of vectors v indexed by ι in E that is orthonormal in the 𝕜 sense, any linear isometry from E to E' will map this set to another set of vectors in E' that is also orthonormal in the 𝕜 sense. In other words, if we apply a linear isometry to each vector in an orthonormal set, the resulting set will also be orthonormal. More concisely: A linear isometry preserves the orthonormality of vectors between two inner product spaces.
`real_inner_div_norm_mul_norm_eq_neg_one_iff` theorem real_inner_div_norm_mul_norm_eq_neg_one_iff : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x The theorem states that for any two vectors in a real inner product space, the value of their inner product divided by the product of their norms equals -1 if and only if both vectors are nonzero and one vector is a negative multiple of the other. The "multiple" here is represented by a real number r that is less than 0. This implies that the vectors are in the same line but in opposite directions, as the inner product divided by the product of their norms measures the cosine of the angle between them, and a cosine of -1 indicates that the vectors are aligned but pointing in opposite directions. More concisely: Given any two non-zero vectors in a real inner product space, their inner product equals the negative product of their norms if and only if they are negatives of each other.
`inner_map_complex` theorem inner_map_complex : ∀ {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : InnerProductSpace ℝ G] (f : G ≃ₗᵢ[ℝ] ℂ) (x y : G), ⟪x, y⟫_ℝ = ((starRingEnd ℂ) (f x) * f y).re This theorem states that for any inner product space of dimension 2 over the real numbers `ℝ` and any isometric linear map `f` from this space to the complex numbers `ℂ`, the inner product of any two vectors `x` and `y` in this space can be calculated as the real part of the complex conjugate of `f(x)` multiplied by `f(y)`. Here, `starRingEnd ℂ` denotes the complex conjugate operation and `.re` denotes the real part of a complex number. More concisely: For any 2-dimensional real inner product space and isometric linear map to complex numbers, the inner product of two vectors x and y is equal to the real part of the complex conjugate of f(x) times f(y).
`real_inner_comm` theorem real_inner_comm : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by sorry This theorem, `real_inner_comm`, states that for any type `F` which is a normed-additive-commutative-group and also an inner product space over the real numbers, the inner product of any two elements `x` and `y` of this type, denoted as `⟪y, x⟫_ℝ`, is equal to the inner product `⟪x, y⟫_ℝ`. In other words, this theorem demonstrates that the operation of inner product in this context is commutative. More concisely: For any normed-additive-commutative group and inner product space `F` over the real numbers, the inner product is commutative: `⟪x, y⟫_ℝ = ⟪y, x⟫_ℝ` for all `x, y ∈ F`.
`real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two` theorem real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x, y⟫_ℝ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2 This theorem is called the polarization identity and it relates the real inner product of two vectors to their norms. Specifically, for any normed additive commutative group `F` that also has an inner product space over the real numbers, the real inner product of any two elements `x` and `y` of `F` is equal to half of the difference between the sum of the squares of their norms and the square of the norm of their difference. In mathematical notation, we have `⟪x, y⟫_ℝ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2` for all `x` and `y` in `F`. More concisely: The real inner product of two vectors in a normed additive commutative group with an inner product space over the real numbers is equal to half the sum of the squares of their norms minus the square of the norm of their difference.
`dist_div_norm_sq_smul` theorem dist_div_norm_sq_smul : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F}, x ≠ 0 → y ≠ 0 → ∀ (R : ℝ), dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y This theorem establishes the formula for calculating the Euclidean distance between the images of two nonzero points, `x` and `y`, under an inversion with the center at zero. Specifically, each point is scaled by the square of the ratio of a real number `R` to its norm, and the distance between these transformed points is equal to `(R^2 / (norm of x * norm of y)) * (distance between x and y)`. This is a concept from Euclidean Geometry often related to inversions or transformations around a general point. More concisely: The Euclidean distance between the inverted points `x` and `y` with center at zero is `(R^2 / (\|\|x\|\| \|\|y\|\|)) * \|\|x - y\|\|`, where `R` is a real number and `\|\|.\|\|` denotes the Euclidean norm.*
`innerSL_apply_norm` theorem innerSL_apply_norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x : E), ‖(innerSL 𝕜) x‖ = ‖x‖ The theorem `innerSL_apply_norm` states that for any type `𝕜` that behaves like a real or complex number (satisfies `RCLike 𝕜`), and any type `E` that is a normed additive commutative group and an inner product space over `𝕜`, the function `innerSL` (which gives the continuous sesquilinear form associated to the inner product) is an isometry. This is expressed precisely by the equation `‖(innerSL 𝕜) x‖ = ‖x‖` for any `x` in `E`, meaning the norm of the image of `x` under `innerSL` is the same as the norm of `x` itself. Note that a related `LinearIsometry`, which is a type of function preserving the inner product structure, is defined as `toDualMap` in `InnerProductSpace.Dual`. More concisely: For any type `𝕜` acting like a real or complex number and any normed additive commutative group and inner product space `E` over `𝕜`, the continuous sesquilinear form `innerSL` associated to the inner product is an isometry. Equivalently, the norm of `innerSL` applied to any element `x` in `E` equals the norm of `x`.
`InnerProductSpace.Core.inner_neg_left` theorem InnerProductSpace.Core.inner_neg_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y : F), ⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜 This Lean theorem, `InnerProductSpace.Core.inner_neg_left`, states that for any type `𝕜` that resembles a ring, and any additive commutative group `F` that is also a `𝕜`-module, as well as any two elements `x` and `y` of `F`, the inner product of `-x` and `y` is equal to the negation of the inner product of `x` and `y`. In other words, the inner product operation in this context respects the distributivity of scalar multiplication over vector addition. More concisely: For any additive commutative group `F` that is a `𝕜`-module over a ring `𝕜`, the inner product of `-x` and `y` equals the negation of the inner product of `x` and `y`, for all `x, y ∈ F`.
`eq_of_norm_le_re_inner_eq_norm_sq` theorem eq_of_norm_le_re_inner_eq_norm_sq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x y : E}, ‖x‖ ≤ ‖y‖ → RCLike.re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2 → x = y This theorem states that for any types `𝕜` and `E` such that `𝕜` is an instance of `RCLike` and `E` is both a normed additive commutative group and an inner product space over `𝕜`, for any elements `x` and `y` of `E`, if the norm of `x` is less than or equal to the norm of `y` and the real component of the inner product of `x` and `y` equals the square of the norm of `y`, then `x` is equal to `y`. This theorem can be understood geometrically as stating that a sphere of radius equal to the norm of `y` is tangent to a plane described by the equation 'inner product of `x` and `y` equals the square of `y`'s norm' at the point `x = y`. More concisely: Given a normed additive commutative group `E` over a RCLike ring `𝕜` and an inner product space `E`, if `x, y ∈ E` satisfy `\|\|x\|\| ≤ \|\|y\|\|` and `∝(x, y) = \|\|y\|\|²`, then `x = y`.
`norm_add_pow_two` theorem norm_add_pow_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2 The theorem `norm_add_pow_two` states that for any type `𝕜` which behaves like a ring of scalars (as denoted by `RCLike 𝕜`), any `E` which is a normed add commutative group, and any `E` which is an inner product space over `𝕜`, the square of the norm of the sum of two vectors `x` and `y` in `E` is equal to the sum of the square of the norm of `x`, twice the real part of the inner product of `x` and `y`, and the square of the norm of `y`. This essentially provides a way to expand the square of the norm of a sum of two vectors in an inner product space. More concisely: For any normed add commutative group `E` over a ring of scalars `𝕜`, being an inner product space, the square of the norm of `x + y` equals the sum of the square of the norm of `x`, twice the dot product of `x` and `y`, and the square of the norm of `y`.
`Orthonormal.inner_sum` theorem Orthonormal.inner_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (l₁ l₂ : ι → 𝕜) (s : Finset ι), ⟪s.sum fun i => l₁ i • v i, s.sum fun i => l₂ i • v i⟫_𝕜 = s.sum fun i => (starRingEnd 𝕜) (l₁ i) * l₂ i This theorem states that for any field `𝕜`, if `v` is an orthonormal set of vectors in an inner product space over this field, then the inner product of two linear combinations (expressed as sums) of these vectors, with coefficients given by two functions `l₁` and `l₂` from `ι` to `𝕜`, is equal to the sum of the products of the corresponding coefficients, with the first one being conjugated. The sum is taken over a finite subset `s` of `ι`. In essence, it provides a convenient form to compute the inner product in such cases. The starRingEnd operation denotes complex conjugation for complex fields, and leaves real coefficients unchanged. More concisely: For any inner product space over a field and orthonormal set of vectors, the inner product of two linear combinations of these vectors is equal to the sum of the products of the corresponding coefficients, with the first coefficient conjugated.
`norm_sub_eq_sqrt_iff_real_inner_eq_zero` theorem norm_sub_eq_sqrt_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F}, ‖x - y‖ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖).sqrt ↔ ⟪x, y⟫_ℝ = 0 This theorem, named `norm_sub_eq_sqrt_iff_real_inner_eq_zero`, establishes a relationship between the norms and the inner product of two vectors in a Real number inner product space. Specifically, it asserts that for any two vectors `x` and `y` in a normed additively commutative group with an inner product (a type of metric space), the norm of the difference between `x` and `y` being equal to the square root of the sum of the squares of their norms (a form of Pythagorean theorem) holds if and only if the real inner product of `x` and `y` is zero. More concisely: In a Real number inner product space, the norm of the difference between two vectors is equal to the square root of the sum of the squares of their norms if and only if their inner product is zero.
`im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four` theorem im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), RCLike.im ⟪x, y⟫_𝕜 = (‖x - RCLike.I • y‖ * ‖x - RCLike.I • y‖ - ‖x + RCLike.I • y‖ * ‖x + RCLike.I • y‖) / 4 This theorem, referred to as the Polarization Identity, states that for any field that behaves like the complex numbers or the real numbers (denoted by 𝕜), and for any normed additive commutative group with an inner product space (denoted by E), the imaginary part of the inner product of any two elements in E, can be calculated as a function of the norm of the two elements. Specifically, it is the difference of the squared norm of the element obtained by subtracting from the first element the imaginary unit times the second element and the squared norm of the element obtained by adding to the first element the imaginary unit times the second element, all divided by 4. More concisely: For any normed additive commutative group with an inner product space over a field behaving like the complex numbers, the imaginary part of their inner product equals one-quarter the difference between the squared norms of the sum and difference of the elements, with one multiplied by the imaginary unit.
`inner_neg_left` theorem inner_neg_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜 This theorem states that for any inner product space `E` over a scalar field `𝕜` with a commutative group structure and a norm, if we have two elements `x` and `y` in `E`, then the inner product of `-x` and `y` is equal to the negation of the inner product of `x` and `y`. In mathematical notation, this would be expressed as `⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜`. This property is one of the basic properties of inner product spaces. More concisely: The inner product of the negation of an element with another element in an inner product space is equal to the negation of their inner product. In other words, `⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜`.
`norm_eq_sqrt_real_inner` theorem norm_eq_sqrt_real_inner : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F), ‖x‖ = (⟪x, x⟫_ℝ).sqrt := by sorry This theorem states that for any type `F` that is a normed add commutative group and has a real inner product space structure, the norm of an element `x` of type `F` is equal to the square root of the real inner product of `x` with itself. In mathematical notation, this is saying that for any vector `x` in such a space `F`, the equation `‖x‖ = sqrt()` holds. More concisely: For any normed add commutative group `F` with a real inner product space structure, the norm of an element `x` equals the square root of the inner product of `x` with itself: `‖x‖ = sqrt()`.
`real_inner_mul_inner_self_le` theorem real_inner_mul_inner_self_le : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ This theorem represents the Cauchy-Schwarz inequality for real inner products. It states that for any type `F` which is a normed add comm group and an inner product space over the real numbers, and for any two elements `x` and `y` of this type, the square of the inner product of `x` and `y` is less than or equal to the product of the inner product of `x` with itself and `y` with itself. In mathematical notation, this can be written as: $(x \cdot y)^2 \leq (x \cdot x) \cdot (y \cdot y)$, where `$\cdot$` denotes the inner product. More concisely: For any real inner product space `F` and elements `x, y` in `F`, the inner product `(x · y)²` is less than or equal to the product of the norms `‖x‖²` and `‖y‖²`.
`re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two` theorem re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), RCLike.re ⟪x, y⟫_𝕜 = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2 The theorem `re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two` states that for any type `𝕜` that is a ring with a conjugation operation, and any type `E` that forms a normed additive commutative group and an inner product space over `𝕜`, the real part of the inner product of two elements `x` and `y` of `E` is equal to one-half of the difference between the square of the norm of the sum of `x` and `y`, and the sums of the squares of the norms of `x` and `y`. This is known as the polarization identity. More concisely: The real part of the inner product of two elements in a normed additive commutative group and an inner product space over a ring with a conjugation operation equals half the difference between the sum of their squared norms and the square of their norm-sum. (Polarization identity)
`norm_add_mul_self_real` theorem norm_add_mul_self_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖ This theorem states that in a normed add commutative group `F` over the real numbers endowed with an inner product, for any two elements `x` and `y` of `F`, the square of the norm of the sum of `x` and `y` is equal to the sum of the square of the norm of `x`, twice the inner product of `x` and `y`, and the square of the norm of `y`. In simple terms, it's an expression of the identity (x+y)^2 = x^2 + 2xy + y^2 in the context of inner product spaces. More concisely: In a normed additive commutative group endowed with an inner product, the norm of the sum of two elements is equal to the sum of their norms and twice their inner product.
`real_inner_smul_self_left` theorem real_inner_smul_self_left : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F) (r : ℝ), ⟪r • x, x⟫_ℝ = r * (‖x‖ * ‖x‖) This theorem states that for any real number `r` and any vector `x` from an inner product space over the real numbers, the inner product of `x` with `r` times itself is equal to `r` times the square of the norm of `x`. In other words, it is defining a property of the inner product in terms of scalar multiplication and vector norms in a real inner product space. More concisely: For any real inner product space and any of its elements `x` and scalar `r`, the inner product of `x` with `r` times `x` equals `r` times the square of the norm of `x`. In symbols: `∥x∥² = * r²` or ` = r * ∥x∥²`.
`sum_inner` theorem sum_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} (s : Finset ι) (f : ι → E) (x : E), ⟪s.sum fun i => f i, x⟫_𝕜 = s.sum fun i => ⟪f i, x⟫_𝕜 The theorem `sum_inner` states that for any field `𝕜`, any normed add commutative group `E`, and any inner product space `𝕜 E`, given a finite set `s` of type `ι`, a function `f` mapping from `ι` to `E`, and an element `x` of `E`, the inner product of the sum of the set `s` under function `f` and `x` is equal to the sum of the inner products of each element in the set `s` (when transformed by function `f`) and `x`. In mathematical terms, it's stating that the inner product operation preserves the additivity when the sum operation is applied to the first component of the inner product. More concisely: For any inner product space over a field and a finite set with a function to the space, the inner product of the sum of the set under the function and an element is equal to the sum of the inner products of each set element and the element under the function.
`inner_eq_norm_mul_iff` theorem inner_eq_norm_mul_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x y : E}, ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y This theorem states that given any two vectors `x` and `y` in an inner product space over a field that resembles the complex numbers, if the inner product of `x` and `y` is equal to the product of their norms, then the vectors are nonnegative real multiples of each other. This is one form of the equality case for the Cauchy-Schwarz inequality. Note that there is a related theorem `norm_inner_eq_norm_iff`, which has a similar conclusion but only requires the absolute value of the inner product to equal the product of the norms. More concisely: If two vectors in an inner product space over a field with complex-like scalars have equal inner product equal to the product of their norms, then they are nonnegative real multiples of each other. (Cauchy-Schwarz equality)
`Orthonormal.tsum_inner_products_le` theorem Orthonormal.tsum_inner_products_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} (x : E) {v : ι → E}, Orthonormal 𝕜 v → ∑' (i : ι), ‖⟪v i, x⟫_𝕜‖ ^ 2 ≤ ‖x‖ ^ 2 "Bessel's Inequality" ensures that for any type 𝕜, where 𝕜 is a real or complex-like field, and type E, which is a NormedAddCommGroup and an InnerProductSpace over 𝕜, for any type ι, any element "x" of E, and any function "v" from ι to E, if "v" is an orthonormal set of vectors in this inner product space (meaning that each vector has norm 1 and any pair of different vectors are orthogonal), then the sum of the squares of the norms of the inner products of "v i" and "x" (for each "i" in ι) is at most the square of the norm of "x". This theorem is one of the fundamental results in linear algebra regarding inner product spaces. More concisely: For any orthonormal set of vectors in a real or complex inner product space, the sum of the squares of the inner products of each vector with an arbitrary element and the vector itself is less than or equal to the square of the norm of the element.
`InnerProductSpace.Core.add_left` theorem InnerProductSpace.Core.add_left : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x y z : F), ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜 This theorem states that the inner product operation in an inner product space is additive in the first coordinate. Specifically, given any inner product space with a field `𝕜` and a module `F`, for any three elements `x`, `y`, and `z` in `F`, the inner product of the sum of `x` and `y` with `z` (`⟪x + y, z⟫_𝕜`) is equal to the sum of the inner product of `x` with `z` and the inner product of `y` with `z` (`⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜`). This property is one of the key characteristics of the inner product operation. More concisely: The inner product of the sum of two vectors in an inner product space is equal to the sum of their inner products with a third vector.
`InnerProductSpace.Core.inner_self_im` theorem InnerProductSpace.Core.inner_self_im : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F), RCLike.im ⟪x, x⟫_𝕜 = 0 The theorem `InnerProductSpace.Core.inner_self_im` states that for any ring 𝕜 that is a "Real/C-complex-like" structure (RCLike), and for any additive commutative group F that is a module over 𝕜, if 𝕜 and F together form an inner product space (denoted by `InnerProductSpace.Core 𝕜 F`), then the imaginary part of the inner product of any element `x` of `F` with itself is zero. In other words, the inner product of an element with itself in this context is always a real number. More concisely: For any RCLike ring 𝕜 and its module F forming an inner product space, the self-inner product of any element in F is real.
`norm_add_eq_sqrt_iff_real_inner_eq_zero` theorem norm_add_eq_sqrt_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F}, ‖x + y‖ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖).sqrt ↔ ⟪x, y⟫_ℝ = 0 This theorem, which is a form of the Pythagorean theorem, states that for any type `F` which is a normed additive commutative group and has an inner product space over the real numbers, given any two elements `x` and `y` of `F`, the norm of the sum of `x` and `y` is equal to the square root of the sum of the squares of the norms of `x` and `y` if and only if the real inner product of `x` and `y` is zero. In mathematical notation, this is saying that ‖x + y‖ equals the square root of (‖x‖^2 + ‖y‖^2) if and only if the inner product of x and y over the real numbers is zero. More concisely: For any normed additive commutative group `F` with an inner product over the real numbers, the norm of their sum is equal to the square root of the sum of the squares of their norms if and only if they are orthogonal (have zero inner product).
`real_inner_self_eq_norm_mul_norm` theorem real_inner_self_eq_norm_mul_norm : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F), ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖ := by sorry This theorem states that for any real inner product space 'F', the real inner product of any element 'x' with itself is equal to the square of the norm of 'x'. Here, a real inner product space is a normed add comm group with an inner product operation that takes two elements of the group and produces a real number. The norm of an element is a measure of its "length" or "magnitude". More concisely: In a real inner product space, the inner product of an element with itself equals the square of its norm.
`InnerProductSpace.Core.inner_smul_left` theorem InnerProductSpace.Core.inner_smul_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y : F) {r : 𝕜}, ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜 This theorem states that for any scalar `r` and any two vectors `x` and `y` in an inner product space (over a field `𝕜` with a star-ring-end operation) with scalar multiplication, the inner product of the multiplication of `r` and `x`, with `y`, is equal to the multiplication of the star of `r` and the inner product of `x` and `y`. In mathematical terms, it represents the property: `⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜`. This theorem demonstrates one of the essential properties of inner product spaces, namely the distributive property of scalar multiplication with respect to the inner product operation. More concisely: For any scalar `r` and vectors `x` and `y` in an inner product space, the scalar multiplication of `r` with vector `x`, and the inner product of `x` with `y`, is equal to the inner product of `x` with the star-operation of `r` times `y`. In symbolic form: `⟪r • x, y⟫_𝕜 = ⟪x, (starRingEnd 𝕜) r * y⟫_𝕜`.
`re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four` theorem re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), RCLike.re ⟪x, y⟫_𝕜 = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4 This theorem states the polarization identity in the context of an inner product space. Given a type `𝕜` which is an instance of `RCLike` and a type `E` which is an instance of `NormedAddCommGroup` and `InnerProductSpace 𝕜 E`, for any two elements `x` and `y` of `E`, the real part of their inner product equals the difference of the square of the norm of their sum and the square of the norm of their difference, divided by four. The formula is: \[ \text{Re}⟪x, y⟫_𝕜 = \frac{‖x + y‖^2 - ‖x - y‖^2}{4} \] This identity provides an important relationship between the inner product and the norm in an inner product space. More concisely: The real part of the inner product of two elements in a normed inner product space equals one-fourth the difference between the square of their norms.
`LinearIsometry.orthonormal_comp_iff` theorem LinearIsometry.orthonormal_comp_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [inst_3 : NormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] {v : ι → E} (f : E →ₗᵢ[𝕜] E'), Orthonormal 𝕜 (⇑f ∘ v) ↔ Orthonormal 𝕜 v The theorem `LinearIsometry.orthonormal_comp_iff` states that for any set of vectors `v` in an inner product space `E`, and for any linear isometry `f` mapping `E` to another inner product space `E'`, `v` being an orthonormal set is equivalent to the set of vectors obtained by applying `f` to `v` (written as `⇑f ∘ v` in Lean 4) being orthonormal. This means a linear isometry preserves the property of being orthonormal. In terms of mathematical symbols, if `v` is an orthonormal set in `E`, and `f` is a linear isometry from `E` to `E'`, then `f(v)` is orthonormal in `E'`, and vice versa. More concisely: For any orthonormal set `v` in an inner product space `E` and any linear isometry `f` from `E` to an inner product space `E'`, `f(v)` is orthonormal in `E'` if and only if `v` is orthonormal in `E`.
`continuous_inner` theorem continuous_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E], Continuous fun p => ⟪p.1, p.2⟫_𝕜 This theorem states that for any type `𝕜` and `E`, where `𝕜` is a ring-completeness-like structure, `E` is a normed commutative additive group, and `E` is an inner product space over `𝕜`, the inner product of any pair of elements in `E` is a continuous function. In mathematical terms, it means the inner product operation is continuous in this inner product space. More concisely: Given a ring-completeness-like structure `𝕜`, a normed commutative additive group `E` over `𝕜`, and an inner product space `E` over `𝕜`, the inner product is a continuous function on `E × E`.
`Orthonormal.inner_left_sum` theorem Orthonormal.inner_left_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (l : ι → 𝕜) {s : Finset ι} {i : ι}, i ∈ s → ⟪s.sum fun i => l i • v i, v i⟫_𝕜 = (starRingEnd 𝕜) (l i) The theorem states that for a given set of orthonormal vectors in an inner product space, the inner product of a linear combination of these vectors with one of the vectors yields the coefficient of that vector. More specifically, if `𝕜` is a unit type, `E` is a normed add commutative group, and `ι` is a type, then for a function `v` mapping `ι` to `E` that forms an orthonormal set, and for a function `l` that assigns scalars from `𝕜` to the elements of `ι`, for any finite set `s` of `ι` and any element `i` of `s`, the inner product of the sum of the scaled vectors in `s` with `v i` is equal to the conjugate of the scaling factor `l i`. This essentially means that the inner product in this context can be used to isolate individual components of the linear combination. More concisely: For an orthonormal set of vectors `v` in an inner product space, the inner product of a linear combination of these vectors with one vector `vi` is equal to the conjugate of the corresponding scaling factor `li`.
`linearIndependent_of_ne_zero_of_inner_eq_zero` theorem linearIndependent_of_ne_zero_of_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, (∀ (i : ι), v i ≠ 0) → (Pairwise fun i j => ⟪v i, v j⟫_𝕜 = 0) → LinearIndependent 𝕜 v The theorem states that a family of vectors is linearly independent if each vector in the family is nonzero and pairwise orthogonal. Here, 'pairwise orthogonal' means that the inner product of any two distinct vectors in the family equals zero. This holds for any type `𝕜` that behaves like a ring with conjugation, any normed additively commutative group `E` that forms an inner product space over `𝕜`, and a family of vectors `v` indexed by `ι`. More concisely: A family of nonzero vectors in an inner product space over a ring with conjugation is linearly independent if and only if any two distinct vectors are orthogonal.
`InnerProductSpace.conj_symm` theorem InnerProductSpace.conj_symm : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [self : InnerProductSpace 𝕜 E] (x y : E), (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜 This theorem states that the inner product operation in an inner product space is hermitian. In other words, for any two elements (x and y) of an inner product space, taking the complex conjugate (indicated by `starRingEnd` in Lean 4) of the inner product of y and x gives us the inner product of x and y. This property is often referred to as the conjugate symmetry of the inner product. More concisely: The inner product operation in an inner product space is conjugate symmetric, that is, for all x and y in the space, = .*
`real_inner_sub_sub_self` theorem real_inner_sub_sub_self : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ This theorem states that for any real inner product space, the inner product of the difference of two vectors with itself expands algebraically to the difference of the inner product of each vector with itself and twice the inner product of the two vectors. In mathematical terms, it says that for all vectors `x` and `y` in the vector space, `⟪x - y, x - y⟫_ℝ` equals `⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ`. More concisely: For any real inner product space, the inner product of the difference of two vectors with itself equals the inner product of the first vector with itself minus twice the inner product of the first and second vectors plus the inner product of the second vector with itself.
`Orthonormal.inner_right_fintype` theorem Orthonormal.inner_right_fintype : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} [inst_3 : Fintype ι] {v : ι → E}, Orthonormal 𝕜 v → ∀ (l : ι → 𝕜) (i : ι), ⟪v i, Finset.univ.sum fun i => l i • v i⟫_𝕜 = l i This theorem states that for any field `𝕜`, a normed addition commutative group `E`, and an inner product space over `𝕜` and `E`, given a set of orthonormal vectors `v` indexed by a finite type `ι`, if we take the linear combination of the set of orthonormal vectors with coefficients from a function `l : ι → 𝕜`, then the inner product of any vector `v i` from the set and the linear combination is equal to the coefficient `l i` of the vector `v i` in the combination. In other words, when a linear combination of orthonormal vectors is involved in an inner product operation with one of the orthonormal vectors, the result of the inner product operation is the coefficient of the involved vector in the linear combination. More concisely: For any inner product space over a field and a set of orthonormal vectors, the inner product of a vector from the set and the linear combination of the set with coefficients from a function is equal to the coefficient of the vector in the combination.
`InnerProductSpace.Core.inner_add_add_self` theorem InnerProductSpace.Core.inner_add_add_self : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y : F), ⟪x + y, x + y⟫_𝕜 = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜 This theorem states that in an inner product space, the inner product of a vector sum with itself (specifically, `(x + y, x + y)`) can be expanded into the sum of the inner products of the original vectors and their transpositions (i.e., `(x, x) + (x, y) + (y, x) + (y, y)`). The inner product space is defined over a field of scalars `𝕜` and a vector space `F`, where `𝕜` is a real or complex-like field, and `F` is an additive commutative group that also forms a module over `𝕜`. More concisely: In an inner product space over field `𝕜` and vector space `F`, the inner product of the sum of two vectors `x` and `y` with itself is equal to the sum of the inner products of each vector with its transposition: `(x + y, x + y) = (x, x) + (x, y) + (y, x) + (y, y)`.
`Orthonormal.mapLinearIsometryEquiv` theorem Orthonormal.mapLinearIsometryEquiv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [inst_3 : NormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] {v : Basis ι 𝕜 E}, Orthonormal 𝕜 ⇑v → ∀ (f : E ≃ₗᵢ[𝕜] E'), Orthonormal 𝕜 ⇑(v.map f.toLinearEquiv) This theorem states that the property of being an orthonormal set of vectors in an Inner Product Space is preserved under a linear isometric equivalence. More precisely, if we have an orthonormal set of vectors in an Inner Product Space, and we apply a linear isometric equivalence to these vectors (using `Basis.map`), the resulting set of vectors will also be orthonormal. In mathematical terms, for any field `𝕜`, Inner Product Spaces `E` and `E'`, a basis `v` of `E`, and a linear isometric equivalence `f` from `E` to `E'`, if `v` is an orthonormal set of vectors, then the set of vectors obtained by mapping `v` through `f` (`v.map f.toLinearEquiv`) is also an orthonormal set of vectors. More concisely: If `v` is an orthonormal set of vectors in an Inner Product Space `E`, then the set `v.map (linearIsometry f)` is an orthonormal set of vectors in the image space of a linear isometric equivalence `f` from `E` to another Inner Product Space.
`exists_maximal_orthonormal` theorem exists_maximal_orthonormal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {s : Set E}, Orthonormal 𝕜 Subtype.val → ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w The theorem `exists_maximal_orthonormal` states that for any given orthonormal set `v` of vectors in an inner product space `E` over a real or complex-like field `𝕜`, there exists a maximal orthonormal set that includes `v`. Here, a set is deemed maximal if any set `u` that includes the maximal set and is orthonormal is in fact the same set as the maximal set. In the context of the theorem, sets of vectors are represented as subtypes, which are elements of the base type `E` satisfying a certain property, and the norm of a vector and the inner product between two vectors are defined according to the `NormedAddCommGroup` and `InnerProductSpace` structures respectively. More concisely: Given any orthonormal set `v` in an inner product space `E` over a real or complex field, there exists a maximal orthonormal set containing `v` that is equal to every other orthonormal set including it.
`Submodule.coe_inner` theorem Submodule.coe_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (W : Submodule 𝕜 E) (x y : ↥W), ⟪x, y⟫_𝕜 = ⟪↑x, ↑y⟫_𝕜 This theorem states that for any subclass `𝕜` of Type `u_1` and subclass `E` of Type `u_2` under the conditions that `𝕜` is a type similar to `ℝ` (the set of real numbers), `E` is a normed additive commutative group, and `E` is an inner product space over `𝕜`, if `W` is a submodule of `𝕜` and `x` and `y` are members of `W`, then the inner product of `x` and `y` in `𝕜` is the same as the inner product of the coerced values of `x` and `y` in `𝕜`. Essentially, this means that the inner product of two elements in a submodule is the same as their inner product in the containing space. More concisely: For any submodule `W` of a type similar to `ℝ` `𝕜`, and for any `x` and `y` in `W`, the inner product of `x` and `y` in `𝕜` equals the inner product of their coerced values in `𝕜`.
`orthonormal_subtype_iff_ite` theorem orthonormal_subtype_iff_ite : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : DecidableEq E] {s : Set E}, Orthonormal 𝕜 Subtype.val ↔ ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫_𝕜 = if v = w then 1 else 0 The theorem `orthonormal_subtype_iff_ite` describes the condition for a set of vectors in an InnerProductSpace to be orthonormal. This condition is expressed as an `if...else` statement, relating to the inner product of any two vectors `v` and `w` from a given set `s`. The theorem states that for all types `𝕜` and `E`, where `𝕜` exhibits properties of a ring and `E` is a NormedAddCommGroup, and if `E` also has a DecidableEq instance, then a set `s` of elements of type `E` is orthonormal if and only if for all vectors `v` and `w` in `s`, the inner product of `v` and `w` is 1 if `v` and `w` are the same and 0 otherwise. More concisely: A set of vectors in a Normed Additive Commutative Group endowed with a Decidable Equality relation and an Inner Product over a commutative ring is orthonormal if and only if the inner product of any two distinct vectors in the set is zero, and the inner product of any vector with itself is one.
`norm_eq_sqrt_inner` theorem norm_eq_sqrt_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x : E), ‖x‖ = (RCLike.re ⟪x, x⟫_𝕜).sqrt This theorem states that for any type `𝕜` that behaves like a division ring (`RCLike 𝕜`), a normed additive commutative group `E`, and a inner product space `𝕜 E`, the norm of a vector `x` in `E` is equal to the square root of the real part of the inner product of `x` with itself. Specifically, `‖x‖ = sqrt(Re⟪x, x⟫)`, where `‖x‖` is the norm of `x`, `sqrt` is the square root function, `Re⟪x, x⟫` is the real part of the inner product of `x` with itself. This is a generalization of the Pythagorean theorem to inner product spaces. More concisely: For any normed additive commutative group `E` over a division ring `𝕜` with an inner product, the norm of a vector `x` equals the square root of the real part of its inner product with itself: `‖x‖ = sqrt(Re⟪x, x⟫)`.
`norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero` theorem norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ⟪x, y⟫_𝕜 = 0 → ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ The theorem `norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero` is a generalization of the Pythagorean theorem in the context of an inner product space. In more detail, it states that for any two vectors `x` and `y` in an inner product space over a field `𝕜`, if the inner product of the two vectors is zero, then the square of the norm of the sum of the vectors is equal to the sum of the squares of the norms of the individual vectors. This is analogous to the Pythagorean theorem which states that in a right-angled triangle, the square of the length of the hypotenuse (the side opposite the right angle) is equal to the sum of the squares of the lengths of the other two sides. More concisely: In an inner product space, the square of the norm of the sum of two vectors is equal to the sum of the squares of their norms if and only if their inner product is zero.
`real_inner_add_add_self` theorem real_inner_add_add_self : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ This theorem states that for any real inner product space (a vector space with inner product over the real numbers ℝ) and any two vectors x and y in that space, the inner product of the sum of x and y with itself can be expanded to the sum of the inner product of x with itself, twice the inner product of x and y, and the inner product of y with itself. In mathematical notation, this theorem is written as: ⟨x + y, x + y⟩_ℝ = ⟨x, x⟩_ℝ + 2 * ⟨x, y⟩_ℝ + ⟨y, y⟩_ℝ. More concisely: The inner product of the sum of two vectors in a real inner product space with each other is equal to the sum of their self-inner products and twice their inner product with each other.
`Orthonormal.orthonormal_of_forall_eq_or_eq_neg` theorem Orthonormal.orthonormal_of_forall_eq_or_eq_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v w : ι → E}, Orthonormal 𝕜 v → (∀ (i : ι), w i = v i ∨ w i = -v i) → Orthonormal 𝕜 w The theorem `Orthonormal.orthonormal_of_forall_eq_or_eq_neg` states that given an orthonormal family of vectors `v` in an inner product space `E` over a field `𝕜`, another family of vectors `w` is also orthonormal if every vector in `w` equals the corresponding vector in `v` or its negation. In other words, if we have a set of vectors that is orthonormal, and a second set where each vector is either the positive or negative of the corresponding vector in the first set, then the second set is also orthonormal. More concisely: If `{v_i}` is an orthonormal family in an inner product space `E` over a field `𝕜`, and for all `i`, `w_i` is either `v_i` or its negation, then `{w_i}` is also an orthonormal family in `E`.
`inner_zero_right` theorem inner_zero_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x : E), ⟪x, 0⟫_𝕜 = 0 This theorem, `inner_zero_right`, states that for any type `𝕜` behaving like a ring (indicated by `RCLike 𝕜`) and any normed additive commutative group `E` which also constitutes an inner product space over `𝕜` (denoted as `InnerProductSpace 𝕜 E`), the inner product of any element `x` of `E` with the zero element is always zero. This is a fundamental property that holds in any inner product space. More concisely: For any ring-like type `𝕜` and inner product space `E` over `𝕜`, the inner product of any element in `E` with the zero element is zero.
`inner_eq_norm_mul_iff_real` theorem inner_eq_norm_mul_iff_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F}, ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y This theorem states that for any two vectors `x` and `y` in a real inner product space, if the inner product of `x` and `y` equals the product of their norms (i.e., `⟪x, y⟫ = ‖x‖ * ‖y‖`), then the vectors are nonnegative real multiples of each other. This is one form of the equality case for the Cauchy-Schwarz inequality. Note, this is stronger than the related result where the absolute value of the inner product equals the product of the norms. More concisely: If two vectors in a real inner product space have the same inner product as the product of their norms, then they are nonnegative real multiples.
`Orthonormal.linearIndependent` theorem Orthonormal.linearIndependent : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → LinearIndependent 𝕜 v This theorem states that for any orthonormal set of vectors in an inner product space, the set is also linearly independent. More specifically, given a field `𝕜` and a normed additive commutative group `E` that forms an inner product space, any function `v` from an index set `ι` to `E` which forms an orthonormal set is also linearly independent over the field `𝕜`. In other words, no vector in the orthonormal set can be expressed as a linear combination of the others. More concisely: In an inner product space, every orthonormal set of vectors is linearly independent.
`InnerProductSpace.Core.smul_left` theorem InnerProductSpace.Core.smul_left : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x y : F) (r : 𝕜), ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜 This theorem states that for any type 𝕜 that behaves like a ring of complex numbers, and any type F that is a module over 𝕜, the inner product operation is conjugate linear in the first coordinate. This means that for any elements `x` and `y` of `F`, and any scalar `r` of 𝕜, the inner product of `r` scaled by `x` and `y` is equal to the complex conjugate of `r` multiplied by the inner product of `x` and `y`. More concisely: For any complex-like ring 𝕜 and its module F, the inner product is conjugate linear in the first coordinate: $(r\cdot x)\cdot y^* = r^\cdot (x\cdot y)$, where $r\cdot x$ is the scalar multiplication, $y^$ is the complex conjugate of $y$, and $r^*$ is the complex conjugate of $r$.
`InnerProductSpace.Core.inner_conj_symm` theorem InnerProductSpace.Core.inner_conj_symm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y : F), (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜 This theorem, `InnerProductSpace.Core.inner_conj_symm`, states that for any type `𝕜` that behaves like a ring with conjugation, and for any type `F` that behaves like an additive commutative group and is a `𝕜`-module, the inner product of `x` and `y` in an inner product space is equal to the complex conjugate of the inner product of `y` and `x`. Here, `starRingEnd 𝕜` denotes the complex conjugate in the ring `𝕜`. This is a property of inner product spaces in general over the complex numbers. More concisely: For any complex ring `𝕜` with conjugation and additive commutative `𝕜`-module `F`, the inner product of `x` and `y` in an inner product space equals the complex conjugate of the inner product of `y` and `x`.
`real_inner_le_norm` theorem real_inner_le_norm : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x, y⟫_ℝ ≤ ‖x‖ * ‖y‖ This theorem states the Cauchy-Schwarz inequality in the context of an inner product space over the real numbers. For any two elements `x` and `y` in a given normed additive commutative group `F` that is also an inner product space over the real numbers, the absolute value of the inner product of `x` and `y` does not exceed the product of the norms of `x` and `y`. More concisely: For any two vectors x and y in a real inner product space, the inner product of x and y is less than or equal to the product of their magnitudes.
`norm_add_sq` theorem norm_add_sq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2 The theorem `norm_add_sq` states that for any two vectors `x` and `y` in an inner product space over a field `𝕜` (which is also a normed commutative additive group and satisfies the ring-complex-like property), the square of the norm of the sum of the vectors equals the sum of the square of the norm of `x`, twice the real part of the inner product of `x` and `y`, and the square of the norm of `y`. This is essentially the Pythagorean theorem generalized to inner product spaces. More concisely: In an inner product space over a field, the norm of the sum of two vectors equals the sum of their norms squared, plus twice the real part of their inner product.
`LinearIsometry.inner_map_map` theorem LinearIsometry.inner_map_map : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {E' : Type u_7} [inst_3 : NormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜 This theorem states that a linear isometry preserves the inner product. More specifically, for any scalar field `𝕜` and two inner product spaces `E` and `E'` over `𝕜`, if `f` is a linear isometry mapping from `E` to `E'`, then the inner product of `f(x)` and `f(y)` in `E'` is equal to the inner product of `x` and `y` in `E`, where `x` and `y` are any elements of `E`. This theorem is fundamental in the field of linear algebra and is critical to understanding the properties of linear transformations in inner product spaces. More concisely: Given any linear isometry `f` between inner product spaces `E` and `E'` over scalar field `𝕜`, the inner product `⟨f(x), f(y)⟩′` in `E'` equals `⟨x, y⟩` in `E` for any `x, y` in `E`.
`real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul` theorem real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F} {r : ℝ}, x ≠ 0 → r < 0 → ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = -1 This theorem states that in a real inner product space, if you take a nonzero vector and multiply it by a negative scalar to yield a new vector, the inner product of the original vector and the new vector, divided by the product of their norms (or lengths), is always -1. Important conditions here are that the original vector must not be the zero vector, and the scalar used for multiplication must be less than zero. More concisely: In a real inner product space, the dot product of a non-zero vector and its negative scalar multiple, normalized by the product of their norms, equals -1.
`Orthonormal.inner_finsupp_eq_sum_left` theorem Orthonormal.inner_finsupp_eq_sum_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (l₁ l₂ : ι →₀ 𝕜), ⟪(Finsupp.total ι E 𝕜 v) l₁, (Finsupp.total ι E 𝕜 v) l₂⟫_𝕜 = l₁.sum fun i y => (starRingEnd 𝕜) y * l₂ i This theorem states that if we have a set of orthonormal vectors, `v`, in an inner product space over a ring `𝕜`, then the inner product of two linear combinations of these vectors, `l₁` and `l₂`, is equal to the sum of the product of the conjugate of the coefficient of `l₁` and the coefficient of `l₂` over each element `i` in the support of `l₁`. The linear combinations are expressed using the `Finsupp.total` function, which interprets a function `l : α →₀ R` as a linear combination of a family of elements `(v : α → M)`. More concisely: Given an inner product space over a ring, if `v` is a set of orthonormal vectors and `l₁` and `l₂` are linear combinations of these vectors using `Finsupp.total`, then the inner product of `l₁` and `l₂` equals the sum of the products of the conjugates of their respective coefficients over the support of `l₁`.
`Orthonormal.inner_left_finsupp` theorem Orthonormal.inner_left_finsupp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (l : ι →₀ 𝕜) (i : ι), ⟪(Finsupp.total ι E 𝕜 v) l, v i⟫_𝕜 = (starRingEnd 𝕜) (l i) The theorem `Orthonormal.inner_left_finsupp` states that for any type `𝕜` with real-like structure and any normed additive commutative group `E` equipped with an inner product space over `𝕜`, given a set of orthonormal vectors `v` indexed by type `ι`, for any function `l` from `ι` to `𝕜` and any index `i` of type `ι`, the inner product of the total linear combination of the vectors `v` with respect to the function `l` and the vector at index `i` is equal to the complex conjugate of the value of `l` at index `i`. In other words, the inner product of a linear combination of a set of orthonormal vectors with one of those vectors isolates the coefficient of that vector. More concisely: For any orthonormal set of vectors in a real inner product space and any function mapping indices to scalars, the inner product of the linear combination of the vectors with the corresponding function value and any vector from the set equals the complex conjugate of that function value.
`inner_eq_one_iff_of_norm_one` theorem inner_eq_one_iff_of_norm_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x y : E}, ‖x‖ = 1 → ‖y‖ = 1 → (⟪x, y⟫_𝕜 = 1 ↔ x = y) This theorem states that in an inner product space over a ring that behaves like the real numbers (denoted as `𝕜`) with an associated normed additive commutative group (`E`), if the norm of two vectors `x` and `y` each is `1` (meaning they are unit vectors), then the inner product of these two vectors being `1` implies that the two vectors are identical. This is a specific form of the equality case for the Cauchy-Schwarz inequality. More concisely: In an inner product space over a real-like ring with associated normed additive commutative group, if two unit vectors have an inner product of 1, then they are identical.
`LinearIsometryEquiv.inner_map_map` theorem LinearIsometryEquiv.inner_map_map : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {E' : Type u_7} [inst_3 : NormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (x y : E), ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜 This theorem states that for any type 𝕜, any normed additive commutative group E with an inner product space over 𝕜, and another such group E', if there is a linear isometric equivalence 'f' from E to E', then the inner product of f(x) and f(y) (where x and y are elements of E) is equal to the inner product of x and y. In other words, a linear isometric equivalence preserves the inner product. More concisely: A linear isometric map between two inner product spaces preserves the inner product.
`OrthogonalFamily.independent` theorem OrthogonalFamily.independent : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {V : ι → Submodule 𝕜 E}, (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → CompleteLattice.Independent V This theorem states that if a family of subspaces in an inner product space (over a field and a normed add commutative group) is orthogonal, then it forms an independent family of subspaces. Specifically, any collection of elements, each taken from a different subspace in the orthogonal family, is linearly independent. Additionally, the pairwise intersections of elements of the family are zero. More concisely: If a family of subspaces in an inner product space is orthogonal, then any collection of one element from each subspace is linearly independent and their pairwise intersections are zero.
`inner_self_eq_norm_mul_norm` theorem inner_self_eq_norm_mul_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x : E), RCLike.re ⟪x, x⟫_𝕜 = ‖x‖ * ‖x‖ The theorem `inner_self_eq_norm_mul_norm` states that for any type `𝕜` that is a ring complete (as defined by `RCLike 𝕜`), and any type `E` that is a normed add commutative group and an inner product space over `𝕜`, the real component of the inner product of a vector `x` with itself (denoted by `⟪x, x⟫_𝕜`) is equal to the square of the norm of the vector `x` (denoted by `‖x‖ * ‖x‖`). This is a fundamental property in inner product spaces representing the Pythagorean theorem in any such space. More concisely: For any ring complete `𝕜`, normed add commutative group and inner product space `E` over `𝕜`, the inner product `⟪x, x⟫_𝕜` of a vector `x` with itself equals the square of its norm `‖x‖ * ‖x‖`.
`inner_self_eq_zero` theorem inner_self_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x : E}, ⟪x, x⟫_𝕜 = 0 ↔ x = 0 This theorem states that for any type `𝕜` which behaves like a ring, and any normed add commutative group `E` which is also an inner product space over `𝕜`, the inner product of a vector `x` with itself is zero if and only if the vector `x` itself is the zero vector. This is a fundamental property in the context of inner product spaces. More concisely: For any normed add commutative `𝕜`-module `E` (where `𝕜` is a ring) being an inner product space, the inner product of a vector `x` with itself equals zero if and only if `x` is the zero vector.
`norm_add_sq_real` theorem norm_add_sq_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2 This theorem states that for any normed additively commutative group `F` equipped with a real inner product space, the square of the norm of the sum of any two elements `x` and `y` in `F` can be expressed as the sum of the square of the norm of `x`, twice the real inner product of `x` and `y`, and the square of the norm of `y`. This is akin to the algebraic expansion of the square of a binomial, `(a + b)^2 = a^2 + 2ab + b^2`, but in the context of normed vector spaces. More concisely: For any normed additively commutative group `F` endowed with a real inner product, the norm of the sum of two elements `x` and `y` squared equals the sum of the squares of their norms, plus twice the real inner product of `x` and `y`.
`inner_conj_symm` theorem inner_conj_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜 This theorem, `inner_conj_symm`, states that for any two elements `x` and `y` in an inner product space `E` over a field `𝕜` that has a star ring endomorphism, the inner product of `y` and `x` conjugated by the star ring endomorphism is equal to the inner product of `x` and `y`. In mathematical terms, it states that ⟨y, x⟩ₖ⁎ = ⟨x, y⟩ₖ for all `x` and `y` in `E`, where ⟨., .⟩ₖ is the inner product in the space `E`. More concisely: For any inner product space E over a field with a star ring endomorphism, the conjugated inner product of y and x equals the inner product of x and y, i.e., ⟨y, x⟩ₖ⁎ = ⟨x, y⟩ₖ for all x and y in E.
`inner_smul_right` theorem inner_smul_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E) (r : 𝕜), ⟪x, r • y⟫_𝕜 = r * ⟪x, y⟫_𝕜 This theorem, named `inner_smul_right`, states that for any inner product space `E` over a field `𝕜` and any two vectors `x` and `y` from this space and a scalar `r` from the field, the inner product of `x` and the scalar multiplication of `r` and `y` is equal to the scalar `r` multiplied by the inner product of `x` and `y`. In terms of mathematics, it can be written as ⟪x, r • y⟫_𝕜 = r * ⟪x, y⟫_𝕜. This theorem essentially captures one of the key properties of inner product spaces related to scalar multiplication. More concisely: For any inner product space, the inner product of a vector with a scalar times another vector is equal to the scalar times the inner product of the two vectors.
`inner_neg_right` theorem inner_neg_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ⟪x, -y⟫_𝕜 = -⟪x, y⟫_𝕜 The theorem `inner_neg_right` states that for any two elements `x` and `y` of an inner product space `E` over a scalar field `𝕜` (with `𝕜` being a field that behaves like real or complex numbers and `E` being a normed additive commutative group), the inner product of `x` and the negation of `y` is equal to the negation of the inner product of `x` and `y`. In mathematical notation, this is `⟪x, -y⟫_𝕜 = -⟪x, y⟫_𝕜`. More concisely: For any inner product space E over field 𝕜, the inner product of an element x with the negation of another element y is the negative of their inner product, i.e., ⟪x, -y⟫_𝕜 = -⟪x, y⟫_𝕜.
`inner_lt_one_iff_real_of_norm_one` theorem inner_lt_one_iff_real_of_norm_one : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F}, ‖x‖ = 1 → ‖y‖ = 1 → (⟪x, y⟫_ℝ < 1 ↔ x ≠ y) The theorem `inner_lt_one_iff_real_of_norm_one` states that for any two unit vectors `x` and `y` in a real inner product space, the inner product of `x` and `y` being strictly less than `1` implies that `x` and `y` are distinct. Conversely, if `x` and `y` are distinct, their inner product is strictly less than `1`. This theorem is a specific case of the Cauchy-Schwarz inequality, which bounds the inner product of two vectors in terms of their norms. More concisely: In a real inner product space, two distinct unit vectors have an inner product strictly less than 1, while two unit vectors with an inner product strictly less than 1 are distinct.
`inner_add_right` theorem inner_add_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y z : E), ⟪x, y + z⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜 This theorem, named `inner_add_right`, states that for any type `𝕜` and `E`, where `𝕜` has a structure of a ring-like ordered field (`RCLike 𝕜`) and `E` is a normed additive commutative group with an inner product space over `𝕜` (`InnerProductSpace 𝕜 E`), the inner product of `x` with the sum of `y` and `z` (denoted by `⟪x, y + z⟫_𝕜`) equals to the sum of the inner product of `x` with `y` and the inner product of `x` with `z` (denoted by `⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜`). This theorem is a property of inner product spaces reflecting the distributivity of the inner product with respect to vector addition on the right. More concisely: For any ring-like ordered field `𝕜` and inner product space `𝕜[E]`, the inner product of `x` with the sum of `y` and `z` equals the sum of the inner products of `x` with `y` and `z`.
`ext_inner_right` theorem ext_inner_right : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x y : E}, (∀ (v : E), ⟪x, v⟫_𝕜 = ⟪y, v⟫_𝕜) → x = y The theorem `ext_inner_right` states that in any inner product space `E` over a field `𝕜`, if two vectors `x` and `y` have the same inner product with every other vector `v` in the space, then `x` and `y` are equal. This essentially means that a vector is uniquely defined by its inner products with all other vectors in the space. More concisely: If two vectors in an inner product space have the same inner product with every other vector, then they are equal.
`abs_real_inner_le_norm` theorem abs_real_inner_le_norm : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), \|⟪x, y⟫_ℝ\| ≤ ‖x‖ * ‖y‖ This is a theorem stating the Cauchy-Schwarz inequality in the context of normed additive commutative groups and inner product spaces over the real numbers. For any two elements `x` and `y` of a normed additive commutative group `F` that also forms an inner product space over the real numbers, the absolute value of their inner product is less than or equal to the product of their norms. More concisely: For any two elements in a real inner product space, the inner product of the elements is less than or equal to the product of their norms.
`parallelogram_law` theorem parallelogram_law : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x y : E}, ⟪x + y, x + y⟫_𝕜 + ⟪x - y, x - y⟫_𝕜 = 2 * (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜) This theorem states the parallelogram law in the context of inner product spaces. Given an underlying field 𝕜 and a normed additively commutative group E which forms an inner product space, for any two elements x and y in E, the inner product of x + y with itself plus the inner product of x - y with itself equals twice the sum of the inner product of x with itself and the inner product of y with itself. In vector notation, this corresponds to the assertion that \|\|x+y\|\|² + \|\|x-y\|\|² = 2(\|\|x\|\|² + \|\|y\|\|²), a fundamental identity in the geometry of inner product spaces. More concisely: In an inner product space E over field 𝕜, the norms of x and y satisfy the parallelogram identity: \|\|x+y\|\|² + \|\|x-y\|\|² = 2(\|\|x\|\|² + \|\|y\|\|²).
`OrthogonalFamily.summable_iff_norm_sq_summable` theorem OrthogonalFamily.summable_iff_norm_sq_summable : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)] [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E}, OrthogonalFamily 𝕜 G V → ∀ [inst_5 : CompleteSpace E] (f : (i : ι) → G i), (Summable fun i => (V i) (f i)) ↔ Summable fun i => ‖f i‖ ^ 2 The theorem `OrthogonalFamily.summable_iff_norm_sq_summable` states that for a given family `f` of mutually-orthogonal elements of a normed additively commutative group `E` over a field `𝕜` with an inner product space structure, the family `f` is summable if and only if the function mapping each index `i` to the square of the norm of `f i` is summable. This holds under the assumption that `E` is a complete space, and each `G i` is a normed additively commutative group with an inner product space structure, and there are linear isometric embeddings `V` from each `G i` to `E`. More concisely: A family of mutually orthogonal elements in a complete, inner product space over a field is summable if and only if the function mapping each element to the square of its norm is summable.
`inner_eq_zero_symm` theorem inner_eq_zero_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x y : E}, ⟪x, y⟫_𝕜 = 0 ↔ ⟪y, x⟫_𝕜 = 0 This theorem states that for any types `𝕜` and `E`, given `𝕜` has a structure of `RCLike` (i.e., it behaves like a ring with conjugation), `E` is a normed add commutative group, and `E` is also an inner product space over `𝕜`, the inner product of two elements `x` and `y` of `E` is zero if and only if the inner product of `y` and `x` is also zero. This means the condition of zero inner product is symmetric with respect to the two elements. More concisely: For any type `𝕜` with an `RCLike` structure and `E` a normed add commutative group and inner product space over `𝕜`, the inner product is symmetric: `∀ x y : E, x ⋅ y = y ⋅ x`.
`InnerProductSpace.Core.conj_symm` theorem InnerProductSpace.Core.conj_symm : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x y : F), (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜 This theorem states that the inner product operation is hermitian in an inner product space, which means that taking the complex conjugate of the inner product between two vectors x and y is equal to the inner product of y and x. In other words, swapping the arguments of the inner product and taking the complex conjugate of the result gives the same answer as the original inner product. This property holds for any type `𝕜`, which is a ring like ℝ or ℂ, and any type `F`, which is a module over `𝕜`. More concisely: The inner product is hermitian if and only if the inner product of a vector x with another vector y is equal to the complex conjugate of the inner product of y with x.
`Orthonormal.inner_finsupp_eq_zero` theorem Orthonormal.inner_finsupp_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ {s : Set ι} {i : ι}, i ∉ s → ∀ {l : ι →₀ 𝕜}, l ∈ Finsupp.supported 𝕜 𝕜 s → ⟪(Finsupp.total ι E 𝕜 v) l, v i⟫_𝕜 = 0 This theorem states that for any orthonormal set of vectors `v` in an inner product space, if you construct a linear combination of some subset `s` of these vectors, then this linear combination is orthogonal (i.e., has an inner product of zero) to any vector in the orthonormal set not included in `s`. The linear combination is represented as an element `l` of the space of functions supported on `s`, and the inner product is defined over some scalar field `𝕜`. In other words, if a vector is not included in the subset used to form the linear combination, it is orthogonal to the result of the linear combination. More concisely: For any orthonormal set of vectors `v` in an inner product space and any subset `s` of these vectors, the linear combination of vectors in `s` is orthogonal to any vector in `v` not in `s`.
`norm_sub_sq_eq_norm_sq_add_norm_sq_real` theorem norm_sub_sq_eq_norm_sq_add_norm_sq_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F}, ⟪x, y⟫_ℝ = 0 → ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ This theorem is a variant of the Pythagorean theorem, specifically applied to the context of vector spaces with an inner product. It states that for any two vectors `x` and `y` in a normed additively commutative group (a type of vector space) that also has a real inner product space structure, if the inner product of `x` and `y` is zero, then the square of the norm (length) of the vector difference `x - y` equals the sum of the squares of the norms of `x` and `y`. This is essentially saying that in such a vector space, if two vectors are orthogonal (meaning their inner product is zero), then the Pythagorean theorem holds for the lengths of these vectors and their difference. More concisely: In a normed additively commutative group with a real inner product space structure, if two vectors have zero inner product, then the square of the difference of their norms equals the sum of the squares of their individual norms.
`Orthonormal.inner_left_right_finset` theorem Orthonormal.inner_left_right_finset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {s : Finset ι} {v : ι → E}, Orthonormal 𝕜 v → ∀ {a : ι → ι → 𝕜}, (s.sum fun i => s.sum fun j => a i j • ⟪v j, v i⟫_𝕜) = s.sum fun k => a k k The theorem `Orthonormal.inner_left_right_finset` postulates that for any field `𝕜`, normed add commutative group `E`, and inner product space `E` over `𝕜`, given an orthonormal sequence `v` indexed by type `ι`, and a finite set `s` of type `ι`, the double sum of the inner products of pairs of vectors from `v`, each weighted by a function `a`, is equal to the sum of the weights `a k k` for all `k` in `s`. In other words, the weighted inner products sum up to the sum of the weights over the set `s` when the vectors form an orthonormal sequence. The weights `a` are assumed to be from `𝕜`, the scalars in the inner product space. More concisely: For any orthonormal sequence `v` over a field `𝕜` in a normed add commutative group and inner product space `E`, and any finite set `s` of indices from `𝕜`, the double sum of `a(i) ⊤ v(i) ⊤ v(j) a(j)` over `i, j` in `s` equals the sum of `a(k)²` over `k` in `s`.
`orthonormal_subtype_range` theorem orthonormal_subtype_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Function.Injective v → (Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v) The theorem `orthonormal_subtype_range` states that for any types `𝕜`, `E`, and `ι`, and any function `v` mapping from `ι` to `E`, provided that `𝕜` has a real-like structure, `E` is a normed additive commutative group and an inner product space over `𝕜`, then, if `v` is an injective function, the family `v` is orthonormal if and only if the function `Subtype.val`, when applied to the range of `v`, is also orthonormal. Here, `Subtype.val` is a function that takes a subtype and returns the underlying element of the base type. An orthonormal set of vectors means that each vector has a norm of 1 and any pair of different vectors are orthogonal to each other (their inner product is equal to zero). More concisely: For a real-like structure `𝕜`, a normed additive commutative group and inner product space `E` over `𝕜`, and an injective function `v` from `ι` to `E`, the family `{v i \| i ∈ ι}` is orthonormal if and only if the family `{Subtype.val (v "" i) \| i ∈ ι}` is orthonormal.
`Finsupp.inner_sum` theorem Finsupp.inner_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} (l : ι →₀ 𝕜) (v : ι → E) (x : E), ⟪x, l.sum fun i a => a • v i⟫_𝕜 = l.sum fun i a => a • ⟪x, v i⟫_𝕜 This theorem, named `Finsupp.inner_sum`, states that for any type `𝕜` that behaves like a ring, a type `E` that constitutes a normed additive commutative group, and `𝕜` and `E` together forming an inner product space, the inner product of a vector `x` with the sum of scaled vectors (`a` scaled `v i`, where `a` belongs to the `Finsupp` (finite support) type `ι →₀ 𝕜` and `v i` belongs to the type `ι → E`) is equal to the sum of scaled inner products (`a` scaled `⟪x, v i⟫_𝕜`). This corresponds to the distributive property of the inner product over a finite sum. More concisely: For any normed additive commutative group `E` over a ring `𝕜`, the inner product of a vector `x` with the finite sum of scaled vectors `α i ⋅ v i` is equal to the sum of the scaled inner products `α i ⋅ ⟨x, v i⟩_𝕜`.
`InnerProductSpace.norm_sq_eq_inner` theorem InnerProductSpace.norm_sq_eq_inner : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [self : InnerProductSpace 𝕜 E] (x : E), ‖x‖ ^ 2 = RCLike.re ⟪x, x⟫_𝕜 This theorem states that for any inner product space over a field `𝕜` that behaves like the real or complex numbers (denoted by `RCLike 𝕜`) and a normed additive commutative group `E`, the square of the norm of any element `x` in `E` is equal to the real part of the inner product of `x` with itself. Essentially, it is stating that in such a space, the norm induced by the inner product satisfies the property ‖x‖² = Re⟨x, x⟩ for all `x` in `E`. More concisely: In an inner product space over a field behaving like the real or complex numbers and a normed additive commutative group, the norm of an element squared equals the real part of its inner product with itself.
`inner_eq_sum_norm_sq_div_four` theorem inner_eq_sum_norm_sq_div_four : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ⟪x, y⟫_𝕜 = (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - RCLike.I • y‖ ^ 2 - ↑‖x + RCLike.I • y‖ ^ 2) * RCLike.I) / 4 This theorem, known as the Polarization Identity, relates the inner product of two vectors in an inner product space to the norms of certain linear combinations of these vectors. Specifically, for any two vectors `x` and `y` in an inner product space over a scalar field `𝕜` (with an associated structure given by `RCLike`), the inner product of `x` and `y` is equal to a quarter of the difference between the squares of the norms of `x + y` and `x - y`, plus the difference between the squares of the norms of `x - RCLike.I • y` and `x + RCLike.I • y`, all multiplied by the imaginary unit `RCLike.I`. In mathematical notation, this can be written as: ⟪x, y⟫ = (‖x + y‖² - ‖x - y‖² + (‖x - iy‖² - ‖x + iy‖²) * i) / 4, where ⟪ , ⟫ represents the inner product, ‖ ‖ represents the norm, `i` is the imaginary unit, and `*` represents scalar multiplication. More concisely: The inner product of two vectors in an inner product space equals a quarter of the difference between the squared norms of their sum and difference, plus the difference between the squared norms of the vectors multiplied by the imaginary unit, all in the scalar field with `RCLike` structure.
`norm_sub_pow_two_real` theorem norm_sub_pow_two_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2 The theorem `norm_sub_pow_two_real` states that for any two elements `x` and `y` from a real Inner Product Space `F`, the square of the norm of their difference equals to the square of the norm of `x` minus twice the inner product of `x` and `y`, plus the square of the norm of `y`. In mathematical terminology, this theorem states that ‖x - y‖² = ‖x‖² - 2 * ⟪x, y⟫ + ‖y‖² for any x,y ∈ F. More concisely: The square of the norm of the difference between two elements in a real Inner Product Space equals the sum of the differences of their squared norms and twice their inner product.
`real_inner_self_eq_norm_sq` theorem real_inner_self_eq_norm_sq : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F), ⟪x, x⟫_ℝ = ‖x‖ ^ 2 := by sorry This theorem states that for every element `x` in an inner product space `F` over the real numbers, the inner product of `x` with itself (`⟪x, x⟫_ℝ`) is equal to the square of the norm of `x` (`‖x‖ ^ 2`). In other words, it represents the Pythagorean theorem in the context of real inner product spaces: the square of the length of a vector is equal to the square of its components summed together. More concisely: For every element `x` in a real inner product space, the inner product of `x` with itself equals the square of its norm: `⟪x, x⟫_ℝ = ‖x‖ ^ 2`.
`parallelogram_law_with_norm` theorem parallelogram_law_with_norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst : InnerProductSpace 𝕜 E] (x y : E), ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) This theorem states the parallelogram law with respect to the norm in the context of an inner product space. Given any type 𝕜 that operates like the real or complex numbers, and any normed additive commutative group E that also forms an inner product space with 𝕜, the theorem states that for any two elements x and y in E, the sum of the squared norms of x+y and x-y is equal to twice the sum of the squared norms of x and y. In mathematical notation, ‖x + y‖² + ‖x - y‖² = 2 * (‖x‖² + ‖y‖²). More concisely: In an inner product space E over normed field 𝕜, the norm of the sum (difference) of two vectors x and y is equal to the norm of x plus (minus) the norm of y, added (subtracted) twice: ‖x + y‖² = ‖x‖² + ‖y‖² ± 2‖x‖‖y‖.
`norm_inner_eq_norm_iff` theorem norm_inner_eq_norm_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x y : E}, x ≠ 0 → y ≠ 0 → (‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖ ↔ ∃ r, r ≠ 0 ∧ y = r • x) This theorem states that for any non-zero vectors `x` and `y` in an inner product space over a scalar field `𝕜` with a normed add commutative group `E`, if the norm of their inner product equals the product of their norms, then there exists a non-zero scalar `r` such that `y` is a scalar multiple of `x`. This is a special case of the equality condition for the Cauchy-Schwarz inequality. More concisely: If two non-zero vectors `x` and `y` in an inner product space satisfy `∣∣x · y∣∣ = ∣∣x∣∣ ∣∣y∣∣, then `y` is a scalar multiple of `x`.*
`inner_add_add_self` theorem inner_add_add_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ⟪x + y, x + y⟫_𝕜 = ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜 The theorem `inner_add_add_self` states that for any type 𝕜 that behaves like a ring (annotated as `RCLike 𝕜`) and any normed, commutative add group E (annotated as `NormedAddCommGroup E`) that forms an inner product space with 𝕜 (annotated as `InnerProductSpace 𝕜 E`), for any two elements x and y of E, the inner product of the sum of x and y with itself (notated as `⟪x + y, x + y⟫_𝕜`) equals the sum of the inner products of x with itself, x with y, y with x, and y with itself (notated as `⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜`). More concisely: For any normed, commutative add group E that is an inner product space over a ring 𝕜, the inner product of the sum of two elements x and y equals the sum of their inner products. That is, ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫.
`Orthonormal.inner_right_sum` theorem Orthonormal.inner_right_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (l : ι → 𝕜) {s : Finset ι} {i : ι}, i ∈ s → ⟪v i, s.sum fun i => l i • v i⟫_𝕜 = l i This theorem states that, given an orthonormal set of vectors within an inner product space, the inner product of a linear combination of a subset of these vectors with one of those vectors will yield the coefficient of that particular vector in the linear combination. In other words, if you have a set of orthonormal vectors, and you form a linear combination of a subset of these vectors, the inner product of this linear combination with one of the vectors in the subset will give you the coefficient of that vector in the linear combination. This property is often used in the context of Fourier Series or Quantum Mechanics, where an orthonormal basis is used to represent elements in an inner product space. More concisely: Given an orthonormal set of vectors in an inner product space, the inner product of a linear combination of some vectors in the set with one of those vectors equals the coefficient of that vector in the linear combination.
`real_inner_smul_left` theorem real_inner_smul_left : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F) (r : ℝ), ⟪r • x, y⟫_ℝ = r * ⟪x, y⟫_ℝ This theorem states that for any real number `r` and any two elements `x` and `y` from an inner product space over the real numbers (`ℝ`), the inner product of `r` scaled by `x` and `y` is equal to `r` multiplied by the inner product of `x` and `y`. In other words, scaling one of the vectors in the inner product by a real number is the same as scaling the result of the inner product by that number. This is a property of the distributivity of scalar multiplication over the inner product in real inner product spaces. More concisely: For any real number r and elements x, y of an inner product space over the real numbers, r <⟩x,y⟩ = ⟨x, y⟩ ⋅ r, where <⟩denotes the inner product.
`norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero` theorem norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0 This theorem is a variant of the Pythagorean theorem in the context of inner product spaces over the real numbers. Specifically, it states that for any two vectors `x` and `y` in a normed additively commutative group that also forms an inner product space over the real numbers, the squared norm of the sum of `x` and `y` equals the sum of the squared norms of `x` and `y` if and only if the real inner product of `x` and `y` is zero. In other words, the vectors `x` and `y` are orthogonal (perpendicular) if and only if the Pythagorean relation holds for their norms. More concisely: In a real inner product space, two vectors are orthogonal if and only if the sum of their squared norms equals the square of the norm of their sum.
`norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul` theorem norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x : E} {r : 𝕜}, x ≠ 0 → r ≠ 0 → ‖⟪x, r • x⟫_𝕜‖ / (‖x‖ * ‖r • x‖) = 1 The theorem `norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul` states that for any non-zero vector `x` and any non-zero scalar `r` in an inner product space over a ring `𝕜`, the absolute value of the inner product of `x` and the scaled vector `r • x`, divided by the product of their norms, is always 1. In mathematical terms, this can be written as: if `x ≠ 0` and `r ≠ 0`, then `\|⟪x, r • x⟫_𝕜\| / (‖x‖ * ‖r • x‖) = 1`. More concisely: For any non-zero vector `x` and non-zero scalar `r` in an inner product space over a ring, the quotient of the inner product of `x` and `r • x` by the product of their norms equals 1. That is, `\|⟪x, r • x⟫_𝕜\| / (‖x‖ * ‖r • x‖) = 1`.
`norm_sub_eq_norm_add` theorem norm_sub_eq_norm_add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {v w : E}, ⟪v, w⟫_𝕜 = 0 → ‖w - v‖ = ‖w + v‖ This theorem states that for any two orthogonal vectors `v` and `w` in an inner product space over a scalar field `𝕜`, the norm (or magnitude) of their difference (`w - v`) is equal to the norm of their sum (`w + v`). Orthogonal vectors here mean those vectors whose inner product is zero (`⟪v, w⟫_𝕜 = 0`). The theorem is valid under the assumptions that `𝕜` behaves like a real or complex number field (`RCLike 𝕜`) and `E` forms a normed additive commutative group (`NormedAddCommGroup E`). More concisely: In an inner product space over a real or complex number field, the norm of the difference between two orthogonal vectors is equal to the norm of their sum.
`inner_self_eq_norm_sq_to_K` theorem inner_self_eq_norm_sq_to_K : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x : E), ⟪x, x⟫_𝕜 = ↑‖x‖ ^ 2 This theorem states that for any type `𝕜` which is of type `RCLike`, for another type `E` which is a normed additive commutative group and an inner product space over `𝕜`, the inner product of any element `x` of `E` with itself (denoted as `⟪x, x⟫_𝕜`) is equal to the square of the norm of `x` (denoted as `‖x‖^2`). In other words, in the context of inner product spaces, the inner product of a vector with itself equals the square of its norm. More concisely: For any normed additive commutative group and inner product space `E` over a `RCLike` type `𝕜`, the inner product of any `x` in `E` with itself equals the square of its norm: `⟪x, x⟫_𝕜 = ‖x‖^2`.
`InnerProductSpace.smul_left` theorem InnerProductSpace.smul_left : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [self : InnerProductSpace 𝕜 E] (x y : E) (r : 𝕜), ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜 The theorem `InnerProductSpace.smul_left` states that for any types `𝕜` and `E`, with `𝕜` being a ring that supports the conjugate operation and `E` being a normed commutative additive group that forms an inner product space over `𝕜`, the inner product of the scalar multiplication of a vector `x` by a scalar `r` and another vector `y` is equal to the product of the conjugate of `r` and the inner product of `x` and `y`. In mathematical notation, this could be written as for all `x`, `y` in `E` and `r` in `𝕜`, we have `⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜`. More concisely: For any inner product space `E` over a conjugate-compatible ring `𝕜`, the inner product of the scalar multiplication of a vector by a conjugate-preserving scalar and another vector equals the product of the conjugate of the scalar and the inner product of the vectors.
`Orthonormal.sum_inner_products_le` theorem Orthonormal.sum_inner_products_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} (x : E) {v : ι → E} {s : Finset ι}, Orthonormal 𝕜 v → (s.sum fun i => ‖⟪v i, x⟫_𝕜‖ ^ 2) ≤ ‖x‖ ^ 2 The theorem `Orthonormal.sum_inner_products_le` is a statement of Bessel's inequality for finite sums. For a given type `𝕜`, a normed additive commutative group `E`, and an inner product space over `𝕜` and `E`, it asserts that for any element `x` of `E`, any function `v` from an index set `ι` to `E`, and any finite subset `s` of `ι`, if `v` forms an orthonormal set, then the sum over `s` of the squared norms of the inner products of `v i` with `x` is less than or equal to the square of the norm of `x`. In mathematical terms, if $(v_i)_{i \in I}$ is an orthonormal system in `E`, then for any `x` in `E`, we have $\sum_{i \in s} \\|\langle v_i, x \rangle\\|^2 \leq \\|x\\|^2$ for any finite subset `s` of `I`. More concisely: For any orthonormal system $(v\_i)\_i$ in a normed inner product space and any finite subset $s$ of its index set, the sum of the squares of the inner products of elements from the system with any vector in the space is less than or equal to the square of the norm of that vector, i.e., $\sum\_{i \in s} \\|\langle v\_i, x \rangle\\|^2 \leq \\|x\\|^2$.
`norm_sub_pow_two` theorem norm_sub_pow_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2 This theorem, named `norm_sub_pow_two`, is an alias of another theorem called `norm_sub_sq`. The theorem describes an identity in the context of inner product spaces. Given any field `𝕜` satisfying the `RCLike` structure (essentially having a real component extraction function), a normed add commutative group `E`, and an inner product space built over `𝕜` and `E`, for any two elements `x` and `y` of `E`, the square of the norm of the difference of `x` and `y` equals the square of the norm of `x` minus twice the real component of the inner product of `x` and `y`, plus the square of the norm of `y`. Mathematically, it can be written as ‖x - y‖² = ‖x‖² - 2 * Re(⟪x, y⟫) + ‖y‖². More concisely: The square of the norm of the difference between two elements in an inner product space equals the sum of the squares of their individual norms minus twice the real part of their inner product.
`Orthonormal.inner_finsupp_eq_sum_right` theorem Orthonormal.inner_finsupp_eq_sum_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (l₁ l₂ : ι →₀ 𝕜), ⟪(Finsupp.total ι E 𝕜 v) l₁, (Finsupp.total ι E 𝕜 v) l₂⟫_𝕜 = l₂.sum fun i y => (starRingEnd 𝕜) (l₁ i) * y The theorem `Orthonormal.inner_finsupp_eq_sum_right` states that for any field `𝕜`, any normed add commutative group `E`, provided `E` is an inner product space over the field `𝕜`, for any type `ι` and any function `v` from `ι` to `E`, if `v` constitutes an orthonormal set of vectors, then for any two linear combinations `l₁` and `l₂` of vectors from this orthonormal set (expressed as `Finsupp`), the inner product of these two linear combinations is equal to the sum over the second `Finsupp` `l₂`, where each term in the sum is the product of the complex conjugate of the coefficient in `l₁` for a particular index `i`, and the coefficient in `l₂` for the same index `i`. More concisely: For any inner product space `E` over a field `𝕜` and orthonormal set `v` of vectors in `E`, the inner product of their corresponding `Finsupp` linear combinations is equal to the sum of the products of the complex conjugates of their coefficients and the coefficients of the second linear combination for identical indices.
`real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two` theorem real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x, y⟫_ℝ = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2 This is the Polarization Identity theorem, which describes the real inner product in terms of the norm. For any two vectors `x` and `y` in an inner product space over the real numbers, the inner product of `x` and `y` is equal to one-half the difference between the square of the norm of the sum of `x` and `y` and the sum of the squares of the norms of `x` and `y`. Symbolically, this is expressed as: `⟪x, y⟫_ℝ = (‖x + y‖² - ‖x‖² - ‖y‖²) / 2`. More concisely: The real inner product of two vectors x and y is equal to half the difference between the squared norms of their sum and the sum of their squared norms: ⟪x, y⟫\_ℝ = (‖x + y‖² - ‖x‖² - ‖y‖²) / 2.
`inner_sum` theorem inner_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} (s : Finset ι) (f : ι → E) (x : E), ⟪x, s.sum fun i => f i⟫_𝕜 = s.sum fun i => ⟪x, f i⟫_𝕜 This theorem, called `inner_sum`, states that for any scalar field `𝕜`, any normed additive commutative group `E` equipped with an inner product space over `𝕜`, any finite set `s` indexed by `ι`, any function `f` from `ι` to `E`, and any element `x` from `E`, the inner product of `x` and the sum of the elements in `s` mapped by `f` is equal to the sum of the inner products of `x` and each element in `s` mapped by `f`. In mathematical notation, this would be expressed as ⟪x, ∑ f(i)⟫ = ∑ ⟪x, f(i)⟫ for all `i` in `s`. More concisely: For any scalar field 𝕜, normed additive commutative group E with an inner product over 𝕜, any finite indexed set (ι, s), function f : ι → E, and element x in E, ⟪x, ∑ f(i)⟫ = ∑ ⟪x, f(i)⟫.
`InnerProductSpace.Core.definite` theorem InnerProductSpace.Core.definite : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x : F), ⟪x, x⟫_𝕜 = 0 → x = 0 This theorem states that the inner product in an inner product space is positive definite. In particular, for any field `𝕜` and any type `F` that forms a module over `𝕜` and an additive commutative group, if `x` is an element of `F`, and the inner product of `x` with itself (denoted by ⟪x, x⟫_𝕜) equals zero, then `x` must be the zero element of `F`. This is a fundamental property of inner product spaces in linear algebra. More concisely: In an inner product space over a field, the inner product of an element with itself is positive definite, that is, equal to zero implies the element is the zero element.
`Continuous.inner` theorem Continuous.inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {α : Type u_4} [inst_3 : TopologicalSpace α] {f g : α → E}, Continuous f → Continuous g → Continuous fun t => ⟪f t, g t⟫_𝕜 This theorem states that for any field `𝕜` that behaves like real or complex numbers, and any normed add commutative group `E` that is also an inner product space over `𝕜`, if `f` and `g` are two continuous functions from a topological space `α` to `E`, then the function that maps any element `t` of `α` to the inner product of `f(t)` and `g(t)` in `𝕜` is also continuous. More concisely: For any continuous functions $f$ and $g$ from a topological space $\alpha$ to an inner product space $E$ over a field $\mathbb{F}$ that is also a normed additive commutative group, the function mapping $t \mapsto \langle f(t), g(t) \rangle_{\mathbb{F}}$ is continuous.
`Orthonormal.inner_products_summable` theorem Orthonormal.inner_products_summable : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} (x : E) {v : ι → E}, Orthonormal 𝕜 v → Summable fun i => ‖⟪v i, x⟫_𝕜‖ ^ 2 The theorem `Orthonormal.inner_products_summable` states that for any field `𝕜`, a normed add commutative group `E`, an inner product space of `𝕜` and `E`, and an arbitrary type `ι`, for any vector `x` in `E` and any function `v` that maps from `ι` to `E`, if `v` forms an orthonormal set (which means every vector `v i` has norm 1 and any pair of different vectors `v i` and `v j` are orthogonal), then the sequence of the square of the norms of the inner product of `v i` and `x` is summable. In other words, the infinite sum of squared lengths of the projections of `x` onto each vector in the orthonormal set `v` will converge to a finite number. More concisely: For any orthonormal set {vi : ι → E} in an inner product space (E, ⌈·⌉) over a field 𝕜, the series ∑ i ∈ ι \|\|⌈x, vi i⌉\|² converges for any x ∈ E.
`inner_zero_left` theorem inner_zero_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x : E), ⟪0, x⟫_𝕜 = 0 This theorem, `inner_zero_left`, states that for any scalar type `𝕜` and any normed add commutative group `E` with an inner product space over `𝕜`, the inner product of the zero vector and any vector `x` in `E` is always zero. This is a fundamental property of inner product spaces, essentially stating that the zero vector is orthogonal to all other vectors. More concisely: For any inner product space `(E, ⟨·, ·⟩)` over commutative scalar type `𝕜`, ⟨0, x⟩ = 0 for all `x ∈ E`.
`inner_self_nonneg` theorem inner_self_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x : E}, 0 ≤ RCLike.re ⟪x, x⟫_𝕜 This theorem, named `inner_self_nonneg`, states that for any type `𝕜` that has an `RCLike` structure, and for any `E`, a normed additive commutative group which also forms an inner product space over `𝕜`, the inner product of any element `x` of `E` with itself is always non-negative. Here, `RCLike.re` is a function that maps an element of type `𝕜` to the real number line ℝ. In mathematical terms, the theorem says that for any `x` in `E`, the real component of the inner product of `x` with itself (i.e., ⟨x, x⟩_𝕜) is equal to or greater than 0. More concisely: For any normed additive commutative group `E` over a type `𝕜` with an `RCLike` structure, the inner product of any element `x` in `E` with itself is non-negative (i.e., ⟨x, x⟩_𝕜 ≥ 0).
`abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul` theorem abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F} {r : ℝ}, x ≠ 0 → r ≠ 0 → \|⟪x, r • x⟫_ℝ\| / (‖x‖ * ‖r • x‖) = 1 The theorem states that for any non-zero vector 'x' and any non-zero real number 'r' in a real inner product space, the absolute value of the inner product of the vector with a non-zero multiple of itself, divided by the product of their norms, is always 1. Here, the norm (‖x‖) of a vector 'x' is its length or magnitude, the scalar multiple (r • x) denotes the vector that results from scaling 'x' by factor 'r', and the inner product (⟪x, r • x⟫_ℝ) represents the dot product of 'x' and its scaled version. More concisely: For any non-zero vector x and real number r in a real inner product space, the magnitude of their inner product divided by the product of their norms equals 1. (\|⟪x, r • x⟫_ℝ\| / (‖x‖ * ‖r • x‖) = 1)
`Orthonormal.comp` theorem Orthonormal.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {v : ι → E}, Orthonormal 𝕜 v → ∀ (f : ι' → ι), Function.Injective f → Orthonormal 𝕜 (v ∘ f) The theorem `Orthonormal.comp` states that given an orthonormal family of vectors in an inner product space (which is a set of vectors where each vector has a norm of 1 and any pair of vectors is orthogonal), if we obtain a subfamily of this orthonormal family by composing it with an injective function (a function that doesn't map different inputs to the same output), this subfamily is also an orthonormal family. In other words, selecting vectors from an orthonormal family without repetition (which is ensured by the injectivity of the function) preserves the orthonormal property. More concisely: If `f` is an injective function from an orthonormal family of vectors in an inner product space to itself, then the image of this function is an orthonormal family.
`norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero` theorem norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0 This is a generalization of the Pythagorean theorem to the realm of real inner product spaces. It states that for any two vectors 'x' and 'y' in a real inner product space F, the square of the norm of the vector obtained by subtracting 'y' from 'x' equals the sum of the squares of the norms of 'x' and 'y' if and only if the real inner product of 'x' and 'y' is zero. In other words, 'x' and 'y' are orthogonal (the angle between them is 90 degrees) if and only if the squared length of the difference vector equals the sum of the squared lengths of the original vectors. More concisely: In a real inner product space, two vectors are orthogonal if and only if the square of the norm of their difference is equal to the sum of the squares of their norms.
`norm_sub_sq` theorem norm_sub_sq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2 The theorem `norm_sub_sq` states that for any type `𝕜` that is a real-coefficient-like structure (`RCLike`) and any normed add commutative group `E` that is also an inner product space over `𝕜`, the squared norm (essentially the length squared) of the difference between two elements `x` and `y` of `E` is equal to the squared norm of `x` minus twice the real part of the inner product of `x` and `y` over `𝕜`, plus the squared norm of `y`. This can be seen as a variant of the Pythagorean theorem in an inner product space. More concisely: For any RCLike structure `𝕜` and inner product space `E` over `𝕜`, the squared norm of `x - y` in `E` equals the squared norm of `x` minus twice the inner product of `x` and `y` over `𝕜` plus the squared norm of `y`.
`inner_map_polarization` theorem inner_map_polarization : ∀ {V : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) (x y : V), ⟪T y, x⟫_ℂ = (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ - Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) / 4 The theorem `inner_map_polarization` is a complex polarization identity involving a linear map. This theorem states that for any normed additively commutative group `V` that also forms an inner product space over the complex numbers, and for any linear map `T` from `V` to `V`, and for any vectors `x` and `y` in `V`, the inner product of `T y` and `x` is equal to the expression `(⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ - Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) / 4`. Here, `Complex.I` denotes the imaginary unit, `•` denotes scalar multiplication, and `⟪_ , _⟫_ℂ` denotes the inner product in the complex inner product space. More concisely: For any linear map T between two complex inner product spaces V, and vectors x and y in V, the inner product of T(y) and x equals the complex expression (‖T(x + y)‖\_ℂ^2 + ‖T(x - y)‖\_ℂ^2 + i*(‖T(x + iy)‖\_ℂ^2 - ‖T(x - iy)‖\_ℂ^2)/2, where i is the imaginary unit.
`InnerProductSpace.Core.inner_zero_left` theorem InnerProductSpace.Core.inner_zero_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F), ⟪0, x⟫_𝕜 = 0 This theorem, `InnerProductSpace.Core.inner_zero_left`, states that for any type `𝕜` that behaves like a real or complex number (indicated by `RCLike 𝕜`), and any type `F` that is an additive commutative group and a module over `𝕜` (indicated by `AddCommGroup F` and `Module 𝕜 F`), if we have an inner product space defined on `𝕜` and `F` (indicated by `InnerProductSpace.Core 𝕜 F`), then the inner product of the zero vector and any vector `x` in this space is zero. In mathematical terms, this is expressing the property that inner product of zero vector with any vector is zero: ⟨0, x⟩ = 0. More concisely: For any type `𝕜` behaving like a real or complex number, any additive commutative group and `𝕜`-module `F` with an inner product structure, the inner product of the zero vector and any vector in `F` is zero.
`InnerProductSpace.Core.cauchy_schwarz_aux` theorem InnerProductSpace.Core.cauchy_schwarz_aux : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y : F), InnerProductSpace.Core.normSq (⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y) = InnerProductSpace.Core.normSq x * (InnerProductSpace.Core.normSq x * InnerProductSpace.Core.normSq y - ‖⟪x, y⟫_𝕜‖ ^ 2) This theorem provides a crucial equality used in the proof of the Cauchy-Schwarz inequality in the context of an Inner Product Space. Specifically, it states that for any two elements `x` and `y` from an Inner Product Space over a scalar field `𝕜`, the square of the norm of the difference between the inner product of `x` and `y` scaled by `x` and the inner product of `x` with itself scaled by `y` is equal to the product of the squares of the norms of `x` and `y` minus the square of the norm of the inner product of `x` and `y`. This norm square is computed using the `InnerProductSpace.Core.normSq` function, which returns the real part of the inner product of an element with itself. The theorem avoids the use of squared norms directly to prevent extra rewrites when applying to an inner product space. More concisely: For any two elements `x` and `y` in an Inner Product Space, the square of the dot product of their difference and the scaled versions of themselves is equal to the difference of the squares of their norms.
`real_inner_smul_self_right` theorem real_inner_smul_self_right : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F) (r : ℝ), ⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖) This theorem states that the real inner product of a vector with a scaled version of itself, in a real inner product space, is equal to the scale factor times the square of the norm of the vector. Specifically, for any vector `x` in a normed additively commutative group `F` that also forms a real inner product space, and any real number `r`, the real inner product of `x` and `r` scaled `x` is equal to `r` times the square of the norm of `x`. More concisely: For any vector `x` in a real inner product space `F` and real number `r`, the real inner product of `x` and `r` times `x` equals `r` times the square of the norm of `x`.
`UniformSpace.Completion.inner_coe` theorem UniformSpace.Completion.inner_coe : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (a b : E), ⟪↑E a, ↑E b⟫_𝕜 = ⟪a, b⟫_𝕜 This theorem, `UniformSpace.Completion.inner_coe`, states that for any types `𝕜` and `E`, where `𝕜` is a ring and `E` is a normed-additive-commutative-group with an inner product space over `𝕜`, the inner product of the completion of `E` with respect to `𝕜` of any two elements `a` and `b` of `E` is the same as the inner product of `a` and `b` in the original inner product space `E` over `𝕜`. In simpler terms, taking the completion of an inner product space doesn't change the inner products of the original elements. More concisely: For any normed-additive-commutative `ℝ`-module `E` over a ring `ℝ` with an inner product and completion `ℱ`, the inner product of `ℱ` of any two elements from `E` is equal to their inner product in `E`.
`OrthogonalFamily.comp` theorem OrthogonalFamily.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)] [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E}, OrthogonalFamily 𝕜 G V → ∀ {γ : Type u_6} {f : γ → ι}, Function.Injective f → OrthogonalFamily 𝕜 (fun g => G (f g)) fun g => V (f g) This theorem states that if we have an orthogonal family of subspaces `G` of a normed additive commutative group `E` over a scalar field `𝕜`, then the composition of this orthogonal family with any injective function `f` results in another orthogonal family. Here, orthogonality is defined with respect to the inner product space structure of `E`. The injective function `f` here acts as a mapping from some type `γ` to the index set `ι` of the original orthogonal family. In short, the theorem states that the orthogonality property is preserved under injective mappings in the index set. More concisely: If `G` is an orthogonal family of subspaces of the inner product space `E`, then the composition of `G` with an injective function `f` results in another orthogonal family.
`abs_real_inner_div_norm_mul_norm_eq_one_iff` theorem abs_real_inner_div_norm_mul_norm_eq_one_iff : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), \|⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)\| = 1 ↔ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x The theorem `abs_real_inner_div_norm_mul_norm_eq_one_iff` states that for any two vectors `x` and `y` in a real inner product space, the absolute value of their inner product divided by the product of their norms equals 1 if and only if both vectors are non-zero and there exists a non-zero scalar `r` such that `y` is the scalar multiplication of `r` with `x`. This theorem represents a specific case of equality for the Cauchy-Schwarz inequality. More concisely: For any non-zero vectors x and y in a real inner product space, the absolute value of their inner product equals the product of their norms and 1 if and only if y is a scalar multiple of x.
`isBoundedBilinearMap_inner` theorem isBoundedBilinearMap_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedSpace ℝ E], IsBoundedBilinearMap ℝ fun p => ⟪p.1, p.2⟫_𝕜 This theorem states that for any inner product space `E` over a field `𝕜` which is equipped with a structure of real normed space, the inner product operation is a bounded bilinear map. Bilinearity here means that the inner product operation is linear in each of its two arguments, and boundedness means that there is a real number such that the inner product of any two elements of `E` doesn't exceed this number. These properties are fundamental in functional analysis and are used in many contexts such as the study of operators on Hilbert spaces. More concisely: In an inner product space over a real field with a real norm, the inner product is a bounded, bilinear map.
`norm_sub_mul_self_real` theorem norm_sub_mul_self_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖ This theorem states that for any two elements `x` and `y` of a real inner product space `F`, the square of the norm of their difference is equal to the square of the norm of `x`, minus twice the inner product of `x` and `y`, plus the square of the norm of `y`. This is essentially the expansion of the square of the length of the difference of two vectors in terms of the lengths of the vectors and their inner product. More concisely: The square of the norm of the difference of two elements in a real inner product space is equal to the sum of the differences of their squared norms and twice their inner product.
`inner_sum_smul_sum_smul_of_sum_eq_zero` theorem inner_sum_smul_sum_smul_of_sum_eq_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {ι₁ : Type u_4} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ} (v₁ : ι₁ → F), (s₁.sum fun i => w₁ i) = 0 → ∀ {ι₂ : Type u_5} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (v₂ : ι₂ → F), (s₂.sum fun i => w₂ i) = 0 → ⟪s₁.sum fun i₁ => w₁ i₁ • v₁ i₁, s₂.sum fun i₂ => w₂ i₂ • v₂ i₂⟫_ℝ = (-s₁.sum fun i₁ => s₂.sum fun i₂ => w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2 This theorem states that for any normed additive commutative group `F` with an inner product space over the real numbers, given two finite sets `s₁` and `s₂` each associated with a real-valued weighting function (`w₁` and `w₂` respectively) and a function mapping to `F` (`v₁` and `v₂` respectively), if the sums of the weights in each set equal to zero, then the inner product of the weighted sums of the functions `v₁` and `v₂` is equal to half the negative sum over `s₁` and `s₂` of the product of the weights and the squared norm of the difference between the corresponding elements of `v₁` and `v₂`. More concisely: For any normed additive commutative group `F` with an inner product space over the real numbers, if `w₁, w₂:` Fin Set -> Real, `v₁, v₂:` F -> F, and `s₁, s₂` are finite sets such that `∑ x ∈ s₁ w₁ x = ∑ x ∈ s₂ w₂ x = 0`, then `∫ x ∈ s₁ w₁ x . (v₁ x - v₂ x)⁢(v₁ x - v₂ x) dxdx = -1/2 ∑ x ∈ s₁ w₁ x \|\|v₁ x - v₂ x\|\|²`.
`UniformSpace.Completion.Continuous.inner` theorem UniformSpace.Completion.Continuous.inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {α : Type u_4} [inst_3 : TopologicalSpace α] {f g : α → UniformSpace.Completion E}, Continuous f → Continuous g → Continuous fun x => ⟪f x, g x⟫_𝕜 This theorem states that for any type `𝕜`, any type `E` which is a normed additive commutative group and an inner product space over `𝕜`, and any type `α` which is a topological space, if we have two functions `f` and `g` from `α` to the Hausdorff completion of `E`, then if `f` and `g` are continuous, the function that maps any `x` in `α` to the inner product of `f(x)` and `g(x)` in `𝕜` is also continuous. More concisely: Given a normed additive commutative group and inner product space `E` over a type `𝕜`, two continuous functions `f` and `g` from a topological space `α` to the Hausdorff completion of `E`, the function that maps `x` to the inner product of `f(x)` and `g(x)` is also continuous.
`inner_map_self_eq_zero` theorem inner_map_self_eq_zero : ∀ {V : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V), (∀ (x : V), ⟪T x, x⟫_ℂ = 0) ↔ T = 0 The theorem `inner_map_self_eq_zero` states that for a complex inner product space `V` over the complex numbers, a linear map `T` from `V` to itself is the zero map if and only if the inner product of `T(x)` and `x` is zero for all `x` in `V`. In other words, the condition that for every vector in `V`, the inner product of the image of the vector under `T` and the vector itself equals zero, characterizes the zero linear map. More concisely: A linear map T from a complex inner product space V to itself is the zero map if and only if the inner product of T(x) and x equals zero for all x in V.
`Orthonormal.toSubtypeRange` theorem Orthonormal.toSubtypeRange : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → Orthonormal 𝕜 Subtype.val The theorem `Orthonormal.toSubtypeRange` states that if we have an orthonormal family of vectors `v : ι → E` in an inner product space `E` over a field `𝕜` with a RCLike structure, then the function `Subtype.val : (range v) → E`, which retrieves the underlying vector from each subtype in the range of `v`, also constitutes an orthonormal family. In other words, the orthonormal property is preserved when considering the vectors as elements of a subtype range. More concisely: If `v` is an orthonormal family of vectors in an inner product space, then the underlying vectors in the range of `v` form an orthonormal family.
`Orthonormal.comp_linearIsometryEquiv` theorem Orthonormal.comp_linearIsometryEquiv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [inst_3 : NormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] {v : ι → E}, Orthonormal 𝕜 v → ∀ (f : E ≃ₗᵢ[𝕜] E'), Orthonormal 𝕜 (⇑f ∘ v) This theorem states that a linear isometric equivalence, which is a linear transformation preserving distances, maintains the orthonormality of a set of vectors in an Inner Product Space. In other words, if a set of vectors is orthonormal in an Inner Product Space, then its image under a linear isometric equivalence is also orthonormal. Here, orthonormality means each vector in the set has a norm of 1, and the inner product of any two distinct vectors in the set is zero. More concisely: If T is a linear isometric equivalence on a finite-dimensional inner product space, then T(S) is orthonormal whenever S is an orthonormal set in the space.
`Finsupp.sum_inner` theorem Finsupp.sum_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} (l : ι →₀ 𝕜) (v : ι → E) (x : E), ⟪l.sum fun i a => a • v i, x⟫_𝕜 = l.sum fun i a => (starRingEnd 𝕜) a • ⟪v i, x⟫_𝕜 This theorem states that for any type `𝕜` with a ring-like structure, any type `E` that is a normed commutative additive group and also an inner product space over `𝕜`, and another type `ι`, given a finite support function `l` from `ι` to `𝕜`, a function `v` from `ι` to `E`, and an element `x` of `E`, the inner product of the sum of scaled values of `v` by `l` with `x` is equal to the sum of the scaled inner products of `v` with `x` by the conjugate of `l`. Here, `starRingEnd 𝕜` denotes the conjugation operation in the ring `𝕜`, and `⟪ , ⟫_𝕜` denotes the inner product in the space `E`. More concisely: For any normed commutative additive group `E` over a ring `𝕜` with conjugation ``, and finite support function `l` from `ι` to `𝕜`, the inner product of `x` in `E` with the sum of `l(i) v(i)` over `i` in `ι` equals the sum of `l(i) * (⟪v(i), x⟫_𝕜)` over `i` in `ι`, where `v` is a function from `ι` to `E`.
`re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two` theorem re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), RCLike.re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2 This theorem, named 're_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two', states the polarization identity which relates the real part of the inner product of two vectors to their norms. Specifically, for any field `𝕜` that is RCLike and any normed add commutative group `E` that is also an inner product space, the real part of the inner product of two elements `x` and `y` from `E`, denoted as `RCLike.re ⟪x, y⟫_𝕜`, equals half of the sum of the squares of the norms of `x` and `y`, minus the square of the norm of the difference of `x` and `y`. In mathematical terms, this is expressed as `Re(⟪x, y⟫) = (‖x‖² + ‖y‖² - ‖x - y‖²) / 2`. More concisely: The real part of the inner product of two elements in an RCLike field with respect to a normed add commutative group and inner product space equals half the sum of the squares of their norms minus the square of the norm of their difference.
`InnerProductSpace.Core.inner_add_left` theorem InnerProductSpace.Core.inner_add_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y z : F), ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜 This theorem, `InnerProductSpace.Core.inner_add_left`, states that for any types `𝕜` and `F` where `𝕜` is a ring-like structure and `F` is an additive commutative group that also forms a module over `𝕜`, with `c` being an inner product space core over `𝕜` and `F`, the inner product of the sum of two elements `x` and `y` with a third element `z` is equal to the sum of the inner products of `x` with `z` and `y` with `z`. This is to say, inner product operation is distributive over vector addition on the left side. More concisely: For any inner product space core `c` over commutative ring `𝕜` and additive commutative group `F`, the inner product `��ôt(x + y, z)` equals `��ôt(x, z) + ��ôt(y, z)` for all `x, y, z` in `F`.
`norm_sub_sq_real` theorem norm_sub_sq_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2 This theorem, named `norm_sub_sq_real`, states that for any types `F` which is a normed add commutative group and an inner product space over real numbers, and for any two elements `x` and `y` of type `F`, the square of the norm of the difference of `x` and `y` is equal to the square of the norm of `x` minus two times the inner product of `x` and `y` in real numbers plus the square of the norm of `y`. This is essentially the expansion of the square of the norm of the difference between two elements in such a space. More concisely: For any normed add commutative group and inner product space F over the real numbers, the square of the norm of x - y is equal to the square of the norm of x - y equals the square of the norm of x - y equals the square of the norm of x + the square of the norm of y - 2∥x · y∥, where · denotes the inner product.
`real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul` theorem real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F} {r : ℝ}, x ≠ 0 → 0 < r → ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1 The theorem `real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul` states that for any non-zero vector `x` and positive real number `r`, in an Inner Product Space over the real numbers, the inner product of `x` with `r` times `x`, divided by the product of their norms, equals one. Here, `⟪x, r • x⟫_ℝ` represents the inner product of `x` and `r•x`, `‖x‖` and `‖r • x‖` are the norms of `x` and `r•x`, respectively, and `r•x` represents the scalar multiplication of `r` with `x`. It's a property of inner product spaces that connects the concepts of inner product and norm. More concisely: For any non-zero vector `x` in an inner product space over the real numbers and positive real number `r`, the quotient of the inner product of `x` and `r` times `x` by the product of their norms is equal to 1.
`inner_mul_inner_self_le` theorem inner_mul_inner_self_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ RCLike.re ⟪x, x⟫_𝕜 * RCLike.re ⟪y, y⟫_𝕜 This is the Cauchy-Schwarz inequality for inner product spaces. The theorem states that for any types `𝕜` and `E`, given `𝕜` is an ordered field and `E` is a normed add commutative group with an inner product space over `𝕜`, for any two elements `x` and `y` in `E`, the absolute value of the inner product of `x` and `y` squared is less than or equal to the product of the inner product of `x` with itself and `y` with itself. This is a fundamental inequality in the theory of inner product spaces, often used to prove other theorems. More concisely: For any inner product space over an ordered field, the inner product of two vectors squared is less than or equal to the product of their norms squared.
`real_inner_add_sub_eq_zero_iff` theorem real_inner_add_sub_eq_zero_iff : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ = ‖y‖ This theorem states that for any two vectors `x` and `y` in a real inner product space (a space equipped with a way to multiply vectors and a notion of length), the sum and the difference of these vectors are orthogonal (i.e., their inner product is zero) if and only if they have the same norm (length). In other words, two vectors have the same length if and only if the dot product of their sum and difference is zero. More concisely: In a real inner product space, two vectors have the same norm if and only if their sum and difference are orthogonal.
`inner_sub_left` theorem inner_sub_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y z : E), ⟪x - y, z⟫_𝕜 = ⟪x, z⟫_𝕜 - ⟪y, z⟫_𝕜 The theorem `inner_sub_left` states that for any types `𝕜` and `E` where `𝕜` is a type with some ring-like structure (denoted by `RCLike 𝕜`) and `E` is a normed additive commutative group that also forms an inner product space over `𝕜`, the inner product of the difference of two elements `x` and `y` in `E` with another element `z` in `E` is equal to the difference of the inner products of `x` and `z` and `y` and `z` respectively. In mathematical terms, it says that for all `x`, `y`, and `z` in `E`, the equation `⟪x - y, z⟫_𝕜 = ⟪x, z⟫_𝕜 - ⟪y, z⟫_𝕜` holds true. This theorem represents the distributive property of the inner product operation over subtraction. More concisely: For any normed additive commutative group `E` over a ring-like type `𝕜`, the inner product of the difference of two elements in `E` with a third element is equal to the difference of their individual inner products.
`abs_real_inner_div_norm_mul_norm_le_one` theorem abs_real_inner_div_norm_mul_norm_le_one : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), \|⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)\| ≤ 1 This theorem states that for any type `F` that is a normed-additive-commutative-group and an inner-product-space over the real numbers, for any two vectors `x` and `y` in `F`, the absolute value of the real inner product of `x` and `y` divided by the product of their norms is always less than or equal to 1. This is related to the idea that the cosine of the angle between two non-zero vectors in an inner product space is given by the ratio of the inner product of the vectors and the product of their norms. More concisely: For any normed-additive-commutative-group and inner-product-space F over the real numbers, and any vectors x and y in F, the absolute value of their inner product is less than or equal to the product of their norms.
`inner_add_left` theorem inner_add_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y z : E), ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜 This theorem, named 'inner_add_left', states that for any type 𝕜 and any normed add commutative group E, which also forms an inner product space over 𝕜, the inner product of the sum of two elements (x and y) and a third element z is equal to the sum of the inner products of x and z, and y and z. In mathematical notation, this could be written as: ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜. This property is fundamental to the theory of inner product spaces. More concisely: For any normed add commutative group E that is also an inner product space over field 𝕜, the inner product of the sum of two elements x and y, and a third element z, equals the sum of the inner products of x and z, and y and z: ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜.
`real_inner_div_norm_mul_norm_eq_one_iff` theorem real_inner_div_norm_mul_norm_eq_one_iff : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x This theorem states that for any two vectors `x` and `y` in a real inner product space, the value of their inner product divided by the product of their norms equals one if and only if both vectors are nonzero and one vector is a positive scalar multiple of the other. In more mathematical terms, we have that $\dfrac{⟪x, y⟫_ℝ}{‖x‖ * ‖y‖} = 1$ if and only if $x ≠ 0$ and there exists a positive real number $r$ such that $y = r * x$. More concisely: For any non-zero vectors `x` and `y` in a real inner product space, their inner product equals the product of their norms and one. That is, $⟪x, y⟫\_ℝ = ‖x‖ * ‖y‖ \implies x = r * y$ for some positive scalar $r$.
`InnerProductSpace.Core.inner_mul_inner_self_le` theorem InnerProductSpace.Core.inner_mul_inner_self_le : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y : F), ‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ RCLike.re ⟪x, x⟫_𝕜 * RCLike.re ⟪y, y⟫_𝕜 This is a statement of the Cauchy-Schwarz inequality in the context of inner product spaces. Given an inner product space over a field `𝕜` and a module `F` that forms an additive commutative group and is also a vector space over `𝕜`, the theorem states that for any two vectors `x` and `y` in `F`, the square of the absolute value of the inner product of `x` and `y` (denoted as `‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖`) is less than or equal to the product of the inner products of `x` and `x` and of `y` and `y` (denoted as `RCLike.re ⟪x, x⟫_𝕜 * RCLike.re ⟪y, y⟫_𝕜`). This inequality is a key step in proving that the inner product space is a normed group, specifically for proving the triangle inequality. In the inequality, `RCLike.re` is a function that maps elements of type `K` to real numbers. More concisely: For any inner product space over a field and two of its vectors, the inner product of the vectors multiplied by the conjugate of their dot product is less than or equal to the square of the magnitudes of the vectors' inner products.
`Orthonormal.inner_left_fintype` theorem Orthonormal.inner_left_fintype : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} [inst_3 : Fintype ι] {v : ι → E}, Orthonormal 𝕜 v → ∀ (l : ι → 𝕜) (i : ι), ⟪Finset.univ.sum fun i => l i • v i, v i⟫_𝕜 = (starRingEnd 𝕜) (l i) This theorem states that for any field `𝕜`, any normed additive commutative group `E`, and any inner product space over `E` and `𝕜`, given a type `ι` with a finite number of elements, and a function `v` that maps an element of type `ι` to a vector in `E` such that `v` forms an orthonormal set, for any function `l` from `ι` to `𝕜` and any `i` in `ι`, the inner product of a linear combination of the vectors in `v` (where the coefficients come from `l`) with vector `v i` is equal to the complex conjugate of `l i`. In other words, when you take the inner product of a linear combination of an orthonormal set with one of the vectors in the set, you get back the coefficient of that vector in the linear combination. This is a key property of orthonormal sets in inner product spaces. More concisely: For any orthonormal set `v` in an inner product space over a field `𝕜`, and any function `l` from the index type `ι` to `𝕜`, the inner product of a linear combination of `v` with `v i` equals the complex conjugate of `l i`.
`norm_inner_le_norm` theorem norm_inner_le_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖⟪x, y⟫_𝕜‖ ≤ ‖x‖ * ‖y‖ The theorem `norm_inner_le_norm` is a statement of the Cauchy-Schwarz inequality in the context of an inner product space. Specifically, it says that for any scalar field `𝕜` and any type `E` that forms a normed additive commutative group and also an inner product space over `𝕜`, the norm of the inner product of any two elements `x` and `y` of `E` is less than or equal to the product of the norms of `x` and `y`. In other words, if `⟪., .⟫_𝕜` denotes the inner product and `‖.‖` denotes the norm, then `‖⟪x, y⟫_𝕜‖ ≤ ‖x‖ * ‖y‖` for all `x` and `y` in `E`. More concisely: For any inner product space over a scalar field endowed with a norm, the inner product of any two elements is less than or equal to the product of their respective norms.
`norm_add_mul_self` theorem norm_add_mul_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖ The theorem `norm_add_mul_self` states that for any two elements `x` and `y` of an inner product space over a certain field `𝕜` (which has a property defined by the type class `RCLike`), the square of the norm of `x + y` equals the sum of the square of the norm of `x`, twice the real part of the inner product of `x` and `y`, and the square of the norm of `y`. In mathematical notation, this would be expressed as ‖x + y‖^2 = ‖x‖^2 + 2 Re⟨x, y⟩ + ‖y‖^2. This is essentially the law of cosines in the context of inner product spaces. More concisely: The theorem `norm_add_mul_self` asserts that for elements `x` and `y` in an inner product space over a field `𝕜` with the `RCLike` property, the norm of their sum squared equals the sum of the squares of their individual norms, plus twice the real part of their inner product.
`norm_add_sq_eq_norm_sq_add_norm_sq_real` theorem norm_add_sq_eq_norm_sq_add_norm_sq_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F}, ⟪x, y⟫_ℝ = 0 → ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ This theorem is a variant of the Pythagorean Theorem, in the context of Real Inner Product Spaces. It states that for any two vectors `x` and `y` in a normed additive commutative group `F` which also forms a Real Inner Product Space, if the inner product of `x` and `y` is zero, then the square of the norm (magnitude) of the sum of `x` and `y` is equal to the sum of the squares of the norms of `x` and `y`. In mathematical terms, if `⟪x, y⟫_ℝ = 0`, then `‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖`. This is analogous to the Pythagorean theorem's statement that in a right-angled triangle, the square of the length of the hypotenuse (`c`) is equal to the sum of the squares of the other two sides (`a` and `b`), often expressed as `c^2 = a^2 + b^2`. More concisely: In a real inner product space, if the inner product of two vectors is zero, then the norm of their sum is equal to the sum of their norms.
`ext_inner_map` theorem ext_inner_map : ∀ {V : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (S T : V →ₗ[ℂ] V), (∀ (x : V), ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ S = T The theorem `ext_inner_map` states that for any two linear maps `S` and `T` from a complex vector space `V` to itself, they are equal if and only if, for every vector `x` in `V`, the inner product of `S x` and `x` is equal to the inner product of `T x` and `x`. In mathematical notation, this is expressed as `⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ` for all `x` in `V`. This theorem provides a characterisation of when two linear operators on an inner product space are equal. More concisely: Two linear maps from a complex vector space to itself are equal if and only if they have the same inner product with every vector in the space.
`inner_smul_left` theorem inner_smul_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E) (r : 𝕜), ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜 This theorem, `inner_smul_left`, establishes a property of the inner product operation in the context of an inner product space `E` over a field `𝕜` with a `RCLike` (Regularity and Completeness Like) structure. Specifically, it states that for any two vectors `x` and `y` in `E` and any scalar `r` in `𝕜`, the inner product of the scaled vector `r • x` and `y` is equal to the product of the conjugate of the scalar `r` (represented by `(starRingEnd 𝕜) r`) and the inner product of the original vectors `x` and `y`. This theorem thus encapsulates a form of homogeneity property of the inner product with respect to scalar multiplication. More concisely: For any inner product space E over a field 𝕜 with a RCLike structure, the inner product of a scalar r times a vector x with a vector y is equal to the product of the conjugate of r and the inner product of x and y. In Lean notation, `(∥x, y∥ = (starRingEnd 𝕜) r * ∥x, y∥)`.
`inner_sub_right` theorem inner_sub_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y z : E), ⟪x, y - z⟫_𝕜 = ⟪x, y⟫_𝕜 - ⟪x, z⟫_𝕜 The theorem `inner_sub_right` states that for all elements `x`, `y`, and `z` of an inner product space `E` over a field `𝕜`, the inner product of `x` and the difference `y - z` equals the difference of the inner products of `x` and `y`, and of `x` and `z`. This can be written in mathematical notation as `⟪x, y - z⟫_𝕜 = ⟪x, y⟫_𝕜 - ⟪x, z⟫_𝕜`. Here `⟪., .⟫_𝕜` denotes the inner product operation, `E` is assumed to be a normed additive commutative group, and `𝕜` is assumed to support operations that make it behave like the real or complex numbers. More concisely: The inner product of an element with the difference of two other elements is equal to the difference of their inner products.
`orthonormal_iff_ite` theorem orthonormal_iff_ite : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} [inst_3 : DecidableEq ι] {v : ι → E}, Orthonormal 𝕜 v ↔ ∀ (i j : ι), ⟪v i, v j⟫_𝕜 = if i = j then 1 else 0 This theorem characterizes an indexed set of vectors being orthonormal in an inner product space, given a ring-like structure and a normed additive commutative group. Specifically, it states that a set of vectors `v`, indexed by type `ι`, is orthonormal in the inner product space (over field `𝕜` and vector space `E`) if and only if the inner product of any two distinct vectors in the set is zero, while the inner product of a vector with itself is one. This is equivalent to saying that the inner product of two vectors `v i` and `v j` is equal to the Kronecker delta, which is `1` when `i` and `j` are equal, and `0` otherwise. The theorem relies on the assumption that equality between indices is decidable. More concisely: A set of vectors indexed by type ι in an inner product space over field 𝕜 and vector space E is orthonormal if and only if the inner product of any two distinct vectors is zero and the inner product of a vector with itself is one. Equivalently, the inner product of two vectors is equal to the Kronecker delta.

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.InnerProductSpace.Basic

norm_inner_div_norm_mul_norm_eq_one_iff

theorem norm_inner_div_norm_mul_norm_eq_one_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖⟪x, y⟫_𝕜 / (↑‖x‖ * ↑‖y‖)‖ = 1 ↔ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x

InnerProductSpace.add_left

theorem InnerProductSpace.add_left : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [self : InnerProductSpace 𝕜 E] (x y z : E), ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜

InnerProductSpace.Core.norm_inner_le_norm

theorem InnerProductSpace.Core.norm_inner_le_norm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y : F), ‖⟪x, y⟫_𝕜‖ ≤ ‖x‖ * ‖y‖

Orthonormal.inner_right_finsupp

norm_sub_mul_self

theorem norm_sub_mul_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖

InnerProductSpace.Core.nonneg_re

theorem InnerProductSpace.Core.nonneg_re : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x : F), 0 ≤ RCLike.re ⟪x, x⟫_𝕜

norm_add_pow_two_real

theorem norm_add_pow_two_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2

inner_self_ofReal_re

theorem inner_self_ofReal_re : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x : E), ↑(RCLike.re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜

InnerProductSpace.Core.inner_self_nonneg

theorem InnerProductSpace.Core.inner_self_nonneg : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] {x : F}, 0 ≤ RCLike.re ⟪x, x⟫_𝕜

Orthonormal.comp_linearIsometry

real_inner_div_norm_mul_norm_eq_neg_one_iff

theorem real_inner_div_norm_mul_norm_eq_neg_one_iff : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

inner_map_complex

theorem inner_map_complex : ∀ {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : InnerProductSpace ℝ G] (f : G ≃ₗᵢ[ℝ] ℂ) (x y : G), ⟪x, y⟫_ℝ = ((starRingEnd ℂ) (f x) * f y).re

real_inner_comm

theorem real_inner_comm : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by sorry

real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two

theorem real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x, y⟫_ℝ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2

dist_div_norm_sq_smul

theorem dist_div_norm_sq_smul : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F}, x ≠ 0 → y ≠ 0 → ∀ (R : ℝ), dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y

innerSL_apply_norm

theorem innerSL_apply_norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x : E), ‖(innerSL 𝕜) x‖ = ‖x‖

InnerProductSpace.Core.inner_neg_left

theorem InnerProductSpace.Core.inner_neg_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y : F), ⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜

eq_of_norm_le_re_inner_eq_norm_sq

theorem eq_of_norm_le_re_inner_eq_norm_sq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x y : E}, ‖x‖ ≤ ‖y‖ → RCLike.re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2 → x = y

norm_add_pow_two

theorem norm_add_pow_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * RCLike.re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2

Orthonormal.inner_sum

norm_sub_eq_sqrt_iff_real_inner_eq_zero

theorem norm_sub_eq_sqrt_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F}, ‖x - y‖ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖).sqrt ↔ ⟪x, y⟫_ℝ = 0

im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four

inner_neg_left

theorem inner_neg_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), ⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜

norm_eq_sqrt_real_inner

theorem norm_eq_sqrt_real_inner : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F), ‖x‖ = (⟪x, x⟫_ℝ).sqrt := by sorry

real_inner_mul_inner_self_le

theorem real_inner_mul_inner_self_le : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ

re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two

norm_add_mul_self_real

theorem norm_add_mul_self_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

real_inner_smul_self_left

theorem real_inner_smul_self_left : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F) (r : ℝ), ⟪r • x, x⟫_ℝ = r * (‖x‖ * ‖x‖)

sum_inner

theorem sum_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} (s : Finset ι) (f : ι → E) (x : E), ⟪s.sum fun i => f i, x⟫_𝕜 = s.sum fun i => ⟪f i, x⟫_𝕜

inner_eq_norm_mul_iff

theorem inner_eq_norm_mul_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {x y : E}, ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y

Orthonormal.tsum_inner_products_le

theorem Orthonormal.tsum_inner_products_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} (x : E) {v : ι → E}, Orthonormal 𝕜 v → ∑' (i : ι), ‖⟪v i, x⟫_𝕜‖ ^ 2 ≤ ‖x‖ ^ 2

InnerProductSpace.Core.add_left

theorem InnerProductSpace.Core.add_left : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] (self : InnerProductSpace.Core 𝕜 F) (x y z : F), ⟪x + y, z⟫_𝕜 = ⟪x, z⟫_𝕜 + ⟪y, z⟫_𝕜

InnerProductSpace.Core.inner_self_im

theorem InnerProductSpace.Core.inner_self_im : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x : F), RCLike.im ⟪x, x⟫_𝕜 = 0

norm_add_eq_sqrt_iff_real_inner_eq_zero

theorem norm_add_eq_sqrt_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F}, ‖x + y‖ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖).sqrt ↔ ⟪x, y⟫_ℝ = 0

real_inner_self_eq_norm_mul_norm

theorem real_inner_self_eq_norm_mul_norm : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F), ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖ := by sorry

InnerProductSpace.Core.inner_smul_left

theorem InnerProductSpace.Core.inner_smul_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [c : InnerProductSpace.Core 𝕜 F] (x y : F) {r : 𝕜}, ⟪r • x, y⟫_𝕜 = (starRingEnd 𝕜) r * ⟪x, y⟫_𝕜

re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four

theorem re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x y : E), RCLike.re ⟪x, y⟫_𝕜 = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4

LinearIsometry.orthonormal_comp_iff

continuous_inner

theorem continuous_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E], Continuous fun p => ⟪p.1, p.2⟫_𝕜

Orthonormal.inner_left_sum

linearIndependent_of_ne_zero_of_inner_eq_zero

InnerProductSpace.conj_symm

theorem InnerProductSpace.conj_symm : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [self : InnerProductSpace 𝕜 E] (x y : E), (starRingEnd 𝕜) ⟪y, x⟫_𝕜 = ⟪x, y⟫_𝕜

real_inner_sub_sub_self

theorem real_inner_sub_sub_self : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

`norm_inner_div_norm_mul_norm_eq_one_iff`

`InnerProductSpace.add_left`

`InnerProductSpace.Core.norm_inner_le_norm`

`Orthonormal.inner_right_finsupp`

`norm_sub_mul_self`

`InnerProductSpace.Core.nonneg_re`

`norm_add_pow_two_real`

`inner_self_ofReal_re`

`InnerProductSpace.Core.inner_self_nonneg`

`Orthonormal.comp_linearIsometry`

`real_inner_div_norm_mul_norm_eq_neg_one_iff`

`inner_map_complex`

`real_inner_comm`

`real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two`

`dist_div_norm_sq_smul`

`innerSL_apply_norm`

`InnerProductSpace.Core.inner_neg_left`

`eq_of_norm_le_re_inner_eq_norm_sq`

`norm_add_pow_two`

`Orthonormal.inner_sum`

`norm_sub_eq_sqrt_iff_real_inner_eq_zero`

`im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four`

`inner_neg_left`

`norm_eq_sqrt_real_inner`

`real_inner_mul_inner_self_le`

`re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two`

`norm_add_mul_self_real`

`real_inner_smul_self_left`

`sum_inner`

`inner_eq_norm_mul_iff`

`Orthonormal.tsum_inner_products_le`

`InnerProductSpace.Core.add_left`

`InnerProductSpace.Core.inner_self_im`

`norm_add_eq_sqrt_iff_real_inner_eq_zero`

`real_inner_self_eq_norm_mul_norm`

`InnerProductSpace.Core.inner_smul_left`

`re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four`

`LinearIsometry.orthonormal_comp_iff`

`continuous_inner`

`Orthonormal.inner_left_sum`

`linearIndependent_of_ne_zero_of_inner_eq_zero`

`InnerProductSpace.conj_symm`

`real_inner_sub_sub_self`

`Orthonormal.inner_right_fintype`

`InnerProductSpace.Core.inner_add_add_self`

`Orthonormal.mapLinearIsometryEquiv`

`exists_maximal_orthonormal`

`Submodule.coe_inner`

`orthonormal_subtype_iff_ite`

`norm_eq_sqrt_inner`

`norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero`

`real_inner_add_add_self`

`Orthonormal.orthonormal_of_forall_eq_or_eq_neg`

`inner_zero_right`

`inner_eq_norm_mul_iff_real`

`Orthonormal.linearIndependent`

`InnerProductSpace.Core.smul_left`

`InnerProductSpace.Core.inner_conj_symm`

`real_inner_le_norm`

`norm_add_sq`

`LinearIsometry.inner_map_map`

`real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul`

`Orthonormal.inner_finsupp_eq_sum_left`

`Orthonormal.inner_left_finsupp`

`inner_eq_one_iff_of_norm_one`

`LinearIsometryEquiv.inner_map_map`

`OrthogonalFamily.independent`

`inner_self_eq_norm_mul_norm`

`inner_self_eq_zero`

`norm_add_sq_real`

`inner_conj_symm`

`inner_smul_right`

`inner_neg_right`

`inner_lt_one_iff_real_of_norm_one`