QuadraticForm.toQuadraticForm_associated
theorem QuadraticForm.toQuadraticForm_associated :
∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : CommSemiring S] [inst_4 : Algebra S R] [inst_5 : Invertible 2] (Q : QuadraticForm R M),
((QuadraticForm.associatedHom S) Q).toQuadraticForm = Q
The theorem `QuadraticForm.toQuadraticForm_associated` states that for any Quadratic Form `Q` over a Module `M` with coefficients in a Commutative Ring `R`, and any type `S` with a Commutative Semiring structure and an Algebra structure over `R`, when `Q` is converted to a Linear Map BilinForm through the associatedHom function and then converted back to a Quadratic Form using the `LinearMap.BilinForm.toQuadraticForm` function, the resulting Quadratic Form is equivalent to the original Quadratic Form `Q`. This is under the assumption that the number 2 is invertible in the setting.
More concisely: For any Quadratic Form `Q` over a module `M` with coefficients in a commutative ring `R`, and any commutative semiring `S` with an algebra structure over `R`, if `2` is invertible, then `QuadraticForm.toQuadraticForm_associated Q` is equal to `Q`.
|
QuadraticForm.IsOrtho.symm
theorem QuadraticForm.IsOrtho.symm :
∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{Q : QuadraticForm R M} {x y : M}, Q.IsOrtho x y → Q.IsOrtho y x
The theorem `QuadraticForm.IsOrtho.symm` states that for any commutative semiring `R`, any additive commutative monoid `M` with a module structure over `R`, any quadratic form `Q` on `M`, and any elements `x` and `y` of `M`, if `x` is orthogonal to `y` with respect to `Q`, then `y` is also orthogonal to `x` with respect to `Q`. Essentially, this theorem provides the symmetry property of orthogonality in the context of quadratic forms.
More concisely: If `x` is orthogonal to `y` with respect to quadratic form `Q` in a commutative semiring `R` with module `M`, then `y` is orthogonal to `x` with respect to `Q`.
|
QuadraticForm.map_smul
theorem QuadraticForm.map_smul :
∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (a : R) (x : M), Q (a • x) = a * a * Q x
This theorem, `QuadraticForm.map_smul`, states that for any commutative semiring `R`, add commutative monoid `M`, and `M` being a module over `R`, then for any quadratic form `Q` over `M`, scalar `a` from `R` and vector `x` from `M`, scaling the vector `x` by `a` and then applying the quadratic form is equivalent to multiplying the result of the application of `Q` to `x` by the square of `a`. In mathematical notation, this is saying that $Q(a \cdot x) = a^2 \cdot Q(x)$ for a quadratic form $Q$, scalar $a$, and vector $x$.
More concisely: For any quadratic form $Q$ over a commutative semiring $R$ and an $R$-module $M$, and for any scalar $a$ in $R$ and vector $x$ in $M$, $Q(a \cdot x) = a^2 \cdot Q(x)$.
|
QuadraticForm.polar_add_left_iff
theorem QuadraticForm.polar_add_left_iff :
∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] {f : M → R} {x x' y : M},
QuadraticForm.polar f (x + x') y = QuadraticForm.polar f x y + QuadraticForm.polar f x' y ↔
f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)
This theorem, named `QuadraticForm.polar_add_left_iff`, establishes a relationship for a polar form of a quadratic form in a commutative ring over an additive commutative group. The theorem states that for any elements `x`, `x'` and `y` of the group, and any function `f` from the group to the ring, the polar form of `f` evaluated at `(x + x', y)` is equal to the sum of the polar forms of `f` evaluated at `(x, y)` and `(x', y)` if and only if the sum of `f` evaluated at `(x + x' + y)`, `(x)`, `(x')` and `(y)` is equal to the sum of `f` evaluated at `(x + x')`, `(x' + y)` and `(y + x)`. This lemma is used to express the bilinearity of `QuadraticForm.polar` without the need for subtraction.
More concisely: For a quadratic form `f` over a commutative ring and any elements `x, x', y` in the additive group, the polar forms `QuadraticForm.polar f (x + x' y)` and `QuadraticForm.polar f (x, y) + QuadraticForm.polar f (x', y)` are equal if and only if `f x + f x' + f y = f (x + x') + f (x' + y) + f y`.
|
QuadraticForm.exists_quadraticForm_ne_zero
theorem QuadraticForm.exists_quadraticForm_ne_zero :
∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Invertible 2] {Q : QuadraticForm R M}, QuadraticForm.associated' Q ≠ 0 → ∃ x, Q x ≠ 0
The theorem `QuadraticForm.exists_quadraticForm_ne_zero` states that for any quadratic form `Q` on a module `M` over a commutative ring `R`, if the associated symmetric bilinear form of `Q` is non-zero, then there exists a non-null vector `x` in the module such that the quadratic form `Q` evaluated at `x` is also non-zero. In other words, if a quadratic form has a non-zero associated bilinear form, it also has at least one non-null vector for which the quadratic form is non-zero.
More concisely: If a quadratic form over a commutative ring with a non-zero associated symmetric bilinear form has a non-zero value on some vector, then there exists a non-null vector for which it takes a non-zero value.
|
QuadraticForm.basisRepr_eq_of_iIsOrtho
theorem QuadraticForm.basisRepr_eq_of_iIsOrtho :
∀ {ι : Type u_6} [inst : Fintype ι] {R : Type u_7} {M : Type u_8} [inst_1 : CommRing R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : Invertible 2] (Q : QuadraticForm R M) (v : Basis ι R M),
LinearMap.IsOrthoᵢ (QuadraticForm.associated Q) ⇑v →
Q.basisRepr v = QuadraticForm.weightedSumSquares R fun i => Q (v i)
This theorem states that for a given quadratic form `Q` over a module `M` with a commutative ring `R` and a basis `v` for `M` indexed by `ι`, if the basis vectors are orthogonal with respect to the linear map associated with `Q`, then the basis representation of `Q` is simply the weighted sum of squares of the values of `Q` on the basis vectors.
More concisely: If the basis vectors of a quadratic form over a commutative ring are orthogonal, then the quadratic form is represented by the weighted sum of squares of its values on those basis vectors.
|
QuadraticForm.ext
theorem QuadraticForm.ext :
∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{Q Q' : QuadraticForm R M}, (∀ (x : M), Q x = Q' x) → Q = Q'
This theorem, `QuadraticForm.ext`, states that for any commutative semiring `R` and any additive commutative monoid `M` that is also a module over `R`, if we have two quadratic forms `Q` and `Q'` on `M` such that for every element `x` of `M`, the value of `Q` at `x` equals the value of `Q'` at `x`, then `Q` and `Q'` are actually the same quadratic form. In other words, two quadratic forms are equal if and only if they agree on all elements of the module.
More concisely: Two quadratic forms on a commutative `R`-module `M` are equal if and only if they yield identical values for all elements of `M`.
|
QuadraticForm.choose_exists_companion
theorem QuadraticForm.choose_exists_companion :
∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M), ⋯.choose = Q.polarBilin
This theorem states that in a commutative ring `R` with an additive commutative group `M` that is a module over `R`, for any quadratic form `Q` (a homogeneous polynomial of degree two) on `R` and `M`, the companion bilinear form is unique and is equal to the `polarBilin` of `Q`. The `.choose` function is used to select this unique companion bilinear form. The `QuadraticForm.polar` function calculates the polar form of the quadratic form, which is a bilinear form.
More concisely: In a commutative ring with modules, the unique companion bilinear form of a quadratic form is equal to its polar form.
|
Mathlib.LinearAlgebra.QuadraticForm.Basic._auxLemma.7
theorem Mathlib.LinearAlgebra.QuadraticForm.Basic._auxLemma.7 :
∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{Q : QuadraticForm R M} {x y : M}, Q.IsOrtho x y = (Q (x + y) = Q x + Q y)
The theorem `Mathlib.LinearAlgebra.QuadraticForm.Basic._auxLemma.7` states that for any commutative semiring `R`, an additive commutative monoid `M`, and a module `M` over `R`, given a quadratic form `Q` on `M` and any two elements `x` and `y` of `M`, the proposition that `x` and `y` are orthogonal with respect to the quadratic form `Q` (denoted as `QuadraticForm.IsOrtho Q x y`) is equivalent to the equality `Q (x + y) = Q x + Q y`. In other words, `x` and `y` are orthogonal under the quadratic form `Q` if and only if the value of the form at the sum of `x` and `y` equals the sum of the value of the form at `x` and at `y`.
More concisely: For any commutative semiring `R`, additive commutative monoid `M`, and quadratic form `Q` on `M` over `R`, elements `x` and `y` of `M` are orthogonal with respect to `Q` if and only if `Q(x + y) = Q(x) + Q(y)`.
|
QuadraticForm.polar_smul_left
theorem QuadraticForm.polar_smul_left :
∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (a : R) (x y : M),
QuadraticForm.polar (⇑Q) (a • x) y = a * QuadraticForm.polar (⇑Q) x y
The theorem `QuadraticForm.polar_smul_left` states that for any commutative ring `R`, additively commutative group `M` and `M` being a module over `R`, for any quadratic form `Q` from `R` to `M`, any scalar factor `a` in `R`, and for any `x` and `y` in `M`, the polar form of `Q` evaluated at `a • x` and `y` is equal to `a` times the polar form of `Q` evaluated at `x` and `y`. This can be interpreted as the linearity property of the polar form of a quadratic form with respect to scalar multiplication on the left argument.
More concisely: For any quadratic form Q over a commutative ring R and additively commutative group M, the polar form of Q is left-linearly homogeneous, i.e., Q(ax, y) = a * Q(x, y) for all a in R and x, y in M.
|
QuadraticForm.map_zero
theorem QuadraticForm.map_zero :
∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(Q : QuadraticForm R M), Q 0 = 0
This theorem, `QuadraticForm.map_zero`, states that for any commutative semiring `R`, any additive commutative monoid `M`, and any module (in the sense of abstract algebra) structure over `M` with scalars in `R`, any quadratic form `Q` applied to the zero element in `M` is equal to zero. This is a general property of quadratic forms in linear algebra.
More concisely: For any commutative semiring R, additive commutative monoid M with a module structure over R, and quadratic form Q over M, Q(0) = 0.
|
QuadraticForm.coeFn_smul
theorem QuadraticForm.coeFn_smul :
∀ {S : Type u_1} {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Monoid S] [inst_4 : DistribMulAction S R] [inst_5 : SMulCommClass S R R] (a : S)
(Q : QuadraticForm R M), ⇑(a • Q) = a • ⇑Q
This theorem states that for any commutative semiring `R`, additive commutative monoid `M`, and monoid `S`, given a `QuadraticForm` `Q` over `R` and `M`, and an element `a` of `S`, the action of the scalar `a` on the quadratic form (notated `a • Q`) is equivalent to the action of the scalar on the function given by the quadratic form (notated `a • ⇑Q`). Here the module structure over `M` and `R` is used along with the distributive action of `S` on `R`, and the commutative interaction between the scalar multiplication of `S` and `R` is also taken into account.
More concisely: For any commutative semiring R, additive commutative monoid M, and monoid S, the scalar action on a QuadraticForm Q over R and M, and an element a of S, is equivalent to the scalar action on the function represented by Q.
|
QuadraticForm.toFun_eq_coe
theorem QuadraticForm.toFun_eq_coe :
∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(Q : QuadraticForm R M), Q.toFun = ⇑Q
This theorem states that for any quadratic form `Q`, the function `toFun` applied to `Q` is equivalent to `Q` when cast to a function (denoted by `⇑Q`). This is true for any type `M` and `R`, where `R` is a commutative semiring and `M` is an additive commutative monoid that is also a module over `R`. In more mathematical terms, this means we can treat the quadratic form `Q` as a function itself, instead of explicitly invoking `toFun`.
More concisely: For any quadratic form Q over a commutative semiring R and additive commutative monoid M that is an R-module, the function application `toFun Q` is equivalent to Q when cast to a function.
|