Basic definitions for classical complex Weierstrass preparation

This module will contain the ordinary finite-dimensional spaces and local analytic definitions used by the proof development. The independently audited public statement remains in Challenge.lean.

@[reducible, inline]

abbrev ClassicalComplexWPT.Base (n : ℕ) : Type

The complex parameter space ℂⁿ.

Equations

• ClassicalComplexWPT.Base n = (Fin n → ℂ)

@[reducible, inline]

abbrev ClassicalComplexWPT.Ambient (n : ℕ) : Type

The parameter space together with the distinguished complex variable.

Equations

• ClassicalComplexWPT.Ambient n = (ClassicalComplexWPT.Base n × ℂ)

theorem ClassicalComplexWPT.ambient_zero_eq (n : ℕ) : 0 = (0, 0)

The additive zero in the ambient product is the pair of coordinate zeros.

def ClassicalComplexWPT.lastSlice {n : ℕ} (f : Ambient n → ℂ) : ℂ → ℂ

Restriction of a function to the distinguished-variable axis.

Equations

• ClassicalComplexWPT.lastSlice f w = f (0, w)

@[simp]

theorem ClassicalComplexWPT.lastSlice_zero {n : ℕ} (f : Ambient n → ℂ) : lastSlice f 0 = f 0

def ClassicalComplexWPT.ExactOrderInLastVariable {n : ℕ} (f : Ambient n → ℂ) (d : ℕ) : Prop

The distinguished-variable slice has a zero of exact order d at the origin: all derivatives of order below d vanish and the derivative of order d does not vanish.

Equations

• ClassicalComplexWPT.ExactOrderInLastVariable f d = ((∀ k < d, iteratedDeriv k (ClassicalComplexWPT.lastSlice f) 0 = 0) ∧ iteratedDeriv d (ClassicalComplexWPT.lastSlice f) 0 ≠ 0)

def ClassicalComplexWPT.preparedPolynomial {n : ℕ} (d : ℕ) (a : Fin d → Base n → ℂ) (x : Ambient n) : ℂ

The monic degree-d polynomial in the distinguished variable.

Equations

• ClassicalComplexWPT.preparedPolynomial d a x = x.2 ^ d + ∑ i : Fin d, a i x.1 * x.2 ^ ↑i

def ClassicalComplexWPT.IsWeierstrassPreparation {n : ℕ} (f : Ambient n → ℂ) (d : ℕ) (a : Fin d → Base n → ℂ) (u : Ambient n → ℂ) : Prop

f is locally the product of a nonvanishing analytic unit and a monic distinguished-variable polynomial whose lower coefficients are analytic and vanish at the base origin.

Equations

• One or more equations did not get rendered due to their size.