mathlib3 documentation

linear_algebra.quadratic_form.basic

Quadratic forms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines quadratic forms over a R-module M. A quadratic form on a ring R is a map Q : M → R such that:

quadratic_form.map_smul: Q (a • x) = a * a * Q x
quadratic_form.polar_add_left, quadratic_form.polar_add_right, quadratic_form.polar_smul_left, quadratic_form.polar_smul_right: the map quadratic_form.polar Q := λ x y, Q (x + y) - Q x - Q y is bilinear.

This notion generalizes to semirings using the approach in [izhakian2016][] which requires that there be a (possibly non-unique) companion bilinear form B such that ∀ x y, Q (x + y) = Q x + Q y + B x y. Over a ring, this B is precisely quadratic_form.polar Q.

To build a quadratic_form from the polar axioms, use quadratic_form.of_polar.

Quadratic forms come with a scalar multiplication, (a • Q) x = Q (a • x) = a * a * Q x, and composition with linear maps f, Q.comp f x = Q (f x).

Main definitions #

quadratic_form.of_polar: a more familiar constructor that works on rings
quadratic_form.associated: associated bilinear form
quadratic_form.pos_def: positive definite quadratic forms
quadratic_form.anisotropic: anisotropic quadratic forms
quadratic_form.discr: discriminant of a quadratic form

Main statements #

quadratic_form.associated_left_inverse,
quadratic_form.associated_right_inverse: in a commutative ring where 2 has an inverse, there is a correspondence between quadratic forms and symmetric bilinear forms
bilin_form.exists_orthogonal_basis: There exists an orthogonal basis with respect to any nondegenerate, symmetric bilinear form B.

Notation #

In this file, the variable R is used when a ring structure is sufficient and R₁ is used when specifically a comm_ring is required. This allows us to keep [module R M] and [module R₁ M] assumptions in the variables without confusion between * from ring and * from comm_ring.

The variable S is used when R itself has a • action.

References #

Tags #

quadratic form, homogeneous polynomial, quadratic polynomial

def quadratic_form.polar {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] (f : M → R) (x y : M) :

R

Up to a factor 2, Q.polar is the associated bilinear form for a quadratic form Q.

Source of this name: https://en.wikipedia.org/wiki/Quadratic_form#Generalization

Equations

quadratic_form.polar f x y = f (x + y) - f x - f y

theorem quadratic_form.polar_add {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] (f g : M → R) (x y : M) :

quadratic_form.polar (f + g) x y = quadratic_form.polar f x y + quadratic_form.polar g x y

theorem quadratic_form.polar_neg {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] (f : M → R) (x y : M) :

quadratic_form.polar (-f) x y = -quadratic_form.polar f x y

theorem quadratic_form.polar_smul {S : Type u_1} {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [monoid S] [distrib_mul_action S R] (f : M → R) (s : S) (x y : M) :

quadratic_form.polar (s • f) x y = s • quadratic_form.polar f x y

theorem quadratic_form.polar_comm {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] (f : M → R) (x y : M) :

quadratic_form.polar f x y = quadratic_form.polar f y x

theorem quadratic_form.polar_add_left_iff {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] {f : M → R} {x x' y : M} :

quadratic_form.polar f (x + x') y = quadratic_form.polar f x y + quadratic_form.polar f x' y ↔ f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)

Auxiliary lemma to express bilinearity of quadratic_form.polar without subtraction.

theorem quadratic_form.polar_comp {S : Type u_1} {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] {F : Type u_3} [ring S] [add_monoid_hom_class F R S] (f : M → R) (g : F) (x y : M) :

quadratic_form.polar (⇑g ∘ f) x y = ⇑g (quadratic_form.polar f x y)

structure quadratic_form (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] :

Type (max u v)

to_fun : M → R
to_fun_smul : ∀ (a : R) (x : M), self.to_fun (a • x) = a * a * self.to_fun x
exists_companion' : ∃ (B : bilin_form R M), ∀ (x y : M), self.to_fun (x + y) = self.to_fun x + self.to_fun y + ⇑B x y

A quadratic form over a module.

For a more familiar constructor when R is a ring, see quadratic_form.of_polar.

Instances for quadratic_form

@[protected, instance]

def quadratic_form.fun_like {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :

fun_like (quadratic_form R M) M (λ (_x : M), R)

Equations

quadratic_form.fun_like = {coe := quadratic_form.to_fun _inst_3, coe_injective' := _}

@[protected, instance]

def quadratic_form.has_coe_to_fun {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :

has_coe_to_fun (quadratic_form R M) (λ (_x : quadratic_form R M), M → R)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

quadratic_form.has_coe_to_fun = {coe := quadratic_form.to_fun _inst_3}

@[simp]

theorem quadratic_form.to_fun_eq_coe {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) :

Q.to_fun = ⇑Q

The simp normal form for a quadratic form is coe_fn, not to_fun.

@[ext]

theorem quadratic_form.ext {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {Q Q' : quadratic_form R M} (H : ∀ (x : M), ⇑Q x = ⇑Q' x) :

Q = Q'

theorem quadratic_form.congr_fun {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {Q Q' : quadratic_form R M} (h : Q = Q') (x : M) :

⇑Q x = ⇑Q' x

theorem quadratic_form.ext_iff {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {Q Q' : quadratic_form R M} :

Q = Q' ↔ ∀ (x : M), ⇑Q x = ⇑Q' x

@[protected]

def quadratic_form.copy {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) (Q' : M → R) (h : Q' = ⇑Q) :

quadratic_form R M

Copy of a quadratic_form with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations

Q.copy Q' h = {to_fun := Q', to_fun_smul := _, exists_companion' := _}

@[simp]

theorem quadratic_form.coe_copy {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) (Q' : M → R) (h : Q' = ⇑Q) :

⇑(Q.copy Q' h) = Q'

theorem quadratic_form.copy_eq {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) (Q' : M → R) (h : Q' = ⇑Q) :

Q.copy Q' h = Q

theorem quadratic_form.map_smul {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) (a : R) (x : M) :

⇑Q (a • x) = a * a * ⇑Q x

theorem quadratic_form.exists_companion {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) :

∃ (B : bilin_form R M), ∀ (x y : M), ⇑Q (x + y) = ⇑Q x + ⇑Q y + ⇑B x y

theorem quadratic_form.map_add_add_add_map {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) (x y z : M) :

⇑Q (x + y + z) + (⇑Q x + ⇑Q y + ⇑Q z) = ⇑Q (x + y) + ⇑Q (y + z) + ⇑Q (z + x)

theorem quadratic_form.map_add_self {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) (x : M) :

⇑Q (x + x) = 4 * ⇑Q x

@[simp]

theorem quadratic_form.map_zero {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) :

⇑Q 0 = 0

@[protected, instance]

def quadratic_form.zero_hom_class {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :

zero_hom_class (quadratic_form R M) M R

Equations

quadratic_form.zero_hom_class = {coe := fun_like.coe quadratic_form.fun_like, coe_injective' := _, map_zero := _}

theorem quadratic_form.map_smul_of_tower {S : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) [comm_semiring S] [algebra S R] [module S M] [is_scalar_tower S R M] (a : S) (x : M) :

⇑Q (a • x) = (a * a) • ⇑Q x

@[simp]

theorem quadratic_form.map_neg {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x : M) :

⇑Q (-x) = ⇑Q x

theorem quadratic_form.map_sub {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x y : M) :

⇑Q (x - y) = ⇑Q (y - x)

@[simp]

theorem quadratic_form.polar_zero_left {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (y : M) :

quadratic_form.polar ⇑Q 0 y = 0

@[simp]

theorem quadratic_form.polar_add_left {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x x' y : M) :

quadratic_form.polar ⇑Q (x + x') y = quadratic_form.polar ⇑Q x y + quadratic_form.polar ⇑Q x' y

@[simp]

theorem quadratic_form.polar_smul_left {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (a : R) (x y : M) :

quadratic_form.polar ⇑Q (a • x) y = a * quadratic_form.polar ⇑Q x y

@[simp]

theorem quadratic_form.polar_neg_left {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x y : M) :

quadratic_form.polar ⇑Q (-x) y = -quadratic_form.polar ⇑Q x y

@[simp]

theorem quadratic_form.polar_sub_left {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x x' y : M) :

quadratic_form.polar ⇑Q (x - x') y = quadratic_form.polar ⇑Q x y - quadratic_form.polar ⇑Q x' y

@[simp]

theorem quadratic_form.polar_zero_right {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (y : M) :

quadratic_form.polar ⇑Q y 0 = 0

@[simp]

theorem quadratic_form.polar_add_right {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x y y' : M) :

quadratic_form.polar ⇑Q x (y + y') = quadratic_form.polar ⇑Q x y + quadratic_form.polar ⇑Q x y'

@[simp]

theorem quadratic_form.polar_smul_right {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (a : R) (x y : M) :

quadratic_form.polar ⇑Q x (a • y) = a * quadratic_form.polar ⇑Q x y

@[simp]

theorem quadratic_form.polar_neg_right {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x y : M) :

quadratic_form.polar ⇑Q x (-y) = -quadratic_form.polar ⇑Q x y

@[simp]

theorem quadratic_form.polar_sub_right {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x y y' : M) :

quadratic_form.polar ⇑Q x (y - y') = quadratic_form.polar ⇑Q x y - quadratic_form.polar ⇑Q x y'

@[simp]

theorem quadratic_form.polar_self {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x : M) :

quadratic_form.polar ⇑Q x x = 2 * ⇑Q x

@[simp]

theorem quadratic_form.polar_bilin_apply {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x y : M) :

⇑(Q.polar_bilin) x y = quadratic_form.polar ⇑Q x y

def quadratic_form.polar_bilin {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) :

quadratic_form.polar as a bilinear form

Equations

Q.polar_bilin = {bilin := quadratic_form.polar ⇑Q, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}

@[simp]

theorem quadratic_form.polar_smul_left_of_tower {S : Type u_1} {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) [comm_semiring S] [algebra S R] [module S M] [is_scalar_tower S R M] (a : S) (x y : M) :

quadratic_form.polar ⇑Q (a • x) y = a • quadratic_form.polar ⇑Q x y

@[simp]

theorem quadratic_form.polar_smul_right_of_tower {S : Type u_1} {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) [comm_semiring S] [algebra S R] [module S M] [is_scalar_tower S R M] (a : S) (x y : M) :

quadratic_form.polar ⇑Q x (a • y) = a • quadratic_form.polar ⇑Q x y

def quadratic_form.of_polar {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (to_fun : M → R) (to_fun_smul : ∀ (a : R) (x : M), to_fun (a • x) = a * a * to_fun x) (polar_add_left : ∀ (x x' y : M), quadratic_form.polar to_fun (x + x') y = quadratic_form.polar to_fun x y + quadratic_form.polar to_fun x' y) (polar_smul_left : ∀ (a : R) (x y : M), quadratic_form.polar to_fun (a • x) y = a • quadratic_form.polar to_fun x y) :

quadratic_form R M

An alternative constructor to quadratic_form.mk, for rings where polar can be used.

Equations

quadratic_form.of_polar to_fun to_fun_smul polar_add_left polar_smul_left = {to_fun := to_fun, to_fun_smul := to_fun_smul, exists_companion' := _}

@[simp]

theorem quadratic_form.of_polar_apply {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (to_fun : M → R) (to_fun_smul : ∀ (a : R) (x : M), to_fun (a • x) = a * a * to_fun x) (polar_add_left : ∀ (x x' y : M), quadratic_form.polar to_fun (x + x') y = quadratic_form.polar to_fun x y + quadratic_form.polar to_fun x' y) (polar_smul_left : ∀ (a : R) (x y : M), quadratic_form.polar to_fun (a • x) y = a • quadratic_form.polar to_fun x y) (ᾰ : M) :

⇑(quadratic_form.of_polar to_fun to_fun_smul polar_add_left polar_smul_left) ᾰ = to_fun ᾰ

theorem quadratic_form.some_exists_companion {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) :

_.some = Q.polar_bilin

In a ring the companion bilinear form is unique and equal to quadratic_form.polar.

@[protected, instance]

def quadratic_form.has_smul {S : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S R] [smul_comm_class S R R] :

has_smul S (quadratic_form R M)

quadratic_form R M inherits the scalar action from any algebra over R.

When R is commutative, this provides an R-action via algebra.id.

Equations

quadratic_form.has_smul = {smul := λ (a : S) (Q : quadratic_form R M), {to_fun := a • ⇑Q, to_fun_smul := _, exists_companion' := _}}

@[simp]

theorem quadratic_form.coe_fn_smul {S : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S R] [smul_comm_class S R R] (a : S) (Q : quadratic_form R M) :

⇑(a • Q) = a • ⇑Q

@[simp]

theorem quadratic_form.smul_apply {S : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S R] [smul_comm_class S R R] (a : S) (Q : quadratic_form R M) (x : M) :

⇑(a • Q) x = a • ⇑Q x

@[protected, instance]

def quadratic_form.has_zero {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :

has_zero (quadratic_form R M)

Equations

quadratic_form.has_zero = {zero := {to_fun := λ (x : M), 0, to_fun_smul := _, exists_companion' := _}}

@[simp]

theorem quadratic_form.coe_fn_zero {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :

⇑0 = 0

@[simp]

theorem quadratic_form.zero_apply {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (x : M) :

⇑0 x = 0

@[protected, instance]

def quadratic_form.inhabited {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :

inhabited (quadratic_form R M)

Equations

quadratic_form.inhabited = {default := 0}

@[protected, instance]

def quadratic_form.has_add {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :

has_add (quadratic_form R M)

Equations

quadratic_form.has_add = {add := λ (Q Q' : quadratic_form R M), {to_fun := ⇑Q + ⇑Q', to_fun_smul := _, exists_companion' := _}}

@[simp]

theorem quadratic_form.coe_fn_add {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q Q' : quadratic_form R M) :

⇑(Q + Q') = ⇑Q + ⇑Q'

@[simp]

theorem quadratic_form.add_apply {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q Q' : quadratic_form R M) (x : M) :

⇑(Q + Q') x = ⇑Q x + ⇑Q' x

@[protected, instance]

def quadratic_form.add_comm_monoid {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :

add_comm_monoid (quadratic_form R M)

Equations

quadratic_form.add_comm_monoid = function.injective.add_comm_monoid coe_fn quadratic_form.add_comm_monoid._proof_2 quadratic_form.coe_fn_zero quadratic_form.coe_fn_add quadratic_form.add_comm_monoid._proof_3

def quadratic_form.coe_fn_add_monoid_hom {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :

quadratic_form R M →+ M → R

@coe_fn (quadratic_form R M) as an add_monoid_hom.

This API mirrors add_monoid_hom.coe_fn.

Equations

quadratic_form.coe_fn_add_monoid_hom = {to_fun := coe_fn quadratic_form.has_coe_to_fun, map_zero' := _, map_add' := _}

@[simp]

theorem quadratic_form.coe_fn_add_monoid_hom_apply {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (x : quadratic_form R M) (ᾰ : M) :

⇑quadratic_form.coe_fn_add_monoid_hom x ᾰ = ⇑x ᾰ

@[simp]

theorem quadratic_form.eval_add_monoid_hom_apply {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (m : M) (ᾰ : quadratic_form R M) :

⇑(quadratic_form.eval_add_monoid_hom m) ᾰ = ⇑ᾰ m

def quadratic_form.eval_add_monoid_hom {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (m : M) :

quadratic_form R M →+ R

Evaluation on a particular element of the module M is an additive map over quadratic forms.

Equations

quadratic_form.eval_add_monoid_hom m = (pi.eval_add_monoid_hom (λ (m : M), R) m).comp quadratic_form.coe_fn_add_monoid_hom

@[simp]

theorem quadratic_form.coe_fn_sum {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} (Q : ι → quadratic_form R M) (s : finset ι) :

⇑(s.sum (λ (i : ι), Q i)) = s.sum (λ (i : ι), ⇑(Q i))

@[simp]

theorem quadratic_form.sum_apply {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} (Q : ι → quadratic_form R M) (s : finset ι) (x : M) :

⇑(s.sum (λ (i : ι), Q i)) x = s.sum (λ (i : ι), ⇑(Q i) x)

@[protected, instance]

def quadratic_form.distrib_mul_action {S : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S R] [smul_comm_class S R R] :

distrib_mul_action S (quadratic_form R M)

Equations

quadratic_form.distrib_mul_action = {to_mul_action := {to_has_smul := quadratic_form.has_smul _inst_6, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}

@[protected, instance]

def quadratic_form.module {S : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [semiring S] [module S R] [smul_comm_class S R R] :

module S (quadratic_form R M)

Equations

quadratic_form.module = {to_distrib_mul_action := quadratic_form.distrib_mul_action _inst_6, add_smul := _, zero_smul := _}

@[protected, instance]

def quadratic_form.has_neg {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] :

has_neg (quadratic_form R M)

Equations

quadratic_form.has_neg = {neg := λ (Q : quadratic_form R M), {to_fun := -⇑Q, to_fun_smul := _, exists_companion' := _}}

@[simp]

theorem quadratic_form.coe_fn_neg {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) :

@[simp]

theorem quadratic_form.neg_apply {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (x : M) :

(⇑-Q) x = -⇑Q x

@[protected, instance]

def quadratic_form.has_sub {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] :

has_sub (quadratic_form R M)

Equations

quadratic_form.has_sub = {sub := λ (Q Q' : quadratic_form R M), (Q + -Q').copy (⇑Q - ⇑Q') _}

@[simp]

theorem quadratic_form.coe_fn_sub {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q Q' : quadratic_form R M) :

⇑(Q - Q') = ⇑Q - ⇑Q'

@[simp]

theorem quadratic_form.sub_apply {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (Q Q' : quadratic_form R M) (x : M) :

⇑(Q - Q') x = ⇑Q x - ⇑Q' x

@[protected, instance]

def quadratic_form.add_comm_group {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] :

add_comm_group (quadratic_form R M)

Equations

quadratic_form.add_comm_group = function.injective.add_comm_group coe_fn quadratic_form.add_comm_group._proof_3 quadratic_form.add_comm_group._proof_4 quadratic_form.add_comm_group._proof_5 quadratic_form.coe_fn_neg quadratic_form.coe_fn_sub quadratic_form.add_comm_group._proof_6 quadratic_form.add_comm_group._proof_7

def quadratic_form.comp {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {N : Type v} [add_comm_monoid N] [module R N] (Q : quadratic_form R N) (f : M →ₗ[R] N) :

quadratic_form R M

Compose the quadratic form with a linear function.

Equations

Q.comp f = {to_fun := λ (x : M), ⇑Q (⇑f x), to_fun_smul := _, exists_companion' := _}

@[simp]

theorem quadratic_form.comp_apply {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {N : Type v} [add_comm_monoid N] [module R N] (Q : quadratic_form R N) (f : M →ₗ[R] N) (x : M) :

⇑(Q.comp f) x = ⇑Q (⇑f x)

def linear_map.comp_quadratic_form {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {S : Type u_1} [comm_semiring S] [algebra S R] [module S M] [is_scalar_tower S R M] (f : R →ₗ[S] S) (Q : quadratic_form R M) :

quadratic_form S M

Compose a quadratic form with a linear function on the left.

Equations

f.comp_quadratic_form Q = {to_fun := λ (x : M), ⇑f (⇑Q x), to_fun_smul := _, exists_companion' := _}

@[simp]

theorem linear_map.comp_quadratic_form_apply {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {S : Type u_1} [comm_semiring S] [algebra S R] [module S M] [is_scalar_tower S R M] (f : R →ₗ[S] S) (Q : quadratic_form R M) (x : M) :

⇑(f.comp_quadratic_form Q) x = ⇑f (⇑Q x)

def quadratic_form.lin_mul_lin {R : Type u_2} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] (f g : M →ₗ[R] R) :

quadratic_form R M

The product of linear forms is a quadratic form.

Equations

quadratic_form.lin_mul_lin f g = {to_fun := ⇑f * ⇑g, to_fun_smul := _, exists_companion' := _}

@[simp]

theorem quadratic_form.lin_mul_lin_apply {R : Type u_2} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] (f g : M →ₗ[R] R) (x : M) :

⇑(quadratic_form.lin_mul_lin f g) x = ⇑f x * ⇑g x

@[simp]

theorem quadratic_form.add_lin_mul_lin {R : Type u_2} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] (f g h : M →ₗ[R] R) :

quadratic_form.lin_mul_lin (f + g) h = quadratic_form.lin_mul_lin f h + quadratic_form.lin_mul_lin g h

@[simp]

theorem quadratic_form.lin_mul_lin_add {R : Type u_2} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] (f g h : M →ₗ[R] R) :

quadratic_form.lin_mul_lin f (g + h) = quadratic_form.lin_mul_lin f g + quadratic_form.lin_mul_lin f h

@[simp]

theorem quadratic_form.lin_mul_lin_comp {R : Type u_2} {M : Type u_4} [comm_semiring R] [add_comm_monoid M] [module R M] {N : Type v} [add_comm_monoid N] [module R N] (f g : M →ₗ[R] R) (h : N →ₗ[R] M) :

(quadratic_form.lin_mul_lin f g).comp h = quadratic_form.lin_mul_lin (f.comp h) (g.comp h)

@[simp]

theorem quadratic_form.sq_apply {R : Type u_2} [comm_semiring R] (ᾰ : R) :

⇑quadratic_form.sq ᾰ = ᾰ * ᾰ

def quadratic_form.sq {R : Type u_2} [comm_semiring R] :

quadratic_form R R

sq is the quadratic form mapping the vector x : R₁ to x * x

Equations

quadratic_form.sq = quadratic_form.lin_mul_lin linear_map.id linear_map.id

def quadratic_form.proj {R : Type u_2} [comm_semiring R] {n : Type u_5} (i j : n) :

quadratic_form R (n → R)

proj i j is the quadratic form mapping the vector x : n → R₁ to x i * x j

Equations

quadratic_form.proj i j = quadratic_form.lin_mul_lin (linear_map.proj i) (linear_map.proj j)

@[simp]

theorem quadratic_form.proj_apply {R : Type u_2} [comm_semiring R] {n : Type u_5} (i j : n) (x : n → R) :

⇑(quadratic_form.proj i j) x = x i * x j

Associated bilinear forms #

Over a commutative ring with an inverse of 2, the theory of quadratic forms is basically identical to that of symmetric bilinear forms. The map from quadratic forms to bilinear forms giving this identification is called the associated quadratic form.

def bilin_form.to_quadratic_form {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) :

quadratic_form R M

A bilinear form gives a quadratic form by applying the argument twice.

Equations

B.to_quadratic_form = {to_fun := λ (x : M), ⇑B x x, to_fun_smul := _, exists_companion' := _}

@[simp]

theorem bilin_form.to_quadratic_form_apply {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) (x : M) :

⇑(B.to_quadratic_form) x = ⇑B x x

@[simp]

theorem bilin_form.to_quadratic_form_zero (R : Type u_2) (M : Type u_4) [semiring R] [add_comm_monoid M] [module R M] :

0.to_quadratic_form = 0

@[simp]

theorem bilin_form.to_quadratic_form_add {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (B₁ B₂ : bilin_form R M) :

(B₁ + B₂).to_quadratic_form = B₁.to_quadratic_form + B₂.to_quadratic_form

@[simp]

theorem bilin_form.to_quadratic_form_smul {S : Type u_1} {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [monoid S] [distrib_mul_action S R] [smul_comm_class S R R] (a : S) (B : bilin_form R M) :

(a • B).to_quadratic_form = a • B.to_quadratic_form

def bilin_form.to_quadratic_form_add_monoid_hom (R : Type u_2) (M : Type u_4) [semiring R] [add_comm_monoid M] [module R M] :

bilin_form R M →+ quadratic_form R M

bilin_form.to_quadratic_form as an additive homomorphism

Equations

bilin_form.to_quadratic_form_add_monoid_hom R M = {to_fun := bilin_form.to_quadratic_form _inst_3, map_zero' := _, map_add' := _}

@[simp]

theorem bilin_form.to_quadratic_form_add_monoid_hom_apply (R : Type u_2) (M : Type u_4) [semiring R] [add_comm_monoid M] [module R M] (B : bilin_form R M) :

⇑(bilin_form.to_quadratic_form_add_monoid_hom R M) B = B.to_quadratic_form

@[simp]

theorem bilin_form.to_quadratic_form_list_sum {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (B : list (bilin_form R M)) :

B.sum.to_quadratic_form = (list.map bilin_form.to_quadratic_form B).sum

@[simp]

theorem bilin_form.to_quadratic_form_multiset_sum {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (B : multiset (bilin_form R M)) :

B.sum.to_quadratic_form = (multiset.map bilin_form.to_quadratic_form B).sum

@[simp]

theorem bilin_form.to_quadratic_form_sum {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} (s : finset ι) (B : ι → bilin_form R M) :

(s.sum (λ (i : ι), B i)).to_quadratic_form = s.sum (λ (i : ι), (B i).to_quadratic_form)

@[simp]

theorem bilin_form.to_quadratic_form_eq_zero {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} :

B.to_quadratic_form = 0 ↔ B.is_alt

theorem bilin_form.polar_to_quadratic_form {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x y : M) :

quadratic_form.polar (λ (x : M), ⇑B x x) x y = ⇑B x y + ⇑B y x

@[simp]

theorem bilin_form.to_quadratic_form_neg {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (B : bilin_form R M) :

(-B).to_quadratic_form = -B.to_quadratic_form

@[simp]

theorem bilin_form.to_quadratic_form_sub {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] (B₁ B₂ : bilin_form R M) :

(B₁ - B₂).to_quadratic_form = B₁.to_quadratic_form - B₂.to_quadratic_form

def quadratic_form.associated_hom (S : Type u_1) {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [comm_semiring S] [algebra S R] [invertible 2] :

quadratic_form R M →ₗ[S] bilin_form R M

associated_hom is the map that sends a quadratic form on a module M over R to its associated symmetric bilinear form. As provided here, this has the structure of an S-linear map where S is a commutative subring of R.

Over a commutative ring, use associated, which gives an R-linear map. Over a general ring with no nontrivial distinguished commutative subring, use associated', which gives an additive homomorphism (or more precisely a ℤ-linear map.)

Equations

quadratic_form.associated_hom S = {to_fun := λ (Q : quadratic_form R M), ⟨⅟ 2 _inst_8, _⟩ • Q.polar_bilin, map_add' := _, map_smul' := _}

@[simp]

theorem quadratic_form.associated_apply (S : Type u_1) {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [comm_semiring S] [algebra S R] [invertible 2] (Q : quadratic_form R M) (x y : M) :

⇑(⇑(quadratic_form.associated_hom S) Q) x y = ⅟ 2 * (⇑Q (x + y) - ⇑Q x - ⇑Q y)

theorem quadratic_form.associated_is_symm (S : Type u_1) {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [comm_semiring S] [algebra S R] [invertible 2] (Q : quadratic_form R M) :

(⇑(quadratic_form.associated_hom S) Q).is_symm

@[simp]

theorem quadratic_form.associated_comp (S : Type u_1) {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [comm_semiring S] [algebra S R] [invertible 2] (Q : quadratic_form R M) {N : Type v} [add_comm_group N] [module R N] (f : N →ₗ[R] M) :

⇑(quadratic_form.associated_hom S) (Q.comp f) = (⇑(quadratic_form.associated_hom S) Q).comp f f

theorem quadratic_form.associated_to_quadratic_form (S : Type u_1) {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [comm_semiring S] [algebra S R] [invertible 2] (B : bilin_form R M) (x y : M) :

⇑(⇑(quadratic_form.associated_hom S) B.to_quadratic_form) x y = ⅟ 2 * (⇑B x y + ⇑B y x)

theorem quadratic_form.associated_left_inverse (S : Type u_1) {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [comm_semiring S] [algebra S R] [invertible 2] {B₁ : bilin_form R M} (h : B₁.is_symm) :

⇑(quadratic_form.associated_hom S) B₁.to_quadratic_form = B₁

theorem quadratic_form.to_quadratic_form_associated (S : Type u_1) {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [comm_semiring S] [algebra S R] [invertible 2] (Q : quadratic_form R M) :

(⇑(quadratic_form.associated_hom S) Q).to_quadratic_form = Q

theorem quadratic_form.associated_right_inverse (S : Type u_1) {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [comm_semiring S] [algebra S R] [invertible 2] :

function.right_inverse ⇑(quadratic_form.associated_hom S) bilin_form.to_quadratic_form

theorem quadratic_form.associated_eq_self_apply (S : Type u_1) {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [comm_semiring S] [algebra S R] [invertible 2] (Q : quadratic_form R M) (x : M) :

⇑(⇑(quadratic_form.associated_hom S) Q) x x = ⇑Q x

@[reducible]

def quadratic_form.associated' {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [invertible 2] :

quadratic_form R M →ₗ[ℤ ] bilin_form R M

associated' is the ℤ-linear map that sends a quadratic form on a module M over R to its associated symmetric bilinear form.

@[protected, instance]

def quadratic_form.can_lift {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [invertible 2] :

can_lift (bilin_form R M) (quadratic_form R M) ⇑(quadratic_form.associated_hom ℕ) bilin_form.is_symm

Symmetric bilinear forms can be lifted to quadratic forms

Equations

quadratic_form.can_lift = {prf := _}

theorem quadratic_form.exists_quadratic_form_ne_zero {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [invertible 2] {Q : quadratic_form R M} (hB₁ : ⇑quadratic_form.associated' Q ≠ 0) :

∃ (x : M), ⇑Q x ≠ 0

There exists a non-null vector with respect to any quadratic form Q whose associated bilinear form is non-zero, i.e. there exists x such that Q x ≠ 0.

@[reducible]

def quadratic_form.associated {R₁ : Type u_3} {M : Type u_4} [comm_ring R₁] [add_comm_group M] [module R₁ M] [invertible 2] :

quadratic_form R₁ M →ₗ[R₁] bilin_form R₁ M

associated is the linear map that sends a quadratic form over a commutative ring to its associated symmetric bilinear form.

@[simp]

theorem quadratic_form.associated_lin_mul_lin {R₁ : Type u_3} {M : Type u_4} [comm_ring R₁] [add_comm_group M] [module R₁ M] [invertible 2] (f g : M →ₗ[R₁] R₁) :

⇑quadratic_form.associated (quadratic_form.lin_mul_lin f g) = ⅟ 2 • (bilin_form.lin_mul_lin f g + bilin_form.lin_mul_lin g f)

def quadratic_form.anisotropic {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) :

Prop

An anisotropic quadratic form is zero only on zero vectors.

Equations

Q.anisotropic = ∀ (x : M), ⇑Q x = 0 → x = 0

theorem quadratic_form.not_anisotropic_iff_exists {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (Q : quadratic_form R M) :

¬Q.anisotropic ↔ ∃ (x : M) (H : x ≠ 0), ⇑Q x = 0

theorem quadratic_form.anisotropic.eq_zero_iff {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {Q : quadratic_form R M} (h : Q.anisotropic) {x : M} :

⇑Q x = 0 ↔ x = 0

theorem quadratic_form.nondegenerate_of_anisotropic {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [invertible 2] (Q : quadratic_form R M) (hB : Q.anisotropic) :

(⇑quadratic_form.associated' Q).nondegenerate

The associated bilinear form of an anisotropic quadratic form is nondegenerate.

def quadratic_form.pos_def {M : Type u_4} {R₂ : Type u} [ordered_ring R₂] [add_comm_monoid M] [module R₂ M] (Q₂ : quadratic_form R₂ M) :

Prop

A positive definite quadratic form is positive on nonzero vectors.

Equations

Q₂.pos_def = ∀ (x : M), x ≠ 0 → 0 < ⇑Q₂ x

theorem quadratic_form.pos_def.smul {M : Type u_4} [add_comm_monoid M] {R : Type u_1} [linear_ordered_comm_ring R] [module R M] {Q : quadratic_form R M} (h : Q.pos_def) {a : R} (a_pos : 0 < a) :

(a • Q).pos_def

theorem quadratic_form.pos_def.nonneg {M : Type u_4} {R₂ : Type u} [ordered_ring R₂] [add_comm_monoid M] [module R₂ M] {Q : quadratic_form R₂ M} (hQ : Q.pos_def) (x : M) :

0 ≤ ⇑Q x

theorem quadratic_form.pos_def.anisotropic {M : Type u_4} {R₂ : Type u} [ordered_ring R₂] [add_comm_monoid M] [module R₂ M] {Q : quadratic_form R₂ M} (hQ : Q.pos_def) :

theorem quadratic_form.pos_def_of_nonneg {M : Type u_4} {R₂ : Type u} [ordered_ring R₂] [add_comm_monoid M] [module R₂ M] {Q : quadratic_form R₂ M} (h : ∀ (x : M), 0 ≤ ⇑Q x) (h0 : Q.anisotropic) :

theorem quadratic_form.pos_def_iff_nonneg {M : Type u_4} {R₂ : Type u} [ordered_ring R₂] [add_comm_monoid M] [module R₂ M] {Q : quadratic_form R₂ M} :

Q.pos_def ↔ (∀ (x : M), 0 ≤ ⇑Q x) ∧ Q.anisotropic

theorem quadratic_form.pos_def.add {M : Type u_4} {R₂ : Type u} [ordered_ring R₂] [add_comm_monoid M] [module R₂ M] (Q Q' : quadratic_form R₂ M) (hQ : Q.pos_def) (hQ' : Q'.pos_def) :

(Q + Q').pos_def

theorem quadratic_form.lin_mul_lin_self_pos_def {M : Type u_4} [add_comm_monoid M] {R : Type u_1} [linear_ordered_comm_ring R] [module R M] (f : M →ₗ[R] R) (hf : linear_map.ker f = ⊥) :

(quadratic_form.lin_mul_lin f f).pos_def

Quadratic forms and matrices #

Connect quadratic forms and matrices, in order to explicitly compute with them. The convention is twos out, so there might be a factor 2⁻¹ in the entries of the matrix. The determinant of the matrix is the discriminant of the quadratic form.

def matrix.to_quadratic_form' {R₁ : Type u_3} {n : Type w} [fintype n] [decidable_eq n] [comm_ring R₁] (M : matrix n n R₁) :

quadratic_form R₁ (n → R₁)

M.to_quadratic_form is the map λ x, col x ⬝ M ⬝ row x as a quadratic form.

Equations

M.to_quadratic_form' = (⇑matrix.to_bilin' M).to_quadratic_form

def quadratic_form.to_matrix' {R₁ : Type u_3} {n : Type w} [fintype n] [decidable_eq n] [comm_ring R₁] [invertible 2] (Q : quadratic_form R₁ (n → R₁)) :

matrix n n R₁

A matrix representation of the quadratic form.

Equations

Q.to_matrix' = ⇑bilin_form.to_matrix' (⇑quadratic_form.associated Q)

theorem quadratic_form.to_matrix'_smul {R₁ : Type u_3} {n : Type w} [fintype n] [decidable_eq n] [comm_ring R₁] [invertible 2] (a : R₁) (Q : quadratic_form R₁ (n → R₁)) :

(a • Q).to_matrix' = a • Q.to_matrix'

theorem quadratic_form.is_symm_to_matrix' {R₁ : Type u_3} {n : Type w} [fintype n] [decidable_eq n] [comm_ring R₁] [invertible 2] (Q : quadratic_form R₁ (n → R₁)) :

Q.to_matrix'.is_symm

@[simp]

theorem quadratic_form.to_matrix'_comp {R₁ : Type u_3} {n : Type w} [fintype n] [comm_ring R₁] [decidable_eq n] [invertible 2] {m : Type w} [decidable_eq m] [fintype m] (Q : quadratic_form R₁ (m → R₁)) (f : (n → R₁) →ₗ[R₁] m → R₁) :

(Q.comp f).to_matrix' = ((⇑linear_map.to_matrix' f).transpose.mul Q.to_matrix').mul (⇑linear_map.to_matrix' f)

def quadratic_form.discr {R₁ : Type u_3} {n : Type w} [fintype n] [comm_ring R₁] [decidable_eq n] [invertible 2] (Q : quadratic_form R₁ (n → R₁)) :

R₁

The discriminant of a quadratic form generalizes the discriminant of a quadratic polynomial.

Equations

Q.discr = Q.to_matrix'.det

theorem quadratic_form.discr_smul {R₁ : Type u_3} {n : Type w} [fintype n] [comm_ring R₁] [decidable_eq n] [invertible 2] {Q : quadratic_form R₁ (n → R₁)} (a : R₁) :

(a • Q).discr = a ^ fintype.card n * Q.discr

theorem quadratic_form.discr_comp {R₁ : Type u_3} {n : Type w} [fintype n] [comm_ring R₁] [decidable_eq n] [invertible 2] {Q : quadratic_form R₁ (n → R₁)} (f : (n → R₁) →ₗ[R₁] n → R₁) :

(Q.comp f).discr = (⇑linear_map.to_matrix' f).det * (⇑linear_map.to_matrix' f).det * Q.discr

theorem bilin_form.nondegenerate_of_anisotropic {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {B : bilin_form R M} (hB : B.to_quadratic_form.anisotropic) :

B.nondegenerate

A bilinear form is nondegenerate if the quadratic form it is associated with is anisotropic.

theorem bilin_form.exists_bilin_form_self_ne_zero {R : Type u_2} {M : Type u_4} [ring R] [add_comm_group M] [module R M] [htwo : invertible 2] {B : bilin_form R M} (hB₁ : B ≠ 0) (hB₂ : B.is_symm) :

∃ (x : M), ¬B.is_ortho x x

There exists a non-null vector with respect to any symmetric, nonzero bilinear form B on a module M over a ring R with invertible 2, i.e. there exists some x : M such that B x x ≠ 0.

theorem bilin_form.exists_orthogonal_basis {V : Type u} {K : Type v} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] [hK : invertible 2] {B : bilin_form K V} (hB₂ : B.is_symm) :

∃ (v : basis (fin (finite_dimensional.finrank K V)) K V), B.is_Ortho ⇑v

Given a symmetric bilinear form B on some vector space V over a field K in which 2 is invertible, there exists an orthogonal basis with respect to B.

noncomputable def quadratic_form.basis_repr {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_6} [fintype ι] (Q : quadratic_form R M) (v : basis ι R M) :

quadratic_form R (ι → R)

Given a quadratic form Q and a basis, basis_repr is the basis representation of Q.

Equations

Q.basis_repr v = Q.comp ↑(v.equiv_fun.symm)

@[simp]

theorem quadratic_form.basis_repr_apply {R : Type u_2} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_6} [fintype ι] {v : basis ι R M} (Q : quadratic_form R M) (w : ι → R) :

⇑(Q.basis_repr v) w = ⇑Q (finset.univ.sum (λ (i : ι), w i • ⇑v i))

def quadratic_form.weighted_sum_squares {S : Type u_1} (R₁ : Type u_3) [comm_semiring R₁] {ι : Type u_6} [fintype ι] [monoid S] [distrib_mul_action S R₁] [smul_comm_class S R₁ R₁] (w : ι → S) :

quadratic_form R₁ (ι → R₁)

The weighted sum of squares with respect to some weight as a quadratic form.

The weights are applied using •; typically this definition is used either with S = R₁ or [algebra S R₁], although this is stated more generally.

Equations

quadratic_form.weighted_sum_squares R₁ w = finset.univ.sum (λ (i : ι), w i • quadratic_form.proj i i)

@[simp]

theorem quadratic_form.weighted_sum_squares_apply {S : Type u_1} {R₁ : Type u_3} [comm_semiring R₁] {ι : Type u_6} [fintype ι] [monoid S] [distrib_mul_action S R₁] [smul_comm_class S R₁ R₁] (w : ι → S) (v : ι → R₁) :

⇑(quadratic_form.weighted_sum_squares R₁ w) v = finset.univ.sum (λ (i : ι), w i • (v i * v i))

theorem quadratic_form.basis_repr_eq_of_is_Ortho {ι : Type u_6} [fintype ι] {R₁ : Type u_1} {M : Type u_2} [comm_ring R₁] [add_comm_group M] [module R₁ M] [invertible 2] (Q : quadratic_form R₁ M) (v : basis ι R₁ M) (hv₂ : (⇑quadratic_form.associated Q).is_Ortho ⇑v) :

Q.basis_repr v = quadratic_form.weighted_sum_squares R₁ (λ (i : ι), ⇑Q (⇑v i))

On an orthogonal basis, the basis representation of Q is just a sum of squares.