OAI/Analysis/Kaplansky/Polynomials.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.algebraStarLetter line 15
2. def OAI.Kaplansky.algebraStarWord line 18
3. theorem OAI.Kaplansky.algebraStarWord_append line 21
4. def OAI.Kaplansky.starWordMonoid line 25
5. theorem OAI.Kaplansky.starWordMonoid_eq_closure line 32
6. theorem OAI.Kaplansky.starAdjoin_eq_wordSpan line 56
7. abbrev OAI.Kaplansky.StarWordPolynomial line 62
8. def OAI.Kaplansky.evalStarWordPolynomial line 64
9. theorem OAI.Kaplansky.starAdjoin_exists_wordPolynomial line 69

   Source documentation

   Every element of the actual algebraic star-adjoin is a finite sum of explicit generator/adjoint words; this includes scalar constants.

   theorem starAdjoin_exists_wordPolynomial (x : Fin N → A) {z : A}
       (hz : z ∈ StarAlgebra.adjoin ℂ (Set.range x)) :
       ∃ p : StarWordPolynomial N, evalStarWordPolynomial x p=z := by
   …

   Mentions: OAI.Kaplansky.StarWordPolynomial, OAI.Kaplansky.evalStarWordPolynomial

10. theorem OAI.Kaplansky.generated_exists_wordPolynomial line 78

    Source documentation

    Norm approximation in the actual closed generated algebra by a finite star polynomial. No density hypothesis is supplied by the caller.

    theorem generated_exists_wordPolynomial (x : Fin N → A) (z : generatedAlgebra (Set.range x))
        {ε : ℝ} (hε : 0<ε) :
        ∃ p : StarWordPolynomial N, ‖evalStarWordPolynomial x p - (z : A)‖ < ε := by
    …

    Mentions: OAI.Kaplansky.generatedAlgebra, OAI.Kaplansky.StarWordPolynomial, OAI.Kaplansky.evalStarWordPolynomial

11. theorem OAI.Kaplansky.evalStarWordPolynomial_mem line 96
12. def OAI.Kaplansky.generatedWordPolynomial line 102
13. theorem OAI.Kaplansky.generatedWordPolynomial_dense line 106
14. theorem OAI.Kaplansky.generated_matrix_polynomial_approximation line 117

    Source documentation

    Arbitrary rectangular matrices over the actual generated algebra have finite star-polynomial approximants in their C*-matrix operator norm.

    theorem generated_matrix_polynomial_approximation (x : Fin N → A)
        {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
        (W : CStarMatrix m n (generatedAlgebra (Set.range x))) {ε : ℝ} (hε : 0<ε) :
        ∃ p : m → n → StarWordPolynomial N,
          ‖CStarMatrix.ofMatrix (fun i j => generatedWordPolynomial x (p i j)) - W‖ < ε := by
    …

    Mentions: OAI.Kaplansky.generatedAlgebra, OAI.Kaplansky.StarWordPolynomial, OAI.Kaplansky.generatedWordPolynomial