Analytic quotient and remainder coefficient sequences

This file feeds the normalized moving coefficient sequence into the \ell^1(\mathbb N) division theorem. The resulting quotient and remainder depend analytically on the base variables. At the base origin, exact order forces the remainder to vanish and the quotient to have constant coefficient one.

@[irreducible]

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

The small perturbation of the normalized distinguished monomial.

Equations

• ClassicalComplexWPT.normalizedPreparationTail p r hr d z = ClassicalComplexWPT.analyticNormalizedCoefficientMap p r hr d z - ClassicalComplexWPT.monomialSeq d

theorem ClassicalComplexWPT.normalizedPreparationTail_def {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (z : Base n) : normalizedPreparationTail p r hr d z = analyticNormalizedCoefficientMap p r hr d z - monomialSeq d

theorem ClassicalComplexWPT.normalizedPreparationQuotient_def {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (z : Base n) : normalizedPreparationQuotient p r hr d z = seqDivisionQuotientGlobal d (normalizedPreparationTail p r hr d z, monomialSeq d)

@[irreducible]

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

The quotient produced by dividing the degree-d monomial by the normalized moving coefficient sequence.

Equations

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

@[irreducible]

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

The low-degree remainder produced by the same division.

Equations

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

theorem ClassicalComplexWPT.normalizedPreparationRemainder_def {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (z : Base n) : normalizedPreparationRemainder p r hr d z = seqDivisionRemainderGlobal d (normalizedPreparationTail p r hr d z, monomialSeq d)

theorem ClassicalComplexWPT.analyticAt_normalizedPreparationTail {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) : AnalyticAt ℂ (normalizedPreparationTail p r hr d) 0

theorem ClassicalComplexWPT.analyticAt_normalizedPreparationQuotient {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (hsmall : ‖normalizedPreparationTail p r hr d 0‖ < 1) : AnalyticAt ℂ (normalizedPreparationQuotient p r hr d) 0

theorem ClassicalComplexWPT.analyticAt_normalizedPreparationRemainder {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) (hsmall : ‖normalizedPreparationTail p r hr d 0‖ < 1) : AnalyticAt ℂ (normalizedPreparationRemainder p r hr d) 0

theorem ClassicalComplexWPT.convolution_monomialSeq (q : ↥OriginSeq) (d : ℕ) : convolution q (monomialSeq d) = seqLowShift d q

Convolution with the degree-d monomial inserts d leading zero coefficients.

theorem ClassicalComplexWPT.convolution_apply_eq_zero_of_right {q p : ↥OriginSeq} {n : ℕ} (hp : ∀ k ≤ n, ↑p k = 0) : ↑(convolution q p) n = 0

theorem ClassicalComplexWPT.normalizedPreparationTail_zero_of_le {n d : ℕ} {f : Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (hp : HasFPowerSeriesAt f p 0) (horder : ExactOrderInLastVariable f d) (r : NNReal) (hr0 : 0 < r) (hr : ↑r < p.radius) {k : ℕ} (hk : k ≤ d) : ↑(normalizedPreparationTail p r hr d 0) k = 0

theorem ClassicalComplexWPT.eventually_normalizedPreparation_factorization {n d : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (hclose : ‖analyticNormalizedCoefficientMap p r hr d 0 - monomialSeq d‖ < 1 / 2) : ∀ᶠ (z : Base n) in nhds 0, monomialSeq d = convolution (normalizedPreparationQuotient p r hr d z) (analyticNormalizedCoefficientMap p r hr d z) + normalizedPreparationRemainder p r hr d z ∧ seqHighShift d (normalizedPreparationRemainder p r hr d z) = 0

theorem ClassicalComplexWPT.normalizedPreparationRemainder_zero {n d : ℕ} {f : Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (hp : HasFPowerSeriesAt f p 0) (horder : ExactOrderInLastVariable f d) (r : NNReal) (hr0 : 0 < r) (hr : ↑r < p.radius) (hsmall : ‖normalizedPreparationTail p r hr d 0‖ < 1) : normalizedPreparationRemainder p r hr d 0 = 0

theorem ClassicalComplexWPT.normalizedPreparationQuotient_zero_apply_zero {n d : ℕ} {f : Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (hp : HasFPowerSeriesAt f p 0) (horder : ExactOrderInLastVariable f d) (r : NNReal) (hr0 : 0 < r) (hr : ↑r < p.radius) (hsmall : ‖normalizedPreparationTail p r hr d 0‖ < 1) : ↑(normalizedPreparationQuotient p r hr d 0) 0 = 1

theorem ClassicalComplexWPT.exists_normalizedPreparationSequences {n d : ℕ} {f : Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (hp : HasFPowerSeriesAt f p 0) (horder : ExactOrderInLastVariable f d) : ∃ (r : NNReal) (hr : ↑r < p.radius), 0 < r ∧ ↑(originWeightedCoeffs p r hr) d ≠ 0 ∧ AnalyticAt ℂ (normalizedPreparationQuotient p r hr d) 0 ∧ AnalyticAt ℂ (normalizedPreparationRemainder p r hr d) 0 ∧ (∀ᶠ (z : Base n) in nhds 0, monomialSeq d = convolution (normalizedPreparationQuotient p r hr d z) (analyticNormalizedCoefficientMap p r hr d z) + normalizedPreparationRemainder p r hr d z ∧ seqHighShift d (normalizedPreparationRemainder p r hr d z) = 0) ∧ normalizedPreparationRemainder p r hr d 0 = 0 ∧ ↑(normalizedPreparationQuotient p r hr d 0) 0 = 1

Exact order yields a radius and analytic quotient/remainder coefficient maps with the preparation factorization, vanishing origin remainder, and unit-normalized origin quotient.