Public existence from analytic sequence preparation

This file reconstructs the public analytic unit and distinguished polynomial from the normalized ℓ¹(ℕ) quotient/remainder supplied by PreparationSequences.

@[simp]

theorem ClassicalComplexWPT.evalL1PowerSeries_zero (a : ↥L1Sequence) : evalL1PowerSeries a 0 = ↑a 0

theorem ClassicalComplexWPT.evalL1PowerSeries_add (a b : ↥L1Sequence) (w : ℂ) : evalL1PowerSeries (a + b) w = evalL1PowerSeries a w + evalL1PowerSeries b w

theorem ClassicalComplexWPT.weighted_scaled_pow (r : ℂ) (hr : r ≠ 0) {d i : ℕ} (hi : i ≤ d) (w : ℂ) : r ^ (d - i) * w ^ i = r ^ d * (r⁻¹ * w) ^ i

noncomputable def ClassicalComplexWPT.preparationCoefficient {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (i : Fin d) : Base n → ℂ

Lower coefficients of the reconstructed distinguished polynomial.

Equations

• ClassicalComplexWPT.preparationCoefficient p r hr d i z = -↑↑r ^ (d - ↑i) * ↑(ClassicalComplexWPT.normalizedPreparationRemainder p r hr d z) ↑i

noncomputable def ClassicalComplexWPT.preparationQuotientEval {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) : Ambient n → ℂ

Evaluation of the normalized division quotient in the original distinguished variable.

Equations

• ClassicalComplexWPT.preparationQuotientEval p r hr d x = ClassicalComplexWPT.evalL1PowerSeries (ClassicalComplexWPT.normalizedPreparationQuotient p r hr d x.1) ((↑↑r)⁻¹ * x.2)

noncomputable def ClassicalComplexWPT.preparationUnit {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) : Ambient n → ℂ

The reconstructed analytic unit.

Equations

• ClassicalComplexWPT.preparationUnit p r hr d x = ↑(ClassicalComplexWPT.originWeightedCoeffs p r hr) d * (↑↑r)⁻¹ ^ d * (ClassicalComplexWPT.preparationQuotientEval p r hr d x)⁻¹

theorem ClassicalComplexWPT.analyticAt_preparationCoefficient {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (hq : AnalyticAt ℂ (normalizedPreparationRemainder p r hr d) 0) (i : Fin d) : AnalyticAt ℂ (preparationCoefficient p r hr d i) 0

theorem ClassicalComplexWPT.preparationCoefficient_zero {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (hrem : normalizedPreparationRemainder p r hr d 0 = 0) (i : Fin d) : preparationCoefficient p r hr d i 0 = 0

theorem ClassicalComplexWPT.preparedPolynomial_preparationCoefficient {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (hr0 : 0 < r) (z : Base n) (w : ℂ) : preparedPolynomial d (preparationCoefficient p r hr d) (z, w) = ↑↑r ^ d * ((↑↑r)⁻¹ ^ d * w ^ d - ∑ i : Fin d, ↑(normalizedPreparationRemainder p r hr d z) ↑i * ((↑↑r)⁻¹ * w) ^ ↑i)

theorem ClassicalComplexWPT.analyticAt_preparationQuotientEval {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (hq : AnalyticAt ℂ (normalizedPreparationQuotient p r hr d) 0) : AnalyticAt ℂ (preparationQuotientEval p r hr d) 0

theorem ClassicalComplexWPT.preparationQuotientEval_zero {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) : preparationQuotientEval p r hr d 0 = ↑(normalizedPreparationQuotient p r hr d 0) 0

theorem ClassicalComplexWPT.analyticAt_preparationUnit {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (hq : AnalyticAt ℂ (normalizedPreparationQuotient p r hr d) 0) (hq0 : ↑(normalizedPreparationQuotient p r hr d 0) 0 = 1) : AnalyticAt ℂ (preparationUnit p r hr d) 0

theorem ClassicalComplexWPT.preparationUnit_zero_ne {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (hr0 : 0 < r) (htop : ↑(originWeightedCoeffs p r hr) d ≠ 0) (hq0 : ↑(normalizedPreparationQuotient p r hr d 0) 0 = 1) : preparationUnit p r hr d 0 ≠ 0

theorem ClassicalComplexWPT.preparation_factorization_of_sequence_factorization {n d : ℕ} {f : Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (hr0 : 0 < r) (htop : ↑(originWeightedCoeffs p r hr) d ≠ 0) (z : Base n) (w : ℂ) (hfac : monomialSeq d = convolution (normalizedPreparationQuotient p r hr d z) (analyticNormalizedCoefficientMap p r hr d z) + normalizedPreparationRemainder p r hr d z) (hsupp : seqHighShift d (normalizedPreparationRemainder p r hr d z) = 0) (hw : ‖(↑↑r)⁻¹ * w‖ < 1) (hrecon : evalL1PowerSeries ((weightedCoefficientSeries p r).sum z) ((↑↑r)⁻¹ * w) = f (z, w)) (hQne : preparationQuotientEval p r hr d (z, w) ≠ 0) : f (z, w) = preparationUnit p r hr d (z, w) * preparedPolynomial d (preparationCoefficient p r hr d) (z, w)

Pointwise reconstruction once sequence division and convergence are available. Keeping the convergence hypotheses explicit makes this lemma reusable for both the public existence and uniqueness arguments.

theorem ClassicalComplexWPT.exists_isWeierstrassPreparation {n d : ℕ} {f : Ambient n → ℂ} (hf : AnalyticAt ℂ f 0) (horder : ExactOrderInLastVariable f d) : ∃ (a : Fin d → Base n → ℂ) (u : Ambient n → ℂ), IsWeierstrassPreparation f d a u

The existence half of classical complex Weierstrass preparation, in the exact public predicate.