The splitting operators Q, R on the Banach algebras B_ρ

For a formal series F in m + 1 variables with distinguished variable x_0, F = x_0^d · wQ d F + wR d F where wR d F collects the monomials of x_0-degree < d (X_pow_mul_wQ_add_wR). This module bounds both pieces in the majorant norm: ‖wR d F‖_ρ ≤ ‖F‖_ρ (a subseries of a positive series) and ‖wQ d F‖_ρ ≤ ρ_0^{-d} ‖F‖_ρ (the monomial x^ν of wQ d F comes from x^{ν + d e_0} of F, whose weight is ρ_0^d times larger). Hence Q = wQ d and R = wR d are continuous linear operators on B_ρ with ‖Q‖ ≤ ρ_0^{-d}, ‖R‖ ≤ 1, the estimate behind the contraction step of the Banach-algebra proof of the Weierstrass division theorem [GR71, Kapitel I].

The module also records the smallness device: if all pure x_0-coefficients of h vanish, shrinking the tail radii ρ_1, …, ρ_m by a factor t ≤ 1 (and keeping ρ_0) multiplies the weight of every monomial of h by at most t, so ‖h‖_{ρ'} ≤ t ‖h‖_ρ can be made as small as required.

The coefficient field K is ℝ or ℂ ([RCLike K]).

theorem Analytic.convNorm_wQ_le {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (d : ℕ) (F : MvPowerSeries (Fin (m + 1)) K) : ConvNorm (↑ρ) (wQ d F) ≤ ↑((↑ρ 0)⁻¹ ^ d) * ConvNorm (↑ρ) F

The quotient piece: ‖wQ d F‖_ρ ≤ ρ_0^{-d} ‖F‖_ρ.

theorem Analytic.convNorm_wR_le {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (d : ℕ) (F : MvPowerSeries (Fin (m + 1)) K) : ConvNorm (↑ρ) (wR d F) ≤ ConvNorm (↑ρ) F

The remainder piece: ‖wR d F‖_ρ ≤ ‖F‖_ρ.

theorem Analytic.wQ_add {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (F G : MvPowerSeries (Fin (m + 1)) K) : wQ d (F + G) = wQ d F + wQ d G

theorem Analytic.wQ_smul {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (c : K) (F : MvPowerSeries (Fin (m + 1)) K) : wQ d (c • F) = c • wQ d F

theorem Analytic.wR_add {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (F G : MvPowerSeries (Fin (m + 1)) K) : wR d (F + G) = wR d F + wR d G

theorem Analytic.wR_smul {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (c : K) (F : MvPowerSeries (Fin (m + 1)) K) : wR d (c • F) = c • wR d F

theorem Analytic.wQ_mem_banachSeries {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (d : ℕ) (F : ↥(BanachSeries K ρ)) : wQ d ↑F ∈ BanachSeries K ρ

theorem Analytic.wR_mem_banachSeries {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (d : ℕ) (F : ↥(BanachSeries K ρ)) : wR d ↑F ∈ BanachSeries K ρ

noncomputable def Analytic.wQLinear (K : Type u_1) [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (d : ℕ) : ↥(BanachSeries K ρ) →ₗ[K] ↥(BanachSeries K ρ)

The quotient operator Q = wQ d as a linear map on B_ρ.

Equations

• Analytic.wQLinear K ρ d = { toFun := fun (F : ↥(Analytic.BanachSeries K ρ)) => ⟨Analytic.wQ d ↑F, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def Analytic.wRLinear (K : Type u_1) [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (d : ℕ) : ↥(BanachSeries K ρ) →ₗ[K] ↥(BanachSeries K ρ)

The remainder operator R = wR d as a linear map on B_ρ.

Equations

• Analytic.wRLinear K ρ d = { toFun := fun (F : ↥(Analytic.BanachSeries K ρ)) => ⟨Analytic.wR d ↑F, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem Analytic.norm_wQLinear_le {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (d : ℕ) (F : ↥(BanachSeries K ρ)) : ‖(wQLinear K ρ d) F‖ ≤ (↑(↑ρ 0))⁻¹ ^ d * ‖F‖

theorem Analytic.norm_wRLinear_le {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (d : ℕ) (F : ↥(BanachSeries K ρ)) : ‖(wRLinear K ρ d) F‖ ≤ 1 * ‖F‖

theorem Analytic.exists_splitting_clm (K : Type u_1) [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (d : ℕ) : ∃ (Q : ↥(BanachSeries K ρ) →L[K] ↥(BanachSeries K ρ)) (R : ↥(BanachSeries K ρ) →L[K] ↥(BanachSeries K ρ)), (∀ (F : ↥(BanachSeries K ρ)), ↑(Q F) = wQ d ↑F) ∧ (∀ (F : ↥(BanachSeries K ρ)), ↑(R F) = wR d ↑F) ∧ ‖Q‖ ≤ (↑(↑ρ 0))⁻¹ ^ d ∧ ‖R‖ ≤ 1

The operator bounds: Q and R are continuous linear operators on B_ρ with ‖Q‖ ≤ ρ_0^{-d} and ‖R‖ ≤ 1 [GR71, Kapitel I].

theorem Analytic.convNorm_tailScale_le {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin (m + 1) → NNReal) {t : NNReal} (ht : t ≤ 1) {h : MvPowerSeries (Fin (m + 1)) K} (h0 : TailVanishes h) : ConvNorm (fun (k : Fin (m + 1)) => if k = 0 then ρ 0 else t * ρ k) h ≤ ↑t * ConvNorm ρ h

Scaling the tail radii by t ≤ 1 scales the norm of a series without pure x_0-terms by at most t.

theorem Analytic.exists_radius_convNorm_le {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius (m + 1)} {h : MvPowerSeries (Fin (m + 1)) K} (hh : ConvNorm (↑ρ) h ≠ ⊤) (h0 : TailVanishes h) {ε : ENNReal} (hε : 0 < ε) : ∃ (ρ' : Radius (m + 1)), ↑ρ' 0 = ↑ρ 0 ∧ (∀ (k : Fin (m + 1)), ↑ρ' k ≤ ↑ρ k) ∧ ConvNorm (↑ρ') h ≤ ε

The smallness device: a convergent series without pure x_0-terms has norm ≤ ε after shrinking the tail radii, keeping ρ_0.