Division in weighted ℓ¹ sequence algebras

This file constructs bounded shifts, convolution division by a small tail, and the specialized one-variable quotient and remainder operators used in complex-analytic Weierstrass preparation.

def ClassicalComplexWPT.prodAntidiagonalEquiv {A : Type u_1} {B : Type u_2} : (A × A) × B × B ≃ (A × B) × A × B

Reassociate a product of two pairs into a pair of products.

Equations

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

@[instance_reducible]

noncomputable instance ClassicalComplexWPT.prodHasAntidiagonal {A : Type u_1} {B : Type u_2} [AddCommMonoid A] [AddCommMonoid B] [Finset.HasAntidiagonal A] [Finset.HasAntidiagonal B] : Finset.HasAntidiagonal (A × B)

Equations

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

noncomputable def ClassicalComplexWPT.L1Coeff.embedFun {I : Type u_1} {J : Type u_2} (e : I ↪ J) (f : ↥(L1Coeff I)) (j : J) : ℂ

Extend an ℓ¹ coefficient function by zero along an embedding.

Equations

• ClassicalComplexWPT.L1Coeff.embedFun e f j = if h : ∃ (i : I), e i = j then ↑f h.choose else 0

@[simp]

theorem ClassicalComplexWPT.L1Coeff.embedFun_apply_self {I : Type u_1} {J : Type u_2} (e : I ↪ J) (f : ↥(L1Coeff I)) (i : I) : embedFun e f (e i) = ↑f i

theorem ClassicalComplexWPT.L1Coeff.embedFun_apply_of_not_mem {I : Type u_1} {J : Type u_2} (e : I ↪ J) (f : ↥(L1Coeff I)) (j : J) (hj : j ∉ Set.range ⇑e) : embedFun e f j = 0

noncomputable def ClassicalComplexWPT.L1Coeff.embed {I : Type u_1} {J : Type u_2} (e : I ↪ J) (f : ↥(L1Coeff I)) : ↥(L1Coeff J)

Embed an ℓ¹ coefficient family by extending it by zero.

Equations

• ClassicalComplexWPT.L1Coeff.embed e f = ⟨ClassicalComplexWPT.L1Coeff.embedFun e f, ⋯⟩

@[simp]

theorem ClassicalComplexWPT.L1Coeff.embed_apply_self {I : Type u_1} {J : Type u_2} (e : I ↪ J) (f : ↥(L1Coeff I)) (i : I) : ↑(embed e f) (e i) = ↑f i

theorem ClassicalComplexWPT.L1Coeff.embed_apply_of_not_mem {I : Type u_1} {J : Type u_2} (e : I ↪ J) (f : ↥(L1Coeff I)) (j : J) (hj : j ∉ Set.range ⇑e) : ↑(embed e f) j = 0

def ClassicalComplexWPT.lowIndex {A : Type u_1} (d : ℕ) : A × ℕ ↪ A × ℕ

The embedding that shifts the distinguished index upward by d.

Equations

• ClassicalComplexWPT.lowIndex d = { toFun := fun (x : A × ℕ) => (x.1, x.2 + d), inj' := ⋯ }

noncomputable def ClassicalComplexWPT.lowShift {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) : ↥(L1Coeff (A × ℕ))

Insert d zero layers below an ℓ¹ coefficient family.

Equations

• ClassicalComplexWPT.lowShift d f = ClassicalComplexWPT.L1Coeff.embed (ClassicalComplexWPT.lowIndex d) f

@[simp]

theorem ClassicalComplexWPT.lowShift_apply_add {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) (a : A) (n : ℕ) : ↑(lowShift d f) (a, n + d) = ↑f (a, n)

theorem ClassicalComplexWPT.lowShift_apply_of_lt {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) (a : A) {n : ℕ} (hn : n < d) : ↑(lowShift d f) (a, n) = 0

theorem ClassicalComplexWPT.lowShift_apply_of_le {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) (a : A) {n : ℕ} (hn : d ≤ n) : ↑(lowShift d f) (a, n) = ↑f (a, n - d)

@[simp]

theorem ClassicalComplexWPT.highShift_lowShift {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) : highShift d (lowShift d f) = f

@[simp]

theorem ClassicalComplexWPT.highShift_lowCut {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) : highShift d (lowCut d f) = 0

theorem ClassicalComplexWPT.lowShift_highShift_add_lowCut {A : Type u_1} (d : ℕ) (f : ↥(L1Coeff (A × ℕ))) : lowShift d (highShift d f) + lowCut d f = f

theorem ClassicalComplexWPT.convolution_comm {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (f g : ↥(L1Coeff A)) : convolution f g = convolution g f

theorem ClassicalComplexWPT.convolution_add_right {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (f g₁ g₂ : ↥(L1Coeff A)) : convolution f (g₁ + g₂) = convolution f g₁ + convolution f g₂

theorem ClassicalComplexWPT.convolution_smul_right {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (c : ℂ) (f g : ↥(L1Coeff A)) : convolution f (c • g) = c • convolution f g

noncomputable def ClassicalComplexWPT.convolutionRightMap {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] : ↥(L1Coeff A) →L[ℂ] ↥(L1Coeff A) →L[ℂ] ↥(L1Coeff A)

Right convolution depends continuously and linearly on the coefficient family.

Equations

• ClassicalComplexWPT.convolutionRightMap = { toFun := ClassicalComplexWPT.convolutionRight, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem ClassicalComplexWPT.convolutionRightMap_apply {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (p : ↥(L1Coeff A)) : convolutionRightMap p = convolutionRight p

noncomputable def ClassicalComplexWPT.divisionPerturbation {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) : ↥(L1Coeff (A × ℕ)) →L[ℂ] ↥(L1Coeff (A × ℕ))

The high-shifted convolution perturbation used by division.

Equations

• ClassicalComplexWPT.divisionPerturbation d p = ClassicalComplexWPT.highShiftCLM d ∘SL ClassicalComplexWPT.convolutionRight p

@[simp]

theorem ClassicalComplexWPT.divisionPerturbation_apply {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p q : ↥(L1Coeff (A × ℕ))) : (divisionPerturbation d p) q = highShift d (convolution q p)

theorem ClassicalComplexWPT.norm_divisionPerturbation_le {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) : ‖divisionPerturbation d p‖ ≤ ‖p‖

noncomputable def ClassicalComplexWPT.divisionPerturbationMap {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) : ↥(L1Coeff (A × ℕ)) →L[ℂ] ↥(L1Coeff (A × ℕ)) →L[ℂ] ↥(L1Coeff (A × ℕ))

The operator-valued linear map p ↦ S_d C_p.

Equations

• ClassicalComplexWPT.divisionPerturbationMap d = { toFun := ClassicalComplexWPT.divisionPerturbation d, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem ClassicalComplexWPT.divisionPerturbationMap_apply {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) : (divisionPerturbationMap d) p = divisionPerturbation d p

noncomputable def ClassicalComplexWPT.divisionInverse {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) : ↥(L1Coeff (A × ℕ)) →L[ℂ] ↥(L1Coeff (A × ℕ))

The inverse of I + S_d C_p, constructed by a Neumann series.

Equations

• ClassicalComplexWPT.divisionInverse d p hp = ↑(Units.oneSub (-ClassicalComplexWPT.divisionPerturbation d p) ⋯)⁻¹

theorem ClassicalComplexWPT.divisionInverse_right {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) (b : ↥(L1Coeff (A × ℕ))) : (divisionInverse d p hp) b + highShift d (convolution ((divisionInverse d p hp) b) p) = b

theorem ClassicalComplexWPT.divisionInverse_left {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) (q : ↥(L1Coeff (A × ℕ))) : (divisionInverse d p hp) (q + highShift d (convolution q p)) = q

noncomputable def ClassicalComplexWPT.divisionQuotient {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) (f : ↥(L1Coeff (A × ℕ))) : ↥(L1Coeff (A × ℕ))

Quotient for division by the normalized divisor w^d + p.

Equations

• ClassicalComplexWPT.divisionQuotient d p hp f = (ClassicalComplexWPT.divisionInverse d p hp) (ClassicalComplexWPT.highShift d f)

noncomputable def ClassicalComplexWPT.divisionQuotientGlobal {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (pf : ↥(L1Coeff (A × ℕ)) × ↥(L1Coeff (A × ℕ))) : ↥(L1Coeff (A × ℕ))

Proof-independent quotient map, defined on all coefficient pairs by total ring inversion.

Equations

• ClassicalComplexWPT.divisionQuotientGlobal d pf = (Ring.inverse (1 + ClassicalComplexWPT.divisionPerturbation d pf.1)) (ClassicalComplexWPT.highShift d pf.2)

theorem ClassicalComplexWPT.divisionQuotientGlobal_eq {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p f : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) : divisionQuotientGlobal d (p, f) = divisionQuotient d p hp f

theorem ClassicalComplexWPT.analyticAt_inverseOneAdd_apply {X : Type u_2} {E : Type u_3} [NormedAddCommGroup X] [NormedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (K : X →L[ℂ] E →L[ℂ] E) (b : X →L[ℂ] E) (x : X) (hK : ‖K x‖ < 1) : AnalyticAt ℂ (fun (y : X) => (Ring.inverse (1 + K y)) (b y)) x

noncomputable def ClassicalComplexWPT.divisionOperatorInput {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) : ↥(L1Coeff (A × ℕ)) × ↥(L1Coeff (A × ℕ)) →L[ℂ] ↥(L1Coeff (A × ℕ)) →L[ℂ] ↥(L1Coeff (A × ℕ))

Extract the divisor perturbation operator from divisor/dividend input.

Equations

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

noncomputable def ClassicalComplexWPT.divisionRhsInput {A : Type u_1} (d : ℕ) : ↥(L1Coeff (A × ℕ)) × ↥(L1Coeff (A × ℕ)) →L[ℂ] ↥(L1Coeff (A × ℕ))

Extract and high-shift the right-hand side from divisor/dividend input.

Equations

• ClassicalComplexWPT.divisionRhsInput d = ClassicalComplexWPT.highShiftCLM d ∘SL ContinuousLinearMap.snd ℂ ↥(ClassicalComplexWPT.L1Coeff (A × ℕ)) ↥(ClassicalComplexWPT.L1Coeff (A × ℕ))

@[simp]

theorem ClassicalComplexWPT.divisionOperatorInput_apply {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (pf : ↥(L1Coeff (A × ℕ)) × ↥(L1Coeff (A × ℕ))) : (divisionOperatorInput d) pf = divisionPerturbation d pf.1

@[simp]

theorem ClassicalComplexWPT.divisionRhsInput_apply {A : Type u_1} (d : ℕ) (pf : ↥(L1Coeff (A × ℕ)) × ↥(L1Coeff (A × ℕ))) : (divisionRhsInput d) pf = highShift d pf.2

theorem ClassicalComplexWPT.analyticAt_divisionQuotientFormula {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (pf : ↥(L1Coeff (A × ℕ)) × ↥(L1Coeff (A × ℕ))) (hp : ‖pf.1‖ < 1) : AnalyticAt ℂ (fun (x : ↥(L1Coeff (A × ℕ)) × ↥(L1Coeff (A × ℕ))) => (Ring.inverse (1 + (divisionOperatorInput d) x)) ((divisionRhsInput d) x)) pf

theorem ClassicalComplexWPT.divisionQuotientFormula_eq_global {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (pf : ↥(L1Coeff (A × ℕ)) × ↥(L1Coeff (A × ℕ))) : (Ring.inverse (1 + (divisionOperatorInput d) pf)) ((divisionRhsInput d) pf) = divisionQuotientGlobal d pf

noncomputable def ClassicalComplexWPT.divisionRemainder {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) (f : ↥(L1Coeff (A × ℕ))) : ↥(L1Coeff (A × ℕ))

Remainder, supported in distinguished-variable degrees below d.

Equations

• ClassicalComplexWPT.divisionRemainder d p hp f = ClassicalComplexWPT.lowCut d (f - ClassicalComplexWPT.convolution (ClassicalComplexWPT.divisionQuotient d p hp f) p)

theorem ClassicalComplexWPT.divisionQuotient_equation {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) (f : ↥(L1Coeff (A × ℕ))) : divisionQuotient d p hp f + highShift d (convolution (divisionQuotient d p hp f) p) = highShift d f

@[simp]

theorem ClassicalComplexWPT.highShift_divisionRemainder {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) (f : ↥(L1Coeff (A × ℕ))) : highShift d (divisionRemainder d p hp f) = 0

theorem ClassicalComplexWPT.division_factorization {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) (f : ↥(L1Coeff (A × ℕ))) : f = lowShift d (divisionQuotient d p hp f) + convolution (divisionQuotient d p hp f) p + divisionRemainder d p hp f

theorem ClassicalComplexWPT.divisionQuotient_unique {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) (f q r : ↥(L1Coeff (A × ℕ))) (hfac : f = lowShift d q + convolution q p + r) (hr : highShift d r = 0) : q = divisionQuotient d p hp f

theorem ClassicalComplexWPT.division_existsUnique {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) (f : ↥(L1Coeff (A × ℕ))) : ∃! qr : ↥(L1Coeff (A × ℕ)) × ↥(L1Coeff (A × ℕ)), f = lowShift d qr.1 + convolution qr.1 p + qr.2 ∧ highShift d qr.2 = 0

Existence and uniqueness of the quotient/remainder pair for a small normalized divisor.

theorem ClassicalComplexWPT.divisionRemainder_apply_of_le {A : Type u_1} [AddCommMonoid A] [Finset.HasAntidiagonal A] (d : ℕ) (p : ↥(L1Coeff (A × ℕ))) (hp : ‖p‖ < 1) (f : ↥(L1Coeff (A × ℕ))) (a : A) {n : ℕ} (hn : d ≤ n) : ↑(divisionRemainder d p hp f) (a, n) = 0

Direct ℓ¹(ℕ) API

def ClassicalComplexWPT.seqHighShift (d : ℕ) (f : ↥(L1Coeff ℕ)) : ↥(L1Coeff ℕ)

Delete the first d coefficients of a one-variable ℓ¹ sequence.

Equations

• ClassicalComplexWPT.seqHighShift d f = ⟨fun (n : ℕ) => ↑f (n + d), ⋯⟩

@[simp]

theorem ClassicalComplexWPT.seqHighShift_apply (d : ℕ) (f : ↥(L1Coeff ℕ)) (n : ℕ) : ↑(seqHighShift d f) n = ↑f (n + d)

theorem ClassicalComplexWPT.norm_seqHighShift_le (d : ℕ) (f : ↥(L1Coeff ℕ)) : ‖seqHighShift d f‖ ≤ ‖f‖

theorem ClassicalComplexWPT.seqHighShift_add (d : ℕ) (f g : ↥(L1Coeff ℕ)) : seqHighShift d (f + g) = seqHighShift d f + seqHighShift d g

theorem ClassicalComplexWPT.seqHighShift_smul (d : ℕ) (c : ℂ) (f : ↥(L1Coeff ℕ)) : seqHighShift d (c • f) = c • seqHighShift d f

noncomputable def ClassicalComplexWPT.seqHighShiftCLM (d : ℕ) : ↥(L1Coeff ℕ) →L[ℂ] ↥(L1Coeff ℕ)

High shift on one-variable sequences as a contraction.

Equations

• ClassicalComplexWPT.seqHighShiftCLM d = { toFun := ClassicalComplexWPT.seqHighShift d, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

def ClassicalComplexWPT.seqLowIndex (d : ℕ) : ℕ ↪ ℕ

The natural-number embedding that shifts indices upward by d.

Equations

• ClassicalComplexWPT.seqLowIndex d = { toFun := fun (n : ℕ) => n + d, inj' := ⋯ }

noncomputable def ClassicalComplexWPT.seqLowShift (d : ℕ) (f : ↥(L1Coeff ℕ)) : ↥(L1Coeff ℕ)

Insert d zero coefficients at the beginning of a one-variable sequence.

Equations

• ClassicalComplexWPT.seqLowShift d f = ClassicalComplexWPT.L1Coeff.embed (ClassicalComplexWPT.seqLowIndex d) f

@[simp]

theorem ClassicalComplexWPT.seqLowShift_apply_add (d : ℕ) (f : ↥(L1Coeff ℕ)) (n : ℕ) : ↑(seqLowShift d f) (n + d) = ↑f n

theorem ClassicalComplexWPT.seqLowShift_apply_of_lt (d : ℕ) (f : ↥(L1Coeff ℕ)) {n : ℕ} (hn : n < d) : ↑(seqLowShift d f) n = 0

theorem ClassicalComplexWPT.seqLowShift_apply_of_le (d : ℕ) (f : ↥(L1Coeff ℕ)) {n : ℕ} (hn : d ≤ n) : ↑(seqLowShift d f) n = ↑f (n - d)

def ClassicalComplexWPT.seqLowCut (d : ℕ) (f : ↥(L1Coeff ℕ)) : ↥(L1Coeff ℕ)

Keep precisely the coefficients below degree d.

Equations

• ClassicalComplexWPT.seqLowCut d f = ⟨fun (n : ℕ) => if n < d then ↑f n else 0, ⋯⟩

@[simp]

theorem ClassicalComplexWPT.seqLowCut_apply_of_lt (d : ℕ) (f : ↥(L1Coeff ℕ)) {n : ℕ} (hn : n < d) : ↑(seqLowCut d f) n = ↑f n

@[simp]

theorem ClassicalComplexWPT.seqLowCut_apply_of_le (d : ℕ) (f : ↥(L1Coeff ℕ)) {n : ℕ} (hn : d ≤ n) : ↑(seqLowCut d f) n = 0

theorem ClassicalComplexWPT.norm_seqLowCut_le (d : ℕ) (f : ↥(L1Coeff ℕ)) : ‖seqLowCut d f‖ ≤ ‖f‖

theorem ClassicalComplexWPT.seqLowCut_add (d : ℕ) (f g : ↥(L1Coeff ℕ)) : seqLowCut d (f + g) = seqLowCut d f + seqLowCut d g

theorem ClassicalComplexWPT.seqLowCut_smul (d : ℕ) (c : ℂ) (f : ↥(L1Coeff ℕ)) : seqLowCut d (c • f) = c • seqLowCut d f

noncomputable def ClassicalComplexWPT.seqLowCutCLM (d : ℕ) : ↥(L1Coeff ℕ) →L[ℂ] ↥(L1Coeff ℕ)

Low-degree cutoff on one-variable sequences as a contraction.

Equations

• ClassicalComplexWPT.seqLowCutCLM d = { toFun := ClassicalComplexWPT.seqLowCut d, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem ClassicalComplexWPT.seqHighShift_seqLowShift (d : ℕ) (f : ↥(L1Coeff ℕ)) : seqHighShift d (seqLowShift d f) = f

@[simp]

theorem ClassicalComplexWPT.seqHighShift_seqLowCut (d : ℕ) (f : ↥(L1Coeff ℕ)) : seqHighShift d (seqLowCut d f) = 0

theorem ClassicalComplexWPT.seqLowShift_highShift_add_lowCut (d : ℕ) (f : ↥(L1Coeff ℕ)) : seqLowShift d (seqHighShift d f) + seqLowCut d f = f

noncomputable def ClassicalComplexWPT.seqDivisionPerturbation (d : ℕ) (p : ↥(L1Coeff ℕ)) : ↥(L1Coeff ℕ) →L[ℂ] ↥(L1Coeff ℕ)

The high-shifted convolution perturbation S_d C_p on ℓ¹(ℕ).

Equations

• ClassicalComplexWPT.seqDivisionPerturbation d p = ClassicalComplexWPT.seqHighShiftCLM d ∘SL ClassicalComplexWPT.convolutionRight p

@[simp]

theorem ClassicalComplexWPT.seqDivisionPerturbation_apply (d : ℕ) (p q : ↥(L1Coeff ℕ)) : (seqDivisionPerturbation d p) q = seqHighShift d (convolution q p)

theorem ClassicalComplexWPT.norm_seqDivisionPerturbation_le (d : ℕ) (p : ↥(L1Coeff ℕ)) : ‖seqDivisionPerturbation d p‖ ≤ ‖p‖

noncomputable def ClassicalComplexWPT.seqDivisionPerturbationMap (d : ℕ) : ↥(L1Coeff ℕ) →L[ℂ] ↥(L1Coeff ℕ) →L[ℂ] ↥(L1Coeff ℕ)

The continuous-linear family of one-variable division perturbations.

Equations

• ClassicalComplexWPT.seqDivisionPerturbationMap d = { toFun := ClassicalComplexWPT.seqDivisionPerturbation d, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem ClassicalComplexWPT.seqDivisionPerturbationMap_apply (d : ℕ) (p : ↥(L1Coeff ℕ)) : (seqDivisionPerturbationMap d) p = seqDivisionPerturbation d p

noncomputable def ClassicalComplexWPT.seqDivisionInverse (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) : ↥(L1Coeff ℕ) →L[ℂ] ↥(L1Coeff ℕ)

The Neumann-series inverse of the one-variable division operator.

Equations

• ClassicalComplexWPT.seqDivisionInverse d p hp = ↑(Units.oneSub (-ClassicalComplexWPT.seqDivisionPerturbation d p) ⋯)⁻¹

theorem ClassicalComplexWPT.seqDivisionInverse_right (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (b : ↥(L1Coeff ℕ)) : (seqDivisionInverse d p hp) b + seqHighShift d (convolution ((seqDivisionInverse d p hp) b) p) = b

theorem ClassicalComplexWPT.seqDivisionInverse_left (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (q : ↥(L1Coeff ℕ)) : (seqDivisionInverse d p hp) (q + seqHighShift d (convolution q p)) = q

noncomputable def ClassicalComplexWPT.seqDivisionQuotient (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (f : ↥(L1Coeff ℕ)) : ↥(L1Coeff ℕ)

The quotient sequence produced by the division inverse.

Equations

• ClassicalComplexWPT.seqDivisionQuotient d p hp f = (ClassicalComplexWPT.seqDivisionInverse d p hp) (ClassicalComplexWPT.seqHighShift d f)

noncomputable def ClassicalComplexWPT.seqDivisionRemainder (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (f : ↥(L1Coeff ℕ)) : ↥(L1Coeff ℕ)

The low-degree remainder sequence produced by division.

Equations

• ClassicalComplexWPT.seqDivisionRemainder d p hp f = ClassicalComplexWPT.seqLowCut d (f - ClassicalComplexWPT.convolution (ClassicalComplexWPT.seqDivisionQuotient d p hp f) p)

noncomputable def ClassicalComplexWPT.seqDivisionOperatorInput (d : ℕ) : ↥(L1Coeff ℕ) × ↥(L1Coeff ℕ) →L[ℂ] ↥(L1Coeff ℕ) →L[ℂ] ↥(L1Coeff ℕ)

Extract the sequence perturbation operator from paired input.

Equations

• ClassicalComplexWPT.seqDivisionOperatorInput d = ClassicalComplexWPT.seqDivisionPerturbationMap d ∘SL ContinuousLinearMap.fst ℂ ↥(ClassicalComplexWPT.L1Coeff ℕ) ↥(ClassicalComplexWPT.L1Coeff ℕ)

noncomputable def ClassicalComplexWPT.seqDivisionRhsInput (d : ℕ) : ↥(L1Coeff ℕ) × ↥(L1Coeff ℕ) →L[ℂ] ↥(L1Coeff ℕ)

Extract and high-shift the sequence right-hand side from paired input.

Equations

• ClassicalComplexWPT.seqDivisionRhsInput d = ClassicalComplexWPT.seqHighShiftCLM d ∘SL ContinuousLinearMap.snd ℂ ↥(ClassicalComplexWPT.L1Coeff ℕ) ↥(ClassicalComplexWPT.L1Coeff ℕ)

@[simp]

theorem ClassicalComplexWPT.seqDivisionOperatorInput_apply (d : ℕ) (pf : ↥(L1Coeff ℕ) × ↥(L1Coeff ℕ)) : (seqDivisionOperatorInput d) pf = seqDivisionPerturbation d pf.1

@[simp]

theorem ClassicalComplexWPT.seqDivisionRhsInput_apply (d : ℕ) (pf : ↥(L1Coeff ℕ) × ↥(L1Coeff ℕ)) : (seqDivisionRhsInput d) pf = seqHighShift d pf.2

noncomputable def ClassicalComplexWPT.seqDivisionQuotientGlobal (d : ℕ) (pf : ↥(L1Coeff ℕ) × ↥(L1Coeff ℕ)) : ↥(L1Coeff ℕ)

Proof-independent quotient, jointly analytic on the open set ‖p‖ < 1.

Equations

• ClassicalComplexWPT.seqDivisionQuotientGlobal d pf = (Ring.inverse (1 + (ClassicalComplexWPT.seqDivisionOperatorInput d) pf)) ((ClassicalComplexWPT.seqDivisionRhsInput d) pf)

theorem ClassicalComplexWPT.seqDivisionQuotientGlobal_eq (d : ℕ) (p f : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) : seqDivisionQuotientGlobal d (p, f) = seqDivisionQuotient d p hp f

theorem ClassicalComplexWPT.analyticAt_seqDivisionQuotientGlobal (d : ℕ) (pf : ↥(L1Coeff ℕ) × ↥(L1Coeff ℕ)) (hp : ‖pf.1‖ < 1) : AnalyticAt ℂ (seqDivisionQuotientGlobal d) pf

noncomputable def ClassicalComplexWPT.seqDivisionRemainderGlobal (d : ℕ) (pf : ↥(L1Coeff ℕ) × ↥(L1Coeff ℕ)) : ↥(L1Coeff ℕ)

Proof-independent remainder, jointly analytic wherever the divisor tail has norm below one.

Equations

• ClassicalComplexWPT.seqDivisionRemainderGlobal d pf = ClassicalComplexWPT.seqLowCut d (pf.2 - ClassicalComplexWPT.convolution (ClassicalComplexWPT.seqDivisionQuotientGlobal d pf) pf.1)

theorem ClassicalComplexWPT.seqDivisionRemainderGlobal_eq (d : ℕ) (p f : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) : seqDivisionRemainderGlobal d (p, f) = seqDivisionRemainder d p hp f

theorem ClassicalComplexWPT.analyticAt_seqDivisionRemainderGlobal (d : ℕ) (pf : ↥(L1Coeff ℕ) × ↥(L1Coeff ℕ)) (hp : ‖pf.1‖ < 1) : AnalyticAt ℂ (seqDivisionRemainderGlobal d) pf

theorem ClassicalComplexWPT.seqDivisionQuotient_equation (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (f : ↥(L1Coeff ℕ)) : seqDivisionQuotient d p hp f + seqHighShift d (convolution (seqDivisionQuotient d p hp f) p) = seqHighShift d f

@[simp]

theorem ClassicalComplexWPT.seqHighShift_divisionRemainder (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (f : ↥(L1Coeff ℕ)) : seqHighShift d (seqDivisionRemainder d p hp f) = 0

theorem ClassicalComplexWPT.seqDivision_factorization (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (f : ↥(L1Coeff ℕ)) : f = seqLowShift d (seqDivisionQuotient d p hp f) + convolution (seqDivisionQuotient d p hp f) p + seqDivisionRemainder d p hp f

theorem ClassicalComplexWPT.seqDivisionQuotient_unique (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (f q r : ↥(L1Coeff ℕ)) (hfac : f = seqLowShift d q + convolution q p + r) (hr : seqHighShift d r = 0) : q = seqDivisionQuotient d p hp f

theorem ClassicalComplexWPT.seqDivision_existsUnique (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (f : ↥(L1Coeff ℕ)) : ∃! qr : ↥(L1Coeff ℕ) × ↥(L1Coeff ℕ), f = seqLowShift d qr.1 + convolution qr.1 p + qr.2 ∧ seqHighShift d qr.2 = 0

The direct Nat-indexed division theorem with a unique quotient/remainder pair.

theorem ClassicalComplexWPT.seqDivisionRemainder_apply_of_le (d : ℕ) (p : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) (f : ↥(L1Coeff ℕ)) {n : ℕ} (hn : d ≤ n) : ↑(seqDivisionRemainder d p hp f) n = 0

theorem ClassicalComplexWPT.seqDivisionGlobal_factorization (d : ℕ) (p f : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) : f = seqLowShift d (seqDivisionQuotientGlobal d (p, f)) + convolution (seqDivisionQuotientGlobal d (p, f)) p + seqDivisionRemainderGlobal d (p, f)

@[simp]

theorem ClassicalComplexWPT.seqHighShift_divisionRemainderGlobal (d : ℕ) (p f : ↥(L1Coeff ℕ)) (hp : ‖p‖ < 1) : seqHighShift d (seqDivisionRemainderGlobal d (p, f)) = 0