Lax Lean Archive

The convergence hypothesis on Lie polynomials

Lax825748.ConvergenceHypothesis · concepts/Lax825748/ConvergenceHypothesis.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

    Definition

    Condition (C) requires that, for every finite ordered family of Lie polynomials P1,…,PqP_1,\ldots,P_q, there are α,C>0\alpha,C>0 such that

    ∣(g,P1i1⋯Pqiq)∣≤αC∣I∣I!.|(g,P_1^{i_1}\cdots P_q^{i_q})|\leq\alpha C^{|I|}I!.

    The constants may depend on the family, but not on the exponents.

    The inequalities I!≤∣I∣!≤q∣I∣I!I!\leq |I|!\leq q^{|I|}I! show that replacing I!I! by ∣I∣!|I|! gives the same condition. Empty families are allowed.

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

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

    1 factorial_comparison proven

    2 total_factorial_iff proven

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.LieRank
    2import Lax825748.Monomials
    3
    4/-!
    5---
    6title: The convergence hypothesis on Lie polynomials
    7type: definition
    8---
    9Condition (C) requires that, for every finite ordered family of Lie
    10polynomials P1,…,PqP_1,\ldots,P_q, there are α,C>0\alpha,C>0 such that
    11∣(g,P1i1⋯Pqiq)∣≤αC∣I∣I!.|(g,P_1^{i_1}\cdots P_q^{i_q})|\leq\alpha C^{|I|}I!.
    12The constants may depend on the family, but not on the exponents.
    13
    14The inequalities I!≤∣I∣!≤q∣I∣I!I!\leq |I|!\leq q^{|I|}I! show that replacing I!I!
    15by ∣I∣!|I|! gives the same condition. Empty families are allowed.
    16-/
    17
    18noncomputable section
    19
    20namespace Lax825748.ConvergenceHypothesis
    21
    22open Lax825748.Series Lax825748.LieRank Lax825748.Monomials
    23
    24def Holds {X : Type} (g : NCSeries X) : Prop :=
    25 ∀ (q : ℕ) (P : Fin q → LiePolynomial X),
    26 ∃ α : ℝ, 0 < α ∧ ∃ C : ℝ, 0 < C ∧
    27 ∀ I : Fin q → ℕ,
    28 |pairing g (orderedPowers (fun j => (P j).val) I)| ≤
    29 α * C ^ totalDegree I * (multiFactorial I : ℝ)
    30
    31def HoldsWithTotalFactorial {X : Type} (g : NCSeries X) : Prop :=
    32 ∀ (q : ℕ) (P : Fin q → LiePolynomial X),
    33 ∃ α : ℝ, 0 < α ∧ ∃ C : ℝ, 0 < C ∧
    34 ∀ I : Fin q → ℕ,
    35 |pairing g (orderedPowers (fun j => (P j).val) I)| ≤
    36 α * C ^ totalDegree I * ((totalDegree I).factorial : ℝ)
    37
    38axiom factorial_comparison {q : ℕ} (I : Fin q → ℕ) :
    39 multiFactorial I ≤ (totalDegree I).factorial ∧
    40 (totalDegree I).factorial ≤ q ^ totalDegree I * multiFactorial I
    41
    42axiom total_factorial_iff {X : Type} (g : NCSeries X) :
    43 Holds g ↔ HoldsWithTotalFactorial g
    44
    45end Lax825748.ConvergenceHypothesis
    46
    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…