Squared norms for series scalars

class NormSq (α : Type) : Type

• normSq : α → α

@[instance_reducible]

instance Rat.instNormSq : NormSq ℚ

Equations

• Rat.instNormSq = { normSq := fun (x : ℚ) => x ^ 2 }

@[instance_reducible]

instance Dyadic.instNormSq : NormSq Dyadic

Equations

• Dyadic.instNormSq = { normSq := fun (x : Dyadic) => x ^ 2 }

theorem Rat.normSq_eq_sq (x : ℚ) : NormSq.normSq x = x ^ 2

theorem Dyadic.normSq_eq_sq (x : Dyadic) : NormSq.normSq x = x ^ 2

class ApproxNormSq (α 𝕜 : Type) [NormSq α] [NontriviallyNormedField 𝕜] [Approx α 𝕜] [Approx α ℝ] : Prop

• approx_normSq {x : α} {x' : 𝕜} (ax : approx x x') : approx (NormSq.normSq x) (‖x'‖ ^ 2)

instance Rat.instApproxNormSq : ApproxNormSq ℚ ℂ

instance Dyadic.instApproxNormSq : ApproxNormSq Dyadic ℂ