Lax Lean Archive

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

Boolean point moments with restricted base coordinates

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

definition

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

    Definition

    The selector evaluations and the constant/base coordinates of §2.3. Keeping the selector evaluation map as a parameter lets the coordinate projection arguments apply at every selector degree.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Mathlib.LinearAlgebra.Matrix.BilinearForm
    2import Mathlib.Data.ZMod.Basic
    3import Mathlib.Algebra.Field.ZMod
    4import Mathlib.Data.Finset.Powerset
    5import Mathlib.Data.Fintype.Powerset
    6
    7/-!
    8---
    9title: Boolean point moments with restricted base coordinates
    10type: definition
    11---
    12The selector evaluations and the constant/base coordinates of §2.3.
    13Keeping the selector evaluation map as a parameter lets the coordinate
    14projection arguments apply at every selector degree.
    15-/
    16
    17namespace Lax342547.MomentSpace
    18
    19abbrev Binary := ZMod 2
    20
    21def SelectorCoordinates (b degree : ℕ) :=
    22 {S : Finset (Fin b) // S.card ≤ degree}
    23
    24instance (b degree : ℕ) : Fintype (SelectorCoordinates b degree) :=
    25 inferInstanceAs (Fintype {S : Finset (Fin b) // S.card ≤ degree})
    26
    27instance (b degree : ℕ) : DecidableEq (SelectorCoordinates b degree) :=
    28 inferInstanceAs (DecidableEq {S : Finset (Fin b) // S.card ≤ degree})
    29
    30def selectorEval {b degree : ℕ} (s : Fin b → Binary)
    31 (c : SelectorCoordinates b degree) : Binary := ∏ i ∈ c.val, s i
    32
    33variable {Label Coord Base : Type}
    34
    35def baseEval (z : Base → Binary) : Option Base → Binary
    36 | none => 1
    37 | some i => z i
    38
    39def point (p : Label → Coord → Binary) (s : Label) (z : Base → Binary)
    40 (i : Coord × Option Base) : Binary := p s i.1 * baseEval z i.2
    41
    42def pointMoment (p : Label → Coord → Binary) (s : Label) (z : Base → Binary) :
    43 Matrix (Coord × Option Base) (Coord × Option Base) Binary :=
    44 fun i j => point p s z i * point p s z j
    45
    46def momentSpace (p : Label → Coord → Binary) (A : Set Base) :
    47 Submodule Binary (Matrix (Coord × Option Base) (Coord × Option Base) Binary) :=
    48 Submodule.span Binary {w | ∃ s z, (∀ i, i ∉ A → z i = 0) ∧ w = pointMoment p s z}
    49
    50def allowed (A : Set Base) (i : Coord × Option Base) : Prop :=
    51 match i.2 with
    52 | none => True
    53 | some b => b ∈ A
    54
    55noncomputable def mask (A : Set Base) (i : Coord × Option Base) : Binary :=
    56 by classical exact if allowed A i then 1 else 0
    57
    58noncomputable def project (A : Set Base) :
    59 Matrix (Coord × Option Base) (Coord × Option Base) Binary →ₗ[Binary]
    60 Matrix (Coord × Option Base) (Coord × Option Base) Binary where
    61 toFun w i j := mask A i * w i j * mask A j
    62 map_add' w v := by
    63 ext i j
    64 change mask A i * (w i j + v i j) * mask A j =
    65 mask A i * w i j * mask A j + mask A i * v i j * mask A j
    66 simp [mul_add, add_mul]
    67 map_smul' c w := by
    68 ext i j
    69 change mask A i * (c * w i j) * mask A j = c * (mask A i * w i j * mask A j)
    70 simp [mul_assoc, mul_left_comm]
    71
    72noncomputable def eraseBase (A : Set Base) (z : Base → Binary) (i : Base) : Binary :=
    73 by classical exact if i ∈ A then z i else 0
    74
    75end Lax342547.MomentSpace
    76
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…