Normalized weighted coefficient sequences

Exact order in the distinguished variable lets us choose a small positive weight so that the normalized coefficient sequence is strictly close to the degree-d monomial in the ordinary complex ℓ¹ norm. This is the Archimedean tail-scaling estimate needed by the Banach-algebra proof.

@[reducible, inline]

noncomputable abbrev ClassicalComplexWPT.OriginSeq : AddSubgroup (PreLp fun (x : ℕ) => ℂ)

Absolutely summable one-variable coefficient sequences at the origin.

Equations

• ClassicalComplexWPT.OriginSeq = ClassicalComplexWPT.L1Coeff ℕ

theorem ClassicalComplexWPT.norm_lastDirection_local (n : ℕ) : ‖lastDirection n‖ = 1

noncomputable def ClassicalComplexWPT.monomialSeq (d : ℕ) : ↥OriginSeq

The monomial coefficient vector supported at degree d.

Equations

• ClassicalComplexWPT.monomialSeq d = lp.single 1 d 1

@[simp]

theorem ClassicalComplexWPT.monomialSeq_apply_same (d : ℕ) : ↑(monomialSeq d) d = 1

@[simp]

theorem ClassicalComplexWPT.monomialSeq_apply_ne {d k : ℕ} (h : k ≠ d) : ↑(monomialSeq d) k = 0

noncomputable def ClassicalComplexWPT.scaleSeq (t : NNReal) (ht : t ≤ 1) (f : ↥OriginSeq) : ↥OriginSeq

Diagonal rescaling of an ℓ¹ sequence by powers of t ≤ 1.

Equations

• ClassicalComplexWPT.scaleSeq t ht f = ⟨fun (k : ℕ) => ↑↑t ^ k * ↑f k, ⋯⟩

@[simp]

theorem ClassicalComplexWPT.scaleSeq_apply (t : NNReal) (ht : t ≤ 1) (f : ↥OriginSeq) (k : ℕ) : ↑(scaleSeq t ht f) k = ↑↑t ^ k * ↑f k

noncomputable def ClassicalComplexWPT.normalizedScale (t : NNReal) (ht : t ≤ 1) (f : ↥OriginSeq) (d : ℕ) : ↥OriginSeq

Rescale a sequence and normalize its coefficient in degree d to one.

Equations

• ClassicalComplexWPT.normalizedScale t ht f d = (↑(ClassicalComplexWPT.scaleSeq t ht f) d)⁻¹ • ClassicalComplexWPT.scaleSeq t ht f

@[simp]

theorem ClassicalComplexWPT.normalizedScale_apply (t : NNReal) (ht : t ≤ 1) (f : ↥OriginSeq) (d k : ℕ) : ↑(normalizedScale t ht f d) k = (↑↑t ^ d * ↑f d)⁻¹ * (↑↑t ^ k * ↑f k)

theorem ClassicalComplexWPT.normalizedScale_sub_monomial_apply_lt {t : NNReal} (ht : t ≤ 1) (ht0 : 0 < t) (f : ↥OriginSeq) (d k : ℕ) (hlow : ∀ j < d, ↑f j = 0) (hfd : ↑f d ≠ 0) : ‖↑(normalizedScale t ht f d - monomialSeq d) k‖ ≤ ↑t / ‖↑f d‖ * ‖↑f k‖

theorem ClassicalComplexWPT.norm_normalizedScale_sub_monomial_le {t : NNReal} (ht : t ≤ 1) (ht0 : 0 < t) (f : ↥OriginSeq) (d : ℕ) (hlow : ∀ j < d, ↑f j = 0) (hfd : ↑f d ≠ 0) : ‖normalizedScale t ht f d - monomialSeq d‖ ≤ ↑t / ‖↑f d‖ * ‖f‖

theorem ClassicalComplexWPT.exists_scale_normalized_close_half (f : ↥OriginSeq) (d : ℕ) (hlow : ∀ j < d, ↑f j = 0) (hfd : ↑f d ≠ 0) : ∃ (t : NNReal) (ht : t ≤ 1), 0 < t ∧ t < 1 ∧ ‖normalizedScale t ht f d - monomialSeq d‖ < 1 / 2

noncomputable def ClassicalComplexWPT.originWeightedCoeffs {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (R : NNReal) (hR : ↑R < p.radius) : ↥OriginSeq

Distinguished-variable coefficients at the base origin, weighted by R^k.

Equations

• ClassicalComplexWPT.originWeightedCoeffs p R hR = ⟨fun (k : ℕ) => ↑↑R ^ k * ClassicalComplexWPT.lastTaylorCoefficient p k 0, ⋯⟩

@[simp]

theorem ClassicalComplexWPT.originWeightedCoeffs_apply {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (R : NNReal) (hR : ↑R < p.radius) (k : ℕ) : ↑(originWeightedCoeffs p R hR) k = ↑↑R ^ k * lastTaylorCoefficient p k 0

theorem ClassicalComplexWPT.originWeightedCoeffs_low_eq_zero {n d : ℕ} {f : Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (hp : HasFPowerSeriesAt f p 0) (horder : ExactOrderInLastVariable f d) (R : NNReal) (hR : ↑R < p.radius) {k : ℕ} (hk : k < d) : ↑(originWeightedCoeffs p R hR) k = 0

theorem ClassicalComplexWPT.originWeightedCoeffs_top_ne_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) : ↑(originWeightedCoeffs p R hR) d ≠ 0

theorem ClassicalComplexWPT.mul_radius_lt_of_le_one {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (R t : NNReal) (hR : ↑R < p.radius) (ht : t ≤ 1) : ↑(t * R) < p.radius

theorem ClassicalComplexWPT.scaleSeq_originWeightedCoeffs {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (R t : NNReal) (hR : ↑R < p.radius) (ht : t ≤ 1) : scaleSeq t ht (originWeightedCoeffs p R hR) = originWeightedCoeffs p (t * R) ⋯

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

Normalize the radially weighted Taylor coefficients at the origin.

Equations

• ClassicalComplexWPT.normalizedOriginCoeffs p r hr d = (↑(ClassicalComplexWPT.originWeightedCoeffs p r hr) d)⁻¹ • ClassicalComplexWPT.originWeightedCoeffs p r hr

@[simp]

theorem ClassicalComplexWPT.normalizedOriginCoeffs_apply {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d k : ℕ) : ↑(normalizedOriginCoeffs p r hr d) k = (↑↑r ^ d * lastTaylorCoefficient p d 0)⁻¹ * (↑↑r ^ k * lastTaylorCoefficient p k 0)

theorem ClassicalComplexWPT.exists_radius_normalizedOrigin_close_half {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 ∧ ‖normalizedOriginCoeffs p r hr d - monomialSeq d‖ < 1 / 2

noncomputable def ClassicalComplexWPT.normalizedCoefficientMap {n : ℕ} (C : Base n → ↥OriginSeq) (denom : ℂ) : Base n → ↥OriginSeq

Normalize any analytic coefficient map by a fixed scalar.

Equations

• ClassicalComplexWPT.normalizedCoefficientMap C denom z = denom⁻¹ • C z

theorem ClassicalComplexWPT.analyticAt_normalizedCoefficientMap {n : ℕ} (C : Base n → ↥OriginSeq) (denom : ℂ) (hC : AnalyticAt ℂ C 0) : AnalyticAt ℂ (normalizedCoefficientMap C denom) 0

theorem ClassicalComplexWPT.eventually_norm_normalizedCoefficientMap_sub_monomial_lt_one {n d : ℕ} (C : Base n → ↥OriginSeq) (denom : ℂ) (hC : AnalyticAt ℂ C 0) (hclose : ‖normalizedCoefficientMap C denom 0 - monomialSeq d‖ < 1 / 2) : ∀ᶠ (z : Base n) in nhds 0, ‖normalizedCoefficientMap C denom z - monomialSeq d‖ < 1

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

The analytic weighted coefficient map normalized by its degree-d coefficient at the base origin.

Equations

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

theorem ClassicalComplexWPT.analyticNormalizedCoefficientMap_zero {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (d : ℕ) : analyticNormalizedCoefficientMap p r hr d 0 = normalizedOriginCoeffs p r hr d

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

theorem ClassicalComplexWPT.exists_normalizedAnalyticCoefficientMap {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 ℂ (analyticNormalizedCoefficientMap p r hr d) 0 ∧ ‖analyticNormalizedCoefficientMap p r hr d 0 - monomialSeq d‖ < 1 / 2 ∧ ∀ᶠ (z : Base n) in nhds 0, ‖analyticNormalizedCoefficientMap p r hr d z - monomialSeq d‖ < 1

Exact distinguished order supplies a normalized analytic coefficient map that is within 1/2 of the monomial at the origin and remains within 1 on a neighborhood of the base origin.