The Weierstrass remainder bound…

TheoremThe Weierstrass remainder bound ‖r‖ ≤ ‖f‖, for the Gauss norm at c#

TauCeti.PowerSeries.IsMulDistinguished.gaussNorm_weierstrassMod_le.{u_1} {R : Type u_1}
  [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {s : ℕ}
  {g : ↥(PowerSeries.IsRestricted.subring c)} [CompleteSpace R]
  (hg : TauCeti.PowerSeries.IsMulDistinguished c s ↑g) (hc : 0 < c)
  (f : ↥(PowerSeries.IsRestricted.subring c)) :
  PowerSeries.gaussNorm norm c ↑((hg.weierstrassMod hc) f) ≤ PowerSeries.gaussNorm norm c ↑f

Lean

Formalized in Tau Ceti as TauCeti.PowerSeries.IsMulDistinguished.gaussNorm_weierstrassMod_le.

Sources

• Tau Ceti documentation: TauCeti.PowerSeries.IsMulDistinguished.gaussNorm_weierstrassMod_le
• Source of TauCeti.PowerSeries.IsMulDistinguished.gaussNorm_weierstrassMod_le in TauCeti/RingTheory/PowerSeries/Weierstrass/DivMod.lean

LeanTauCeti.PowerSeries.IsMulDistinguished.gaussNorm_weierstrassMod_le

Uses 2

Proof usesThe Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2) · The Weierstrass norm identity

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.