Mathlib.Analysis.Normed.Ring.Lemmas

Filter.Tendsto.zero_mul_isBoundedUnder_le theorem

 {f g : ι → α} {l : Filter ι} (hf : Tendsto f l (𝓝 0)) (hg : IsBoundedUnder (· ≤ ·) l ((‖·‖) ∘ g)) :
  Tendsto (fun x => f x * g x) l (𝓝 0)

Full source

theorem Filter.Tendsto.zero_mul_isBoundedUnder_le {f g : ι → α} {l : Filter ι}
    (hf : Tendsto f l (𝓝 0)) (hg : IsBoundedUnder (· ≤ ·) l ((‖·‖) ∘ g)) :
    Tendsto (fun x => f x * g x) l (𝓝 0) :=
  hf.op_zero_isBoundedUnder_le hg (· * ·) norm_mul_le

Product of Zero-Tending and Bounded-Norm Functions Tends to Zero in Non-Unital Seminormed Rings

Informal description

Let $\alpha$ be a non-unital seminormed ring, and let $f, g : \iota \to \alpha$ be functions indexed by a type $\iota$. For a filter $l$ on $\iota$, if $f$ tends to $0$ along $l$ and the norm of $g$ is bounded under $l$, then the product function $x \mapsto f(x) \cdot g(x)$ tends to $0$ along $l$.

Filter.isBoundedUnder_le_mul_tendsto_zero theorem

 {f g : ι → α} {l : Filter ι} (hf : IsBoundedUnder (· ≤ ·) l (norm ∘ f)) (hg : Tendsto g l (𝓝 0)) :
  Tendsto (fun x => f x * g x) l (𝓝 0)

Full source

theorem Filter.isBoundedUnder_le_mul_tendsto_zero {f g : ι → α} {l : Filter ι}
    (hf : IsBoundedUnder (· ≤ ·) l (normnorm ∘ f)) (hg : Tendsto g l (𝓝 0)) :
    Tendsto (fun x => f x * g x) l (𝓝 0) :=
  hg.op_zero_isBoundedUnder_le hf (flip (· * ·)) fun x y =>
    (norm_mul_le y x).trans_eq (mul_comm _ _)

Bounded Norm and Zero Limit Imply Zero Product Limit in Non-Unital Seminormed Rings

Informal description

Let $f, g : \iota \to \alpha$ be functions and $l$ be a filter on $\iota$. If the norm of $f$ is bounded under $l$ and $g$ tends to $0$ along $l$, then the product function $x \mapsto f(x) * g(x)$ tends to $0$ along $l$.

Pi.nonUnitalSeminormedRing instance

{R : ι → Type*} [Fintype ι] [∀ i, NonUnitalSeminormedRing (R i)] : NonUnitalSeminormedRing (∀ i, R i)

Full source

/-- Non-unital seminormed ring structure on the product of finitely many non-unital seminormed
rings, using the sup norm. -/
instance Pi.nonUnitalSeminormedRing {R : ι → Type*} [Fintype ι]
    [∀ i, NonUnitalSeminormedRing (R i)] : NonUnitalSeminormedRing (∀ i, R i) :=
  { seminormedAddCommGroup, nonUnitalRing with
    norm_mul_le x y := NNReal.coe_mono <| calc
      (univ.sup fun i ↦ ‖x i * y i‖₊) ≤ univ.sup ((‖x ·‖₊) * (‖y ·‖₊)) :=
        sup_mono_fun fun _ _ ↦ nnnorm_mul_le _ _
      _ ≤ (univ.sup (‖x ·‖₊)) * univ.sup (‖y ·‖₊) :=
        sup_mul_le_mul_sup_of_nonneg (fun _ _ ↦ zero_le _) fun _ _ ↦ zero_le _}

Product of Non-Unital Seminormed Rings with Sup Norm

Informal description

For a finite index set $\iota$ and a family of non-unital seminormed rings $(R_i)_{i \in \iota}$, the product space $\prod_{i \in \iota} R_i$ is a non-unital seminormed ring when equipped with the supremum norm $\|(x_i)\| = \sup_{i \in \iota} \|x_i\|$.

Pi.seminormedRing instance

{R : ι → Type*} [Fintype ι] [∀ i, SeminormedRing (R i)] : SeminormedRing (∀ i, R i)

Full source

/-- Seminormed ring structure on the product of finitely many seminormed rings,
  using the sup norm. -/
instance Pi.seminormedRing {R : ι → Type*} [Fintype ι] [∀ i, SeminormedRing (R i)] :
    SeminormedRing (∀ i, R i) :=
  { Pi.nonUnitalSeminormedRing, Pi.ring with }

Product of Seminormed Rings with Sup Norm

Informal description

For a finite index set $\iota$ and a family of seminormed rings $(R_i)_{i \in \iota}$, the product space $\prod_{i \in \iota} R_i$ is a seminormed ring when equipped with the supremum norm $\|(x_i)\| = \sup_{i \in \iota} \|x_i\|$.

Pi.nonUnitalNormedRing instance

{R : ι → Type*} [Fintype ι] [∀ i, NonUnitalNormedRing (R i)] : NonUnitalNormedRing (∀ i, R i)

Full source

/-- Normed ring structure on the product of finitely many non-unital normed rings, using the sup
norm. -/
instance Pi.nonUnitalNormedRing {R : ι → Type*} [Fintype ι] [∀ i, NonUnitalNormedRing (R i)] :
    NonUnitalNormedRing (∀ i, R i) :=
  { Pi.nonUnitalSeminormedRing, Pi.normedAddCommGroup with }

Product of Non-Unital Normed Rings with Sup Norm

Informal description

For a finite index set $\iota$ and a family of non-unital normed rings $(R_i)_{i \in \iota}$, the product space $\prod_{i \in \iota} R_i$ is a non-unital normed ring when equipped with the supremum norm $\|(x_i)\| = \sup_{i \in \iota} \|x_i\|$.

Pi.normedRing instance

{R : ι → Type*} [Fintype ι] [∀ i, NormedRing (R i)] : NormedRing (∀ i, R i)

Full source

/-- Normed ring structure on the product of finitely many normed rings, using the sup norm. -/
instance Pi.normedRing {R : ι → Type*} [Fintype ι] [∀ i, NormedRing (R i)] :
    NormedRing (∀ i, R i) :=
  { Pi.seminormedRing, Pi.normedAddCommGroup with }

Product of Normed Rings with Sup Norm

Informal description

For a finite index set $\iota$ and a family of normed rings $(R_i)_{i \in \iota}$, the product space $\prod_{i \in \iota} R_i$ is a normed ring when equipped with the supremum norm $\|(x_i)\| = \sup_{i \in \iota} \|x_i\|$.

Pi.nonUnitalSeminormedCommRing instance

{R : ι → Type*} [Fintype ι] [∀ i, NonUnitalSeminormedCommRing (R i)] : NonUnitalSeminormedCommRing (∀ i, R i)

Full source

/-- Non-unital seminormed commutative ring structure on the product of finitely many non-unital
seminormed commutative rings, using the sup norm. -/
instance Pi.nonUnitalSeminormedCommRing {R : ι → Type*} [Fintype ι]
    [∀ i, NonUnitalSeminormedCommRing (R i)] : NonUnitalSeminormedCommRing (∀ i, R i) :=
  { Pi.nonUnitalSeminormedRing, Pi.nonUnitalCommRing with }

Product of Non-Unital Seminormed Commutative Rings with Sup Norm

Informal description

For a finite index set $\iota$ and a family of non-unital seminormed commutative rings $(R_i)_{i \in \iota}$, the product space $\prod_{i \in \iota} R_i$ is a non-unital seminormed commutative ring when equipped with the supremum norm $\|(x_i)\| = \sup_{i \in \iota} \|x_i\|$.

Pi.nonUnitalNormedCommRing instance

{R : ι → Type*} [Fintype ι] [∀ i, NonUnitalNormedCommRing (R i)] : NonUnitalNormedCommRing (∀ i, R i)

Full source

/-- Normed commutative ring structure on the product of finitely many non-unital normed
commutative rings, using the sup norm. -/
instance Pi.nonUnitalNormedCommRing {R : ι → Type*} [Fintype ι]
    [∀ i, NonUnitalNormedCommRing (R i)] : NonUnitalNormedCommRing (∀ i, R i) :=
  { Pi.nonUnitalSeminormedCommRing, Pi.normedAddCommGroup with }

Product of Non-Unital Normed Commutative Rings with Sup Norm

Informal description

For a finite index set $\iota$ and a family of non-unital normed commutative rings $(R_i)_{i \in \iota}$, the product space $\prod_{i \in \iota} R_i$ is a non-unital normed commutative ring when equipped with the supremum norm $\|(x_i)\| = \sup_{i \in \iota} \|x_i\|$.

Pi.seminormedCommRing instance

{R : ι → Type*} [Fintype ι] [∀ i, SeminormedCommRing (R i)] : SeminormedCommRing (∀ i, R i)

Full source

/-- Seminormed commutative ring structure on the product of finitely many seminormed commutative
rings, using the sup norm. -/
instance Pi.seminormedCommRing {R : ι → Type*} [Fintype ι] [∀ i, SeminormedCommRing (R i)] :
    SeminormedCommRing (∀ i, R i) :=
  { Pi.nonUnitalSeminormedCommRing, Pi.ring with }

Product of Seminormed Commutative Rings with Sup Norm

Informal description

For a finite index set $\iota$ and a family of seminormed commutative rings $(R_i)_{i \in \iota}$, the product space $\prod_{i \in \iota} R_i$ is a seminormed commutative ring when equipped with the supremum norm $\|(x_i)\| = \sup_{i \in \iota} \|x_i\|$.

Pi.normedCommutativeRing instance

{R : ι → Type*} [Fintype ι] [∀ i, NormedCommRing (R i)] : NormedCommRing (∀ i, R i)

Full source

/-- Normed commutative ring structure on the product of finitely many normed commutative rings,
using the sup norm. -/
instance Pi.normedCommutativeRing {R : ι → Type*} [Fintype ι] [∀ i, NormedCommRing (R i)] :
    NormedCommRing (∀ i, R i) :=
  { Pi.seminormedCommRing, Pi.normedAddCommGroup with }

Product of Normed Commutative Rings with Sup Norm

Informal description

For a finite index set $\iota$ and a family of normed commutative rings $(R_i)_{i \in \iota}$, the product space $\prod_{i \in \iota} R_i$ is a normed commutative ring when equipped with the supremum norm $\|(x_i)\| = \sup_{i \in \iota} \|x_i\|$.

NonUnitalSeminormedRing.toContinuousMul instance

[NonUnitalSeminormedRing α] : ContinuousMul α

Full source

instance (priority := 100) NonUnitalSeminormedRing.toContinuousMul [NonUnitalSeminormedRing α] :
    ContinuousMul α :=
  ⟨continuous_iff_continuousAt.2 fun x =>
      tendsto_iff_norm_sub_tendsto_zero.2 <| by
        have : ∀ e : α × α,
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := by
          intro e
          calc
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
              rw [mul_sub, sub_mul, sub_add_sub_cancel]
            _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
              norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
        refine squeeze_zero (fun e => norm_nonneg _) this ?_
        convert
          ((continuous_fst.tendsto x).norm.mul
                ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
            (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul _)
        -- Porting note: `show` used to select a goal to work on
        rotate_right
        · show Tendsto _ _ _
          exact tendsto_const_nhds
        · simp⟩

Multiplication is Continuous in Non-Unital Seminormed Rings

Informal description

Every non-unital seminormed ring $\alpha$ has a continuous multiplication operation.

NonUnitalSeminormedRing.toIsTopologicalRing instance

[NonUnitalSeminormedRing α] : IsTopologicalRing α

Full source

/-- A seminormed ring is a topological ring. -/
instance (priority := 100) NonUnitalSeminormedRing.toIsTopologicalRing [NonUnitalSeminormedRing α] :
    IsTopologicalRing α where

Non-Unital Seminormed Rings are Topological Rings

Informal description

Every non-unital seminormed ring $\alpha$ is a topological ring.

SeparationQuotient.instNonUnitalNormedRing instance

[NonUnitalSeminormedRing α] : NonUnitalNormedRing (SeparationQuotient α)

Full source

instance [NonUnitalSeminormedRing α] : NonUnitalNormedRing (SeparationQuotient α) where
  __ : NonUnitalRing (SeparationQuotient α) := inferInstance
  __ : NormedAddCommGroup (SeparationQuotient α) := inferInstance
  norm_mul_le := Quotient.ind₂ norm_mul_le

Non-unital Normed Ring Structure on Separation Quotient of Non-unital Seminormed Rings

Informal description

For any non-unital seminormed ring $\alpha$, the separation quotient of $\alpha$ is a non-unital normed ring.

SeparationQuotient.instNonUnitalNormedCommRing instance

[NonUnitalSeminormedCommRing α] : NonUnitalNormedCommRing (SeparationQuotient α)

Full source

instance [NonUnitalSeminormedCommRing α] : NonUnitalNormedCommRing (SeparationQuotient α) where
  __ : NonUnitalCommRing (SeparationQuotient α) := inferInstance
  __ : NormedAddCommGroup (SeparationQuotient α) := inferInstance
  norm_mul_le := Quotient.ind₂ norm_mul_le

Non-unital Normed Commutative Ring Structure on Separation Quotient of Non-unital Seminormed Commutative Rings

Informal description

For any non-unital seminormed commutative ring $\alpha$, the separation quotient of $\alpha$ is a non-unital normed commutative ring.

SeparationQuotient.instNormedRing instance

[SeminormedRing α] : NormedRing (SeparationQuotient α)

Full source

instance [SeminormedRing α] : NormedRing (SeparationQuotient α) where
  __ : Ring (SeparationQuotient α) := inferInstance
  __ : NormedAddCommGroup (SeparationQuotient α) := inferInstance
  norm_mul_le := Quotient.ind₂ norm_mul_le

Normed Ring Structure on Separation Quotient of Seminormed Rings

Informal description

For any seminormed ring $\alpha$, the separation quotient of $\alpha$ is a normed ring.

SeparationQuotient.instNormedCommRing instance

[SeminormedCommRing α] : NormedCommRing (SeparationQuotient α)

Full source

instance [SeminormedCommRing α] : NormedCommRing (SeparationQuotient α) where
  __ : CommRing (SeparationQuotient α) := inferInstance
  __ : NormedAddCommGroup (SeparationQuotient α) := inferInstance
  norm_mul_le := Quotient.ind₂ norm_mul_le

Normed Commutative Ring Structure on Separation Quotient of Seminormed Commutative Rings

Informal description

For any seminormed commutative ring $\alpha$, the separation quotient of $\alpha$ is a normed commutative ring.

SeparationQuotient.instNormOneClass instance

[SeminormedAddCommGroup α] [One α] [NormOneClass α] : NormOneClass (SeparationQuotient α)

Full source

instance [SeminormedAddCommGroup α] [One α] [NormOneClass α] :
    NormOneClass (SeparationQuotient α) where
  norm_one := norm_one (α := α)

Norm of One in Separation Quotient

Informal description

For any seminormed additive commutative group $\alpha$ with a multiplicative identity and satisfying `NormOneClass`, the separation quotient of $\alpha$ also satisfies `NormOneClass`, meaning the norm of the multiplicative identity in the quotient is 1.

NNReal.lipschitzWith_sub theorem

: LipschitzWith 2 (fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 - p.2)

Full source

lemma lipschitzWith_sub : LipschitzWith 2 (fun (p : ℝ≥0ℝ≥0 × ℝ≥0) ↦ p.1 - p.2) := by
  rw [← isometry_subtype_coe.lipschitzWith_iff]
  have : Isometry (Prod.map ((↑) : ℝ≥0 → ℝ) ((↑) : ℝ≥0 → ℝ)) :=
    isometry_subtype_coe.prodMap isometry_subtype_coe
  convert (((LipschitzWith.prod_fst.comp this.lipschitz).sub
    (LipschitzWith.prod_snd.comp this.lipschitz)).max_const 0)
  norm_num

Lipschitz continuity of subtraction on nonnegative reals with constant 2

Informal description

The function $f : \mathbb{R}_{\geq 0} \times \mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0}$ defined by $f(p) = p_1 - p_2$ is Lipschitz continuous with constant 2.

Int.instNormedCommRing instance

: NormedCommRing ℤ

Full source

instance Int.instNormedCommRing : NormedCommRing ℤ where
  __ := instCommRing
  __ := instNormedAddCommGroup
  norm_mul_le m n := by simp only [norm, Int.cast_mul, abs_mul, le_rfl]

The Normed Commutative Ring Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a normed commutative ring, where the norm is given by the absolute value function.

Int.instNormOneClass instance

: NormOneClass ℤ

Full source

instance Int.instNormOneClass : NormOneClass ℤ :=
  ⟨by simp [← Int.norm_cast_real]⟩

Norm of One in Integers

Informal description

The integers $\mathbb{Z}$ satisfy $\|1\| = 1$ with respect to their canonical norm (absolute value).

Int.instNormMulClass instance

: NormMulClass ℤ

Full source

instance Int.instNormMulClass : NormMulClass ℤ :=
  ⟨fun a b ↦ by simp [← Int.norm_cast_real, abs_mul]⟩

Strictly Multiplicative Norm Property of Integers

Informal description

The integers $\mathbb{Z}$ form a normed multiplicative class, where the norm is strictly multiplicative, i.e., the norm of the product of two integers equals the product of their norms: $\|a \cdot b\| = \|a\| \cdot \|b\|$.

antilipschitzWith_mul_left theorem

{a : α} (ha : a ≠ 0) : AntilipschitzWith (‖a‖₊⁻¹) (a * ·)

Full source

lemma antilipschitzWith_mul_left {a : α} (ha : a ≠ 0) : AntilipschitzWith (‖a‖₊‖a‖₊⁻¹) (a * ·) :=
  AntilipschitzWith.of_le_mul_dist fun _ _ ↦ by simp [dist_eq_norm, ← mul_sub, ha]

Antilipschitz Property of Left Multiplication in Normed Rings

Informal description

For any nonzero element $a$ in a normed ring $\alpha$, the left multiplication map $x \mapsto a \cdot x$ is antilipschitz with constant $\|a\|^{-1}$.

antilipschitzWith_mul_right theorem

{a : α} (ha : a ≠ 0) : AntilipschitzWith (‖a‖₊⁻¹) (· * a)

Full source

lemma antilipschitzWith_mul_right {a : α} (ha : a ≠ 0) : AntilipschitzWith (‖a‖₊‖a‖₊⁻¹) (· * a) :=
  AntilipschitzWith.of_le_mul_dist fun _ _ ↦ by simp [dist_eq_norm, ← sub_mul, mul_comm, ha]

Antilipschitz Property of Right Multiplication in Normed Rings

Informal description

For any nonzero element $a$ in a normed ring $\alpha$, the right multiplication map $x \mapsto x \cdot a$ is antilipschitz with constant $\|a\|^{-1}$.

Dilation.mulLeft definition

(a : α) (ha : a ≠ 0) : α →ᵈ α

Full source

/-- Multiplication by a nonzero element `a` on the left, as a `Dilation` of a ring with a strictly
multiplicative norm. -/
@[simps!]
def Dilation.mulLeft (a : α) (ha : a ≠ 0) : α →ᵈ α where
  toFun b := a * b
  edist_eq' := ⟨‖a‖₊, nnnorm_ne_zero_iff.2 ha, fun x y ↦ by
    simp [edist_nndist, nndist_eq_nnnorm, ← mul_sub]⟩

Left multiplication as a dilation in a normed ring

Informal description

For a nonzero element $a$ in a ring $\alpha$ with a strictly multiplicative norm, the left multiplication map $x \mapsto a \cdot x$ is a dilation. Specifically, the map scales distances by the norm of $a$, i.e., $\text{dist}(a \cdot x, a \cdot y) = \|a\| \cdot \text{dist}(x, y)$ for all $x, y \in \alpha$.

Dilation.mulRight definition

(a : α) (ha : a ≠ 0) : α →ᵈ α

Full source

/-- Multiplication by a nonzero element `a` on the right, as a `Dilation` of a ring with a strictly
multiplicative norm. -/
@[simps!]
def Dilation.mulRight (a : α) (ha : a ≠ 0) : α →ᵈ α where
  toFun b := b * a
  edist_eq' := ⟨‖a‖₊, nnnorm_ne_zero_iff.2 ha, fun x y ↦ by
    simp [edist_nndist, nndist_eq_nnnorm, ← sub_mul, ← mul_comm (‖a‖₊)]⟩

Right multiplication as a dilation in a normed ring

Informal description

For a nonzero element $a$ in a ring $\alpha$ with a strictly multiplicative norm, the right multiplication map $x \mapsto x \cdot a$ is a dilation. Specifically, the map scales distances by the norm of $a$, i.e., $\text{dist}(x \cdot a, y \cdot a) = \|a\| \cdot \text{dist}(x, y)$ for all $x, y \in \alpha$.

Filter.comap_mul_left_cobounded theorem

{a : α} (ha : a ≠ 0) : comap (a * ·) (cobounded α) = cobounded α

Full source

@[simp]
lemma comap_mul_left_cobounded {a : α} (ha : a ≠ 0) :
    comap (a * ·) (cobounded α) = cobounded α :=
  Dilation.comap_cobounded (Dilation.mulLeft a ha)

Left Multiplication Preserves Cobounded Filter in Normed Rings

Informal description

For any nonzero element $a$ in a normed ring $\alpha$, the preimage of the cobounded filter under the left multiplication map $x \mapsto a \cdot x$ is equal to the cobounded filter itself, i.e., $\text{comap}\, (a \cdot \cdot)\, (\text{cobounded}\, \alpha) = \text{cobounded}\, \alpha$.

Filter.comap_mul_right_cobounded theorem

{a : α} (ha : a ≠ 0) : comap (· * a) (cobounded α) = cobounded α

Full source

@[simp]
lemma comap_mul_right_cobounded {a : α} (ha : a ≠ 0) :
    comap (· * a) (cobounded α) = cobounded α :=
  Dilation.comap_cobounded (Dilation.mulRight a ha)

Right Multiplication Preserves Cobounded Filter in Normed Rings

Informal description

For any nonzero element $a$ in a normed ring $\alpha$, the preimage of the cobounded filter under the right multiplication map $x \mapsto x \cdot a$ is equal to the cobounded filter itself, i.e., $\text{comap}\, (\cdot * a)\, (\text{cobounded}\, \alpha) = \text{cobounded}\, \alpha$.

IsOfFinOrder.norm_eq_one theorem

(ha : IsOfFinOrder a) : ‖a‖ = 1

Full source

protected lemma IsOfFinOrder.norm_eq_one (ha : IsOfFinOrder a) : ‖a‖ = 1 :=
  ((normHom : α →*₀ ℝ).toMonoidHom.isOfFinOrder ha).eq_one <| norm_nonneg _

Norm of Finite Order Element Equals One

Informal description

For any element $a$ of finite order in a normed ring $\alpha$, the norm of $a$ is equal to $1$, i.e., $\|a\| = 1$.

AddChar.norm_apply theorem

{G : Type*} [AddLeftCancelMonoid G] [Finite G] (ψ : AddChar G α) (x : G) : ‖ψ x‖ = 1

Full source

@[simp] lemma AddChar.norm_apply {G : Type*} [AddLeftCancelMonoid G] [Finite G] (ψ : AddChar G α)
    (x : G) : ‖ψ x‖ = 1 := (ψ.toMonoidHom.isOfFinOrder <| isOfFinOrder_of_finite _).norm_eq_one

Norm of Additive Character on Finite Monoid Equals One

Informal description

Let $G$ be a finite additive left-cancel monoid and $\psi \colon G \to \alpha$ be an additive character. Then for every $x \in G$, the norm of $\psi(x)$ equals 1, i.e., $\|\psi(x)\| = 1$.