Lax Lean Archive

Calculus of convergent power series

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

    The geometric coefficient bound is equivalent to absolute summability at some positive polyradius. Convergent series form a real subalgebra and are closed under partial differentiation.

    A formally continuous algebra homomorphism sending each variable to a convergent series with zero constant term preserves convergence. This is composition of convergent power series at the origin.

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

    2 composition proven

    3 partial_derivative proven

    4 subalgebra proven

    Lean source view on GitHub

    1import Lax825748.ConvergentSeries
    2import Mathlib.Analysis.SpecificLimits.Normed
    3import Mathlib.Algebra.Algebra.Subalgebra.Basic
    4
    5/-!
    6---
    7title: Calculus of convergent power series
    8type: theorem
    9---
    10The geometric coefficient bound is equivalent to absolute summability at
    11some positive polyradius. Convergent series form a real subalgebra and are
    12closed under partial differentiation.
    13
    14A formally continuous algebra homomorphism sending each variable to a
    15convergent series with zero constant term preserves convergence. This is
    16composition of convergent power series at the origin.
    17-/
    18
    19noncomputable section
    20
    21namespace Lax825748.AnalyticCalculus
    22
    23open Lax825748.FormalSeries Lax825748.Monomials ConvergentSeries
    24
    25axiom absolute_convergence {d : ℕ} (f : StateSeries d) :
    26 Convergent f ↔ ∃ r : ℝ, 0 < r ∧
    27 Summable (fun I : Fin d →₀ ℕ => |MvPowerSeries.coeff I f| * r ^ totalDegree I)
    28
    29axiom subalgebra (d : ℕ) :
    30 ∃ A : Subalgebra ℝ (StateSeries d), ∀ f, f ∈ A ↔ Convergent f
    31
    32axiom partial_derivative {d : ℕ} (f : StateSeries d) (hf : Convergent f)
    33 (i : Fin d) :
    34 Convergent (MvPowerSeries.pderiv ℝ i f)
    35
    36axiom composition {d e : ℕ} (φ : StateSeries d →ₐ[ℝ] StateSeries e)
    37 (hc : FormallyContinuous φ)
    38 (h0 : ∀ i, MvPowerSeries.constantCoeff (φ (MvPowerSeries.X i)) = 0)
    39 (hφ : ∀ i, Convergent (φ (MvPowerSeries.X i)))
    40 (f : StateSeries d) (hf : Convergent f) :
    41 Convergent (φ f)
    42
    43end Lax825748.AnalyticCalculus
    44
    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…