Restriction to the distinguished axis #
The regularity condition of the Weierstrass theorems, f(0, …, 0, x_m) ∼ x_m^d in the printed
form [BM88, proof of Theorem 4.4, p. 24], concerns the restriction of the series to the
distinguished axis. This module provides that restriction, axis f := f(x_0, 0, …, 0) as a series
in one variable, as a ring homomorphism axisHom (the antidiagonal of a pure power x_0^k
consists of pure powers, Finsupp.antidiagonal_single), together with its values on the lifts
liftFirst (inverse: axis (liftFirst e) = e) and liftTail (the constant term), and the
majorant-norm comparisons ‖axis f‖_{ρ_0} ≤ ‖f‖_ρ, ‖liftFirst e‖_ρ = ‖e‖_{ρ_0} that keep both
operations inside the convergent series.
The coefficient field K is ℝ or ℂ ([RCLike K]).
Restriction of a series in x_0, …, x_m to the x_0-axis: f(x_0, 0, …, 0).
Equations
- Analytic.axis f ν = (MvPowerSeries.coeff (Finsupp.single 0 (ν 0))) f
Instances For
Restriction to the x_0-axis as a ring homomorphism.
Equations
- Analytic.axisHom K = { toFun := Analytic.axis, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }