Lax Lean Archive

Lie rank is the least analytic realization dimension

Lax825748.Minimality · concepts/Lax825748/Minimality.lean · lax-825748

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

    Theorem

    A series has Lie rank dd and satisfies (C) if and only if dd is the least dimension of its analytic differential representations. The least dimension is attained. Constant series are included with dimension zero.

    Concept map
    24 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.Realization
    2
    3/-!
    4---
    5title: Lie rank is the least analytic realization dimension
    6type: theorem
    7---
    8A series has Lie rank dd and satisfies (C) if and only if dd is the
    9least dimension of its analytic differential representations. The least
    10dimension is attained. Constant series are included with dimension zero.
    11-/
    12
    13noncomputable section
    14
    15namespace Lax825748.Minimality
    16
    17open Lax825748.Series Lax825748.LieRank Lax825748.DifferentialRepresentation
    18open AnalyticRepresentations
    19
    20def IsLeastDimension {X : Type} (g : NCSeries X) (d : ℕ) : Prop :=
    21 (∃ R : Representation X d, IsAnalytic R ∧ Represents R g) ∧
    22 ∀ e, (∃ R : Representation X e, IsAnalytic R ∧ Represents R g) → d ≤ e
    23
    24axiom least_dimension {X : Type} [Finite X] (g : NCSeries X) (d : ℕ) :
    25 (HasLieRank g d ∧ ConvergenceHypothesis.Holds g) ↔ IsLeastDimension g d
    26
    27end Lax825748.Minimality
    28
    Show 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…