Documentation

LeanPool.LocalComplexGeometry.Germs.Representatives

Canonical chosen analytic representatives #

Abstract germs cannot be evaluated away from the origin. For finite specialization arguments it is convenient to choose one analytic representative for each germ and retain the theorem identifying its raw function germ.

source
noncomputable def LocalComplexGeometry.HolomorphicGerm.representative {n : ℕ} (f : ↥(HolomorphicGerm n)) :
ComplexEuclidean n → ℂ

A chosen analytic representative of a holomorphic germ.

Equations
Instances For
    source
    theorem LocalComplexGeometry.HolomorphicGerm.analyticAt_representative {n : ℕ} (f : ↥(HolomorphicGerm n)) :
    AnalyticAt ℂ (representative f) 0

    The chosen representative is analytic at the origin.

    source
    theorem LocalComplexGeometry.HolomorphicGerm.coe_representative {n : ℕ} (f : ↥(HolomorphicGerm n)) :
    ↑(representative f) = ↑f

    The chosen representative represents the original germ.

    source
    noncomputable def LocalComplexGeometry.HolomorphicGerm.coefficientRepresentatives {n k : ℕ} (c : Fin k → ↥(HolomorphicGerm n)) :
    Fin k → ComplexEuclidean n → ℂ

    Chosen representatives of a finite coefficient vector.

    Equations
    Instances For
      source
      theorem LocalComplexGeometry.HolomorphicGerm.analyticAt_coefficientRepresentatives {n k : ℕ} (c : Fin k → ↥(HolomorphicGerm n)) (i : Fin k) :
      AnalyticAt ℂ (coefficientRepresentatives c i) 0
      source
      theorem LocalComplexGeometry.HolomorphicGerm.coe_coefficientRepresentatives {n k : ℕ} (c : Fin k → ↥(HolomorphicGerm n)) (i : Fin k) :
      ↑(coefficientRepresentatives c i) = ↑(c i)