Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Polar rank of the formal mixer quadratic

Lax342547.FormalQuadratic · concepts/Lax342547/FormalQuadratic.lean · lax-342547

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    The formal row variables for each indexed mixer product are disjoint. The quadratic is a sum of products H_i(u_i,v_i), with each middle form nonsingular. Its polar rank is exactly twice the sum of the middle dimensions, including in characteristic two. Affine translations and constant terms do not change the polar form of the binary function.

    Concept map
    2 concepts; 5 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 affine_polar proven

    2 affine_polar_matrix_rank proven

    3 polar_rank proven

    Lean source view on GitHub

    1import Lax342547.MomentSpace
    2import Mathlib.LinearAlgebra.QuadraticForm.Prod
    3import Mathlib.LinearAlgebra.Dimension.Constructions
    4import Mathlib.LinearAlgebra.BilinearForm.Properties
    5import Mathlib.LinearAlgebra.Matrix.Rank
    6
    7/-!
    8---
    9title: Polar rank of the formal mixer quadratic
    10type: lemma
    11---
    12The formal row variables for each indexed mixer product are disjoint.
    13The quadratic is a sum of products H_i(u_i,v_i), with each middle form
    14nonsingular. Its polar rank is exactly twice the sum of the middle
    15dimensions, including in characteristic two. Affine translations and
    16constant terms do not change the polar form of the binary function.
    17-/
    18
    19namespace Lax342547.FormalQuadratic
    20
    21variable {K B : Type} [Field K] [Fintype B] {V : B → Type}
    22 [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
    23
    24abbrev Rows (V : B → Type) := ∀ i, V i × V i
    25
    26def cross (H : ∀ i, LinearMap.BilinForm K (V i)) : LinearMap.BilinForm K (Rows V) :=
    27 ∑ i, (H i).comp ((LinearMap.fst K (V i) (V i)).comp (LinearMap.proj i))
    28 ((LinearMap.snd K (V i) (V i)).comp (LinearMap.proj i))
    29
    30def quadratic (H : ∀ i, LinearMap.BilinForm K (V i)) : QuadraticForm K (Rows V) :=
    31 (cross H).toQuadraticMap
    32
    33axiom polar_rank [∀ i, FiniteDimensional K (V i)]
    34 (H : ∀ i, LinearMap.BilinForm K (V i)) (hH : ∀ i, (H i).Nondegenerate) :
    35 Module.finrank K (LinearMap.range (quadratic H).polarBilin) =
    36 2 * ∑ i, Module.finrank K (V i)
    37
    38open Lax342547.MomentSpace
    39
    40def affinePolar {U : Type} [AddCommGroup U] (f : U → Binary) (u v : U) : Binary :=
    41 f (u + v) + f u + f v + f 0
    42
    43def polarMatrix {I : Type} [DecidableEq I] (f : (I → Binary) → Binary) : Matrix I I Binary :=
    44 fun i j => affinePolar f (Pi.single i 1) (Pi.single j 1)
    45
    46axiom affine_polar {U W : Type} [AddCommGroup U] [Module Binary U]
    47 [AddCommGroup W] [Module Binary W] (C : LinearMap.BilinForm Binary W)
    48 (A : U →ₗ[Binary] W) (w : W) (c : Binary) (u v : U) :
    49 affinePolar (fun z => c + C (w + A z) (w + A z)) u v = (C + C.flip) (A u) (A v)
    50
    51axiom affine_polar_matrix_rank {I W : Type} [Fintype I] [DecidableEq I]
    52 [AddCommGroup W] [Module Binary W] (C : LinearMap.BilinForm Binary W)
    53 (A : (I → Binary) →ₗ[Binary] W) (w : W) (c : Binary) :
    54 (polarMatrix (fun z => c + C (w + A z) (w + A z))).rank =
    55 Module.finrank Binary (LinearMap.range ((C + C.flip).comp A A))
    56
    57end Lax342547.FormalQuadratic
    58
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…