Lax Lean Archive

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

Actual finite atom parameterization and degrees

Lax342547.AtomParameters · concepts/Lax342547/AtomParameters.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

    Every flavor is parameterized by its retained binary coordinates; generic parameters cover all allowed base points, and actual atom/base/selector degrees are checked.

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

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

    1 atom_selector_degree proven

    2 generic_parameters_cover proven

    3 parameter_atom_degree proven

    4 parameter_coordinate_degree proven

    5 parameter_tensor_degree proven

    Lean source view on GitHub

    1import Lax342547.AtomFunctionals
    2import Lax342547.PolynomialTensors
    3
    4/-!
    5---
    6title: Actual finite atom parameterization and degrees
    7type: lemma
    8---
    9Every flavor is parameterized by its retained binary coordinates; generic parameters cover all allowed base points, and actual atom/base/selector degrees are checked.
    10-/
    11
    12namespace Lax342547.AtomParameters
    13
    14open Lax342547.MomentSpace Lax342547.Atoms Lax342547.TagGeometry Lax342547.ConcreteCut
    15open Lax342547.ConcreteGeometry Lax342547.SelectorInterpolation
    16
    17noncomputable def ParameterSize {k : ℕ} (n : ℕ) (l : Tag k) (f : Flavor k) :=
    18 Fintype.card {i : Base k n // i ∈ retained l f}
    19
    20noncomputable def parameterBase {k n : ℕ} (l : Tag k) (f : Flavor k)
    21 (x : Fin (ParameterSize n l f) → Binary) (i : Base k n) : Binary := by
    22 classical
    23 exact if hi : i ∈ retained l f then x ((Fintype.equivFin _).toFun ⟨i,hi⟩) else 0
    24
    25noncomputable def parameterAtom {k n b degree : ℕ} (l : Tag k) (s : Fin b → Binary) (f : Flavor k)
    26 (x : Fin (ParameterSize n l f) → Binary) : Profile k n b degree :=
    27 atom l s (parameterBase l f x) (by
    28 classical
    29 intro i hi
    30 have hn : i ∉ retained l f := by
    31 rintro hf
    32 apply hi
    33 cases i with
    34 | inl j => exact hf.1
    35 | inr j => trivial
    36 simp [parameterBase,hn])
    37
    38axiom parameter_coordinate_degree {k n : ℕ} (l : Tag k) (f : Flavor k) (i : Base k n) :
    39 (fun x => parameterBase l f x i) ∈ selectorSpan (ParameterSize n l f) 1
    40
    41axiom generic_parameters_cover {k n : ℕ} (l : Tag k) (z : Base k n → Binary)
    42 (hz : ∀ i,i ∉ allowedBase k n l → z i = 0) :
    43 ∃ x : Fin (ParameterSize n l Flavor.generic) → Binary,parameterBase l Flavor.generic x = z
    44
    45axiom parameter_atom_degree {k n b degree : ℕ} (l : Tag k) (s : Fin b → Binary) (f : Flavor k)
    46 (φ : Module.Dual Binary (Profile k n b degree)) :
    47 (fun x => φ (parameterAtom (degree := degree) l s f x)) ∈ selectorSpan (ParameterSize n l f) 2
    48
    49axiom atom_selector_degree {k n b degree : ℕ} (l : Tag k) (φ : Module.Dual Binary (Profile k n b degree))
    50 (z : Base k n → Binary) (hz : ∀ i,i ∉ allowedBase k n l → z i = 0) :
    51 (fun s => φ (atom (degree := degree) l s z hz)) ∈ selectorSpan b (degree+degree)
    52
    53axiom parameter_tensor_degree {k n b degree : ℕ} (l : Tag k) (s : Fin b → Binary) (f : Flavor k)
    54 (ψ : Module.Dual Binary (Moment k n b degree)) :
    55 (fun x => ψ (pointMoment selectorEval s (parameterBase l f x))) ∈ selectorSpan (ParameterSize n l f) 2
    56
    57end Lax342547.AtomParameters
    58
    Show 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…