Lax Lean Archive

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

Concrete cut-space testers and the ordered mixer form

Lax342547.ConcreteCut · concepts/Lax342547/ConcreteCut.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 profile space is the image of the restricted cut map. The tester functionals descend from actual allowed moment representatives. The mixer sum retains the ordered component indices e,f in equation (2.9).

    Concept map
    8 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 exists_testers proven

    2 gradient_properties proven

    Lean source view on GitHub

    1import Lax342547.ConcreteGeometry
    2import Lax342547.RawFrames
    3
    4/-!
    5---
    6title: Concrete cut-space testers and the ordered mixer form
    7type: lemma
    8---
    9The profile space is the image of the restricted cut map. The tester
    10functionals descend from actual allowed moment representatives. The
    11mixer sum retains the ordered component indices e,f in equation (2.9).
    12-/
    13
    14namespace Lax342547.ConcreteCut
    15
    16open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    17open Lax342547.CutProfiles
    18
    19noncomputable instance (k : ℕ) : Fintype (Component (Tag k)) := by
    20 classical
    21 exact inferInstanceAs (Fintype {e : Finset (Tag k) // e.card = 2})
    22
    23noncomputable instance (k : ℕ) : DecidableEq (Component (Tag k)) := Classical.decEq _
    24
    25def tagSpace (k n b degree : ℕ) (l : Tag k) : Submodule Binary (Moment k n b degree) :=
    26 momentSpace selectorEval (allowedBase k n l)
    27
    28abbrev Representation (k n b degree : ℕ) := representatives (tagSpace k n b degree)
    29
    30def representationCut (k n b degree : ℕ) :
    31 Representation k n b degree →ₗ[Binary] (Component (Tag k) → Moment k n b degree) :=
    32 cutMap.comp (representatives (tagSpace k n b degree)).subtype
    33
    34abbrev Profile (k n b degree : ℕ) := LinearMap.range (representationCut k n b degree)
    35
    36def representativeAt {k n b degree : ℕ} (l : Tag k) :
    37 Representation k n b degree →ₗ[Binary] Moment k n b degree :=
    38 (LinearMap.proj l).comp (representatives (tagSpace k n b degree)).subtype
    39
    40def ordinarySum {k n b degree r : ℕ} (hr : 2 * r ≤ n) (t : Tag k) :
    41 Representation k n b degree →ₗ[Binary] Binary :=
    42 ∑ l : Tag k, ∑ d : Tag k, (blockTester hr (ordinary d t)).comp (representativeAt l)
    43
    44noncomputable def sharedSum {k n b degree r : ℕ} (hr : 2 * r ≤ n) (t : Tag k) :
    45 Representation k n b degree →ₗ[Binary] Binary := by
    46 classical
    47 exact ∑ l ∈ Finset.univ.erase t, (blockTester hr shared).comp (representativeAt l)
    48
    49/-- Unlike a and b, this quantity belongs to a specified representation. -/
    50def chiStar {k n b degree r : ℕ} (hr : 2 * r ≤ n) :
    51 Representation k n b degree →ₗ[Binary] Binary :=
    52 ∑ l : Tag k, (eta hr).comp (representativeAt l)
    53
    54structure Testers {k n b degree r : ℕ} (hr : 2 * r ≤ n) where
    55 aTag : Tag k → Profile k n b degree →ₗ[Binary] Binary
    56 bTag : Tag k → Profile k n b degree →ₗ[Binary] Binary
    57 ordinary_formula : ∀ t w, aTag t ((representationCut k n b degree).rangeRestrict w) = ordinarySum hr t w
    58 shared_formula : ∀ t w, bTag t ((representationCut k n b degree).rangeRestrict w) = sharedSum hr t w
    59
    60def Testers.role {k n b degree r : ℕ} {hr : 2 * r ≤ n} (D : Testers (k := k) (b := b) (degree := degree) hr) :
    61 Profile k n b degree →ₗ[Binary] Binary := ∑ t, D.aTag t
    62
    63def profileAt {k n b degree : ℕ} (e : Component (Tag k)) :
    64 Profile k n b degree →ₗ[Binary] Moment k n b degree :=
    65 (LinearMap.proj e).comp (LinearMap.range (representationCut k n b degree)).subtype
    66
    67def matrixPairing {I : Type} [Fintype I] : LinearMap.BilinForm Binary (Matrix I I Binary) where
    68 toFun := matrixPair
    69 map_add' x y := by
    70 ext w
    71 simp [matrixPair, Matrix.add_apply, add_smul, Finset.sum_add_distrib, LinearMap.sum_apply]
    72 map_smul' a x := by
    73 ext w
    74 simp [matrixPair, Matrix.smul_apply, mul_smul, Finset.smul_sum, LinearMap.sum_apply]
    75
    76noncomputable def mixingForm {k n b degree J : ℕ}
    77 (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) :
    78 LinearMap.BilinForm Binary (Profile k n b degree) :=
    79 ∑ j, ∑ e, ∑ f, matrixPairing.comp (profileAt e)
    80 ((RawFrames.sandwich (L j e f) (R j e f)).comp (profileAt f))
    81
    82noncomputable def gradient {k n b degree r J : ℕ} {hr : 2 * r ≤ n}
    83 (D : Testers (k := k) (b := b) (degree := degree) hr)
    84 (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) :
    85 LinearMap.BilinForm Binary (Profile k n b degree) :=
    86 GradientForm.form D.role D.aTag D.bTag (mixingForm L R)
    87
    88axiom exists_testers {k n b degree r : ℕ} (hr : 2 * r ≤ n) :
    89 Nonempty (Testers (k := k) (b := b) (degree := degree) hr)
    90
    91axiom gradient_properties {k n b degree r J : ℕ} {hr : 2 * r ≤ n}
    92 (D : Testers (k := k) (b := b) (degree := degree) hr)
    93 (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) :
    94 (∀ x y, gradient D L R x y = gradient D L R y x) ∧
    95 ∀ x, gradient D L R x x = D.role x
    96
    97end Lax342547.ConcreteCut
    98
    Show 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…