LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.InnerProductSpace.PiL2

`inner_matrix_col_col` theorem inner_matrix_col_col : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_8} {n : Type u_9} [inst_1 : Fintype m] (A B : Matrix m n 𝕜) (i j : n), ⟪(WithLp.equiv 2 (m → 𝕜)).symm (A.transpose i), (WithLp.equiv 2 (m → 𝕜)).symm (B.transpose j)⟫_𝕜 = (A.conjTranspose * B) i j This theorem states that for any type `𝕜` that behaves like a ring and any types `m` and `n` which represent the indices of rows and columns, respectively, if `A` and `B` are matrices with entries in `𝕜`, the inner product of the `i`-th column of `A` and the `j`-th column of `B` is equal to the element at position `(i, j)` in the matrix product of the conjugate transpose of `A` and `B`. The theorem is applicable for matrices with finite number of rows (`Fintype m`). The inner product and the matrix entries are mapped from the `WithLp` space to `𝕜` space using the `WithLp.equiv` equivalence. More concisely: For any ring-like type `𝕜` and finite matrices `A` and `B` over `𝕜`, the `(i, j)`-entry of the matrix product of `A.transpose.conj`.`B` is equal to the inner product of the `i`-th column of `A` and the `j`-th column of `B`.
`Orthonormal.exists_orthonormalBasis_extension` theorem Orthonormal.exists_orthonormalBasis_extension : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {v : Set E} [inst_3 : FiniteDimensional 𝕜 E], Orthonormal 𝕜 Subtype.val → ∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val This theorem states that in a finite-dimensional inner product space, any orthonormal subset can be extended to an orthonormal basis. More specifically, given a finite dimensional inner product space over a certain field, if we have a set of vectors that is orthonormal (i.e., each vector has norm 1 and any pair of distinct vectors is orthogonal), then there exists an extended set and a bijection function such that the original orthonormal set is a subset of the extended set and the bijection function is equivalent to extracting the underlying element from a subtype. More concisely: In a finite-dimensional inner product space, every orthonormal set can be extended to an orthonormal basis.
`OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary` theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (a b : OrthonormalBasis ι 𝕜 E), a.toBasis.toMatrix ⇑b ∈ Matrix.unitaryGroup ι 𝕜 The theorem `OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary` states that for any type `ι`, type `𝕜` with a ring-like structure, and a type `E` that is a normed add commutative group with an inner product space over `𝕜`, given `a` and `b` as orthonormal bases in this space, the change-of-basis matrix from `a` to `b` is a unitary matrix. This means that the matrix that transforms coordinates from basis `a` to basis `b` preserves lengths and angles, as it is in the unitary group of `ι` by `ι` matrices over `𝕜`. The condition of being in the unitary group means that the star-transpose of the matrix is its inverse. This theorem holds for any finite type `ι` and assumes that the equality of elements of `ι` is decidable. More concisely: For any orthonormal bases `a` and `b` of a normed add commutative group `E` over a ring-like type `𝕜` with an inner product space, the change-of-basis matrix from `a` to `b` is a unitary matrix, i.e., it preserves lengths and angles by being in the unitary group of `ι` by `ι` matrices over `𝕜`, where unitary matrices have star-transposes as their inverses.
`OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal` theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal : ∀ {ι : Type u_1} {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : Fintype ι] [inst_3 : DecidableEq ι] (a b : OrthonormalBasis ι ℝ F), a.toBasis.toMatrix ⇑b ∈ Matrix.orthogonalGroup ι ℝ This theorem states that the change-of-basis matrix between two orthonormal bases `a` and `b` is an orthogonal matrix. Here, `a` and `b` are orthonormal bases in an inner product space over the real numbers with a `Fintype ι` index set and a `DecidableEq ι` equality decision procedure. The theorem specifically asserts that the matrix representation of the basis transformation from `a` to `b` belongs to the group of orthogonal matrices of size `ι` over the real numbers (`Matrix.orthogonalGroup ι ℝ`). More concisely: The change-of-basis matrix between two orthonormal bases in a real inner product space is an orthogonal matrix.
`OrthonormalBasis.orthonormal` theorem OrthonormalBasis.orthonormal : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E), Orthonormal 𝕜 ⇑b The theorem `OrthonormalBasis.orthonormal` states that for any set of vectors in an inner product space `E` over field `𝕜`, indexed by type `ι`, if these vectors form an orthonormal basis `b`, then the function `b` mapping from `ι` to `E` possesses the property of orthonormality. The property of orthonormality means that for every vector in the set, the norm is one, and the inner product of any two distinct vectors in the set is zero. This theorem applies to finite types `ι`, and `𝕜` is a field that behaves like real or complex numbers in its operations. More concisely: If `b` is an orthonormal basis of the inner product space `E` over field `𝕜`, then for all `i, j ∈ ι` with `i ≠ j`, we have `∥bi∥ = 1` and `〈bi, bj〉 = 0`.
`EuclideanSpace.norm_eq` theorem EuclideanSpace.norm_eq : ∀ {𝕜 : Type u_8} [inst : RCLike 𝕜] {n : Type u_9} [inst_1 : Fintype n] (x : EuclideanSpace 𝕜 n), ‖x‖ = (Finset.univ.sum fun i => ‖x i‖ ^ 2).sqrt The theorem `EuclideanSpace.norm_eq` states that for any number system `𝕜` that behaves like the real or complex numbers (as indicated by `RCLike 𝕜`), and for any finite type `n` (which effectively denotes the dimension of our Euclidean space), given any point `x` in the `n`-dimensional Euclidean space over `𝕜`, the norm of `x` (denoted by `‖x‖`) is equal to the square root of the sum of squares of the norms of its coordinates. The sum is taken over all coordinates, represented as the elements of the universal finite set denoted by `Finset.univ`. In mathematical terms, if `x` is a point in an `n`-dimensional Euclidean space, the norm of `x` is given by `‖x‖ = sqrt(∑_{i ∈ univ} ‖x_i‖^2)`, where `sqrt` denotes the square root, `∑` denotes the summation and `x_i` are the coordinates of `x`. More concisely: For any number system `𝕜` with `RCLike` structure and any point `x` in an `n`-dimensional Euclidean space over `𝕜`, the norm of `x` is equal to the square root of the sum of the squares of its coordinates' norms.
`Basis.toBasis_toOrthonormalBasis` theorem Basis.toBasis_toOrthonormalBasis : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v), (v.toOrthonormalBasis hv).toBasis = v The theorem `Basis.toBasis_toOrthonormalBasis` states that for any finite-dimensional inner product space `E` over a ring `𝕜` that behaves like real or complex numbers, if we have a basis `v` for `E` and this basis is orthonormal (meaning each basis vector has norm 1 and any pair of different basis vectors are orthogonal), then the basis obtained by converting this orthonormal basis back to a regular basis is the same as the original basis `v`. In other words, the process of converting a basis to an orthonormal basis and then back to a regular basis is an identity operation on the set of orthonormal bases. More concisely: For any finite-dimensional inner product space over a ring behaving like the real or complex numbers, if a basis is orthonormal, then converting it to a regular basis and back yields the original basis.
`OrthonormalBasis.det_to_matrix_orthonormalBasis` theorem OrthonormalBasis.det_to_matrix_orthonormalBasis : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (a b : OrthonormalBasis ι 𝕜 E), ‖a.toBasis.det ⇑b‖ = 1 This theorem states that for any type `ι`, any type `𝕜` which behaves like a ring, a type `E` that is a normed additive commutative group and an inner product space over `𝕜`, and any two orthonormal bases `a` and `b` of `ι` over `𝕜` in `E`; the determinant of the change-of-basis matrix from `a` to `b` has a norm equal to 1. Here, `Fintype ι` asserts that `ι` is a finite type and `DecidableEq ι` asserts that equality between elements of type `ι` is a decidable relation. More concisely: For any finite type `ι`, given orthonormal bases `a` and `b` of a normed additive commutative group and inner product space `E` over a ring `𝕜`, the norm of the change-of-basis matrix from `a` to `b` is equal to 1.
`Mathlib.Analysis.InnerProductSpace.PiL2._auxLemma.2` theorem Mathlib.Analysis.InnerProductSpace.PiL2._auxLemma.2 : ∀ {α : Type u} {a : α} {p : α → Prop}, (a ∈ {x \| p x}) = p a This theorem states that for any type `α`, any value `a` of `α`, and any predicate `p` on `α`, the condition of `a` being in the set of all `x` of type `α` that satisfy `p` is equivalent to `p a` being true. In other words, the membership of `a` in the set defined by `p` is the same as the truth of `p` when applied to `a`. More concisely: For any type `α`, predicate `p` on `α`, and value `a` of type `α`, `a` is in the set `{x : α \| p x}` if and only if `p a` is true.
`EuclideanSpace.single_apply` theorem EuclideanSpace.single_apply : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] (i : ι) (a : 𝕜) (j : ι), EuclideanSpace.single i a j = if j = i then a else 0 The theorem `EuclideanSpace.single_apply` states that for any types `ι` and `𝕜`, where `𝕜` is RCLike and `ι` has decidable equality, given elements `i` and `j` of `ι` and an element `a` of `𝕜`, the application of the `EuclideanSpace.single` function to `i` and `a` at the point `j` is `a` if `j` equals `i` and `0` otherwise. In other words, the function `EuclideanSpace.single` assigns the value `a` to the coordinate indexed by `i` and assigns `0` to all other coordinates in a Euclidean space. More concisely: For any type `ι` with decidable equality and `𝕜` an RCLike ring, the function `EuclideanSpace.single` assigns the value `a` to the `i`-th coordinate and `0` to all other coordinates in a Euclidean space.
`OrthonormalBasis.det_to_matrix_orthonormalBasis_real` theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_real : ∀ {ι : Type u_1} {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : Fintype ι] [inst_3 : DecidableEq ι] (a b : OrthonormalBasis ι ℝ F), a.toBasis.det ⇑b = 1 ∨ a.toBasis.det ⇑b = -1 The theorem `OrthonormalBasis.det_to_matrix_orthonormalBasis_real` states that for any type `ι`, with `F` being a type of a normed additive commutative group that also has an inner product space over the real numbers, and for any finite `ι` that has decidable equality, if `a` and `b` are orthonormal bases in `F`, the determinant of the change-of-basis matrix from `a` to `b` is either 1 or -1. In other words, the change of basis from one orthonormal basis to another doesn't cause any scaling, only rotations and reflections. More concisely: For any finite orthonormal bases `a` and `b` of a real inner product space `F`, the determinant of the change-of-basis matrix from `a` to `b` is either 1 or -1.
`DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate` theorem DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : FiniteDimensional 𝕜 E] {n : ℕ} (hn : FiniteDimensional.finrank 𝕜 E = n) [inst_5 : DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ), (DirectSum.IsInternal.subordinateOrthonormalBasis hn hV hV') a ∈ V (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV') The theorem `DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate` states that for any index set `ι`, scalar field `𝕜` which follows the rules of a ring with commutative multiplication (RCLike), a normed additive commutative group `E` that is also an inner product space over `𝕜`, a finite type `ι`, a finite-dimensional space `E` over `𝕜`, a natural number `n` equal to the finite rank of `E` over `𝕜`, a decidable equality on `ι`, and a direct sum `V` of submodules of `E` that is an internal direct sum, the basis constructed by the method `DirectSum.IsInternal.subordinateOrthonormalBasis` is subordinate to the orthogonal family `V`. In other words, every basis vector obtained from the method `DirectSum.IsInternal.subordinateOrthonormalBasis` belongs to the associated submodule in `V`, determined by the method `DirectSum.IsInternal.subordinateOrthonormalBasisIndex`. More concisely: Given an inner product space `E` over a commutative ring `𝕜` with a finite-dimensional internal direct sum `V` of submodules, the orthonormal basis obtained from `DirectSum.IsInternal.subordinateOrthonormalBasis` belongs to each submodule in `V`.
`inner_matrix_row_row` theorem inner_matrix_row_row : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_8} {n : Type u_9} [inst_1 : Fintype n] (A B : Matrix m n 𝕜) (i j : m), ⟪(WithLp.equiv 2 (n → 𝕜)).symm (A i), (WithLp.equiv 2 (n → 𝕜)).symm (B j)⟫_𝕜 = (B * A.conjTranspose) j i This theorem states that for any field `𝕜` (with elements that can be related by a certain relation `RCLike`), any finite type `n`, any types `m` and `n`, and any two matrices `A` and `B` with entries in `𝕜` and rows indexed by `m` and columns indexed by `n`, the inner product of the `i`-th row of `A` and the `j`-th row of `B` (in the `WithLp` space with `p=2` and underlying type `n → 𝕜`), is equal to the entry at position `(j, i)` of the matrix product of `B` and the conjugate transpose of `A`. This theorem connects the concept of the inner product, which is a central notion in linear algebra and functional analysis, with the operation of matrix multiplication and conjugate transposition. More concisely: For any field `𝕜`, finite type `n`, and matrices `A` and `B` with entries in `𝕜` and sizes `m x n` and `n x m` respectively, the dot product of the `i`-th row of `A` and the `j`-th row of `B` equals the entry at position `(j, i)` in the matrix product of `B` and the conjugate transpose of `A`.
`exists_orthonormalBasis` theorem exists_orthonormalBasis : ∀ (𝕜 : Type u_3) [inst : RCLike 𝕜] (E : Type u_4) [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : FiniteDimensional 𝕜 E], ∃ w b, ⇑b = Subtype.val The theorem `exists_orthonormalBasis` states that for any type `𝕜` with a structure of real or complex numbers (`RCLike 𝕜`), and any type `E` that has the structure of a normed additive commutative group and an inner product space over `𝕜`, if `E` is also a finite-dimensional vector space over `𝕜` (`FiniteDimensional 𝕜 E`), then there exists an orthonormal basis. Specifically, there exist entities `w` and `b` such that the application of `b` yields the underlying element of the type (this is what `⇑b = Subtype.val` means). This theorem essentially guarantees the existence of an orthonormal basis in any finite-dimensional inner product space. More concisely: In any finite-dimensional inner product space over real or complex numbers, there exists an orthonormal basis.
`orthonormalBasis_one_dim` theorem orthonormalBasis_one_dim : ∀ {ι : Type u_1} [inst : Fintype ι] (b : OrthonormalBasis ι ℝ ℝ), (⇑b = fun x => 1) ∨ ⇑b = fun x => -1 This theorem states that for any orthonormal basis of the real numbers ℝ (denoted as `b`), the basis is found to be constituted either entirely by the vector `1` or entirely by the vector `-1`. The type of the index set (`ι`) for the basis is arbitrary and finite. In other words, every element in the basis is equal to either `1` or `-1`, given the orthonormality condition. More concisely: Every finite orthonormal basis of the real numbers consists only of elements equal to 1 or -1.
`OrthonormalBasis.coe_toBasis` theorem OrthonormalBasis.coe_toBasis : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E), ⇑b.toBasis = ⇑b This theorem states that for any type `ι`, any ring `𝕜` where `𝕜` is an instance of `RCLike`, and any type `E` which forms a normed additive commutative group and an inner product space over `𝕜`, if `b` is an orthonormal basis of `E` indexed by `ι` over `𝕜`, then the function obtained by applying the coercion of `b` via the `toBasis` function of `OrthonormalBasis` is the same as the function obtained by directly coercing `b`. In other words, converting an orthonormal basis to a basis doesn't change the basis elements when you map over the index set `ι`. More concisely: For any type `ι`, ring `𝕜`, type `E` forming a normed additive commutative group and inner product space over `𝕜`, and orthonormal basis `b: E ⊓ ι → E` of `E` over `𝕜`, the coercions of `b` via `toBasis` of `OrthonormalBasis` and directly coercing `b` are equal.
`EuclideanSpace.inner_single_left` theorem EuclideanSpace.inner_single_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι), ⟪EuclideanSpace.single i a, v⟫_𝕜 = (starRingEnd 𝕜) a * v i The theorem `EuclideanSpace.inner_single_left` states that for any type `ι` (representing the dimensions of the Euclidean space), any type `𝕜` that behaves like a ring-complemented lattice (indicated by `RCLike 𝕜`), if there exists a decidable equality for `ι` (indicated by `DecidableEq ι`) and the `ι` type is finite (`Fintype ι`), then for any `i` of type `ι`, any `a` of type `𝕜`, and any vector `v` in the Euclidean space of `ι` dimensions over `𝕜`, the inner product of the vector given by `1 : 𝕜` at coordinate `i` and `0 : 𝕜` at all other coordinates with `v` is equal to the conjugate of `a` (given by `(starRingEnd 𝕜) a`) multiplied by the `i`th coordinate of `v`. This theorem essentially describes the behavior of the inner product operation in the standard real/complex Euclidean space when one of the vectors is a standard basis vector. More concisely: For a finite-dimensional Euclidean space over a ring-complemented lattice `𝕜` with decidable equality, the inner product of the standard basis vector `1` at coordinate `i` and a vector `v`, and `(starRingEnd 𝕜) a` times the `i`th coordinate of `v`, is equal.
`EuclideanSpace.orthonormal_single` theorem EuclideanSpace.orthonormal_single : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι], Orthonormal 𝕜 fun i => EuclideanSpace.single i 1 The theorem `EuclideanSpace.orthonormal_single` states that for any set `ι`, any ring-completed field `𝕜`, whenever `ι` has a decidable equality and is finite (as indicated by `Fintype ι`), the vectors formed by the function `EuclideanSpace.single` with the value `1` inputted for each `i` in `ι`, form an orthonormal system. In other words, each of these vectors has a norm of `1`, and the inner product of any two different vectors is `0`, satisfying the conditions of orthonormality. More concisely: For any finite Decidable Type ι and ring-completed field 𝕜, the family of vectors obtained by applying `EuclideanSpace.single 1` to each element of ι forms an orthonormal system in the Euclidean Space over 𝕜.