Lax Lean Archive

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

Bilinear parts of ordered evaluations on every atom flavor

Lax342547.BinaryMixer · concepts/Lax342547/BinaryMixer.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 mixed coefficient matrix is defined directly by evaluating the two point inputs. Its free and sharp submatrices are the corresponding ambient matrix restrictions, independently of the tags and flavors. Thus the rank estimates on the always retained blocks imply the required rank bounds on each full flavor parameter space.

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

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

    1 ambientParity_eval proven

    2 bilinearPart_eq proven

    3 block_rank_le proven

    4 parity_free_block proven

    5 pointInput_affine proven

    6 selfGram_parity_sharp_block proven

    Lean source view on GitHub

    1import Lax342547.Atoms
    2import Lax342547.OrderedMixerLaw
    3import Lax342547.SharpMixerLaw
    4
    5/-!
    6---
    7title: Bilinear parts of ordered evaluations on every atom flavor
    8type: lemma
    9---
    10The mixed coefficient matrix is defined directly by evaluating the two
    11point inputs. Its free and sharp submatrices are the corresponding
    12ambient matrix restrictions, independently of the tags and flavors.
    13Thus the rank estimates on the always retained blocks imply the required
    14rank bounds on each full flavor parameter space.
    15-/
    16
    17namespace Lax342547.BinaryMixer
    18
    19open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    20open Lax342547.Atoms Lax342547.AtomDirections
    21
    22abbrev ParameterIndex {k : ℕ} (n : ℕ) (l : Tag k) (f : Flavor k) :=
    23 {i : Base k n // i ∈ retained l f}
    24
    25noncomputable def directions {k n b degree : ℕ} (s : Fin b → Binary)
    26 (l : Tag k) (f : Flavor k) : Matrix (Coordinate k n b degree) (ParameterIndex n l f) Binary := by
    27 classical
    28 exact fun i j => if i.2 = some j.val then selectorEval s i.1 else 0
    29
    30noncomputable def pointInput {k n b degree : ℕ} (s : Fin b → Binary)
    31 {l : Tag k} {f : Flavor k} (p : Parameters n l f) : Vector k n b degree :=
    32 point selectorEval s (parameterValue p)
    33
    34noncomputable def mixedMatrix {P Q : Type} [DecidableEq P] [DecidableEq Q]
    35 (f : (P → Binary) → (Q → Binary) → Binary) : Matrix P Q Binary :=
    36 fun i j => f (Pi.single i 1) (Pi.single j 1) + f (Pi.single i 1) 0 +
    37 f 0 (Pi.single j 1) + f 0 0
    38
    39noncomputable def bilinearPart {k n b degree : ℕ} (A : Moment k n b degree)
    40 (s t : Fin b → Binary) (l m : Tag k) (f g : Flavor k) :
    41 Matrix (ParameterIndex n l f) (ParameterIndex n m g) Binary := by
    42 classical
    43 exact mixedMatrix (fun p q => A.toBilin' (pointInput s p) (pointInput t q))
    44
    45def ambientParity {I F : Type} [Fintype F] (L : F → Matrix I I Binary)
    46 (a b : F → Binary) (E : Matrix I I Binary) (c d : Binary) : Matrix I I Binary :=
    47 (∑ j, (a j • L j + b j • (L j).transpose)) + c • E + d • E.transpose
    48
    49axiom ambientParity_eval {I F : Type} [Fintype I] [DecidableEq I] [Fintype F]
    50 (L : F → Matrix I I Binary) (a b : F → Binary) (E : Matrix I I Binary) (c d : Binary)
    51 (x y : I → Binary) :
    52 (ambientParity L a b E c d).toBilin' x y =
    53 (∑ j, (a j * (L j).toBilin' x y + b j * (L j).toBilin' y x)) +
    54 c * E.toBilin' x y + d * E.toBilin' y x
    55
    56axiom pointInput_affine {k n b degree : ℕ} (s : Fin b → Binary)
    57 {l : Tag k} {f : Flavor k} (p : Parameters n l f) :
    58 pointInput (degree := degree) s p = pointInput s (0 : Parameters n l f) +
    59 (directions s l f).mulVec p
    60
    61axiom bilinearPart_eq {k n b degree : ℕ} (A : Moment k n b degree)
    62 (s t : Fin b → Binary) (l m : Tag k) (f g : Flavor k) :
    63 bilinearPart A s t l m f g = (directions s l f).transpose * A * directions t m g
    64
    65axiom block_rank_le {k n b degree : ℕ} (A : Moment k n b degree)
    66 (s t : Fin b → Binary) (l m : Tag k) (f g : Flavor k)
    67 (c : Fin n → Base k n)
    68 (hc : ∀ i, c i ∈ retained l f) (hd : ∀ i, c i ∈ retained m g) :
    69 ((blockDirections s c).transpose * A * blockDirections t c).rank ≤
    70 (bilinearPart A s t l m f g).rank
    71
    72axiom parity_free_block {k n b degree r : ℕ} {F : Type} [Fintype F]
    73 (hr : 2 * r ≤ n) (hd : 1 ≤ degree)
    74 (L : F → Moment k n b degree) (a b' : F → Binary)
    75 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (c d : Binary) (s t : Fin b → Binary) :
    76 (blockDirections s free).transpose * ambientParity L a b' (selfGram hr hd M) c d *
    77 blockDirections t free =
    78 OrderedMixerLaw.familyParity (blockDirections s free) (blockDirections t free) a b' L
    79
    80axiom selfGram_parity_sharp_block {k n b degree r : ℕ}
    81 (hr : 2 * r ≤ n) (hd : 1 ≤ degree)
    82 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (c d : Binary) (s t : Fin b → Binary) :
    83 (blockDirections (k := k) s sharp).transpose *
    84 (c • selfGram hr hd M + d • (selfGram hr hd M).transpose) * blockDirections t sharp =
    85 c • SharpMixerLaw.weighted (fun a => s a + t a) M +
    86 d • (SharpMixerLaw.weighted (fun a => s a + t a) M).transpose
    87
    88end Lax342547.BinaryMixer
    89
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…