Lax Lean Archive

Convergence under polynomial residuals

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

    If gg satisfies (C), so do g∘Qg\circ Q and its centered series g∘Q−(g,Q)g\circ Q-(g,Q) for every noncommutative polynomial QQ. In particular the normalized observation coordinates used in part b) and all their letter residuals satisfy (C).

    Concept map
    5 concepts; 3 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 centered_residual proven

    2 right_residual proven

    In the paper

    • page 9 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.ConvergenceHypothesis
    2
    3/-!
    4---
    5title: Convergence under polynomial residuals
    6type: theorem
    7---
    8If gg satisfies (C), so do g∘Qg\circ Q and its centered series
    9g∘Q−(g,Q)g\circ Q-(g,Q) for every noncommutative polynomial QQ.
    10In particular the normalized observation coordinates used in part b)
    11and all their letter residuals satisfy (C).
    12-/
    13
    14noncomputable section
    15
    16namespace Lax825748.ResidualConvergence
    17
    18open Lax825748.Series ConvergenceHypothesis
    19
    20axiom right_residual {X : Type} (g : NCSeries X) (hg : Holds g)
    21 (Q : NCPolynomial X) :
    22 Holds (rightResidual g Q)
    23
    24axiom centered_residual {X : Type} (g : NCSeries X) (hg : Holds g)
    25 (Q : NCPolynomial X) :
    26 Holds (rightResidual g Q - constantSeries (pairing g Q))
    27
    28end Lax825748.ResidualConvergence
    29
    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…