Lax Lean Archive

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

Actual point atoms determine cut-space functionals

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

    Ambient extension realizes every atom evaluation as a local tensor functional, with actual base degree two and point-atom extensionality on the whole concrete cut space.

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

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

    1 atom_base_degree proven

    2 atom_functional_ext proven

    3 atom_local_functional proven

    4 cut_star_sum proven

    Lean source view on GitHub

    1import Lax342547.CommonAtoms
    2import Lax342547.PointQuadratics
    3import Mathlib.LinearAlgebra.Dual.Lemmas
    4
    5/-!
    6---
    7title: Actual point atoms determine cut-space functionals
    8type: lemma
    9---
    10Ambient extension realizes every atom evaluation as a local tensor functional, with actual base degree two and point-atom extensionality on the whole concrete cut space.
    11-/
    12
    13namespace Lax342547.AtomFunctionals
    14
    15open Lax342547.MomentSpace Lax342547.Atoms Lax342547.TagGeometry Lax342547.ConcreteCut
    16open Lax342547.ConcreteGeometry Lax342547.CutProfiles Lax342547.SelectorInterpolation
    17open scoped BigOperators
    18
    19noncomputable def starMatrixMap {k n b degree : ℕ} (l : Tag k) :
    20 Moment k n b degree →ₗ[Binary] (Component (Tag k) → Moment k n b degree) := by
    21 classical
    22 exact { toFun := fun M e => if l ∈ e.val then M else 0
    23 map_add' := by intro x y; funext e; by_cases h : l ∈ e.val <;> simp [h]
    24 map_smul' := by intro c x; funext e; by_cases h : l ∈ e.val <;> simp [h] }
    25
    26axiom atom_local_functional {k n b degree : ℕ} (l : Tag k)
    27 (φ : Module.Dual Binary (Profile k n b degree)) :
    28 ∃ ψ : Module.Dual Binary (Moment k n b degree),∀ s z
    29 (hz : ∀ i,i ∉ allowedBase k n l → z i = 0),
    30 φ (atom (degree := degree) l s z hz) = ψ (pointMoment selectorEval s z)
    31
    32axiom cut_star_sum {k n b degree : ℕ} (w : Tag k → Moment k n b degree) :
    33 cutMap w = ∑ l,starMatrixMap l (w l)
    34
    35axiom atom_functional_ext {k n b degree : ℕ} (φ : Module.Dual Binary (Profile k n b degree))
    36 (hφ : ∀ l s z (hz : ∀ i,i ∉ allowedBase k n l → z i = 0),
    37 φ (atom (degree := degree) l s z hz) = 0) : φ = 0
    38
    39axiom atom_base_degree {k n b degree r : ℕ} (l : Tag k) (s : Fin b → Binary)
    40 (φ : Module.Dual Binary (Profile k n b degree))
    41 (z : (Fin r → Binary) → Base k n → Binary)
    42 (hz : ∀ x i,i ∉ allowedBase k n l → z x i = 0)
    43 (hdegree : ∀ i,(fun x => z x i) ∈ selectorSpan r 1) :
    44 (fun x => φ (atom (degree := degree) l s (z x) (hz x))) ∈ selectorSpan r 2
    45
    46end Lax342547.AtomFunctionals
    47
    Show ProofShow 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…