Documentation

Mathlib.Analysis.Normed.Field.Lemmas

Normed fields #

In this file we continue building the theory of (semi)normed rings and fields.

source
theorem Filter.Tendsto.zero_mul_isBoundedUnder_le {α : Type u_1} {ι : Type u_3} [NonUnitalSeminormedRing α] {f : ι → α} {g : ι → α} {l : Filter ι} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l ((fun (x : α) => ‖x‖) ∘ g)) :
Filter.Tendsto (fun (x : ι) => f x * g x) l (nhds 0)
source
theorem Filter.isBoundedUnder_le_mul_tendsto_zero {α : Type u_1} {ι : Type u_3} [NonUnitalSeminormedRing α] {f : ι → α} {g : ι → α} {l : Filter ι} (hf : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)) (hg : Filter.Tendsto g l (nhds 0)) :
Filter.Tendsto (fun (x : ι) => f x * g x) l (nhds 0)
source
instance Pi.nonUnitalSeminormedRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NonUnitalSeminormedRing (π i)] :
NonUnitalSeminormedRing ((i : ι) → π i)

Non-unital seminormed ring structure on the product of finitely many non-unital seminormed rings, using the sup norm.

Equations
source
instance Pi.seminormedRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedRing (π i)] :
SeminormedRing ((i : ι) → π i)

Seminormed ring structure on the product of finitely many seminormed rings, using the sup norm.

Equations
source
instance Pi.nonUnitalNormedRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NonUnitalNormedRing (π i)] :
NonUnitalNormedRing ((i : ι) → π i)

Normed ring structure on the product of finitely many non-unital normed rings, using the sup norm.

Equations
source
instance Pi.normedRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NormedRing (π i)] :
NormedRing ((i : ι) → π i)

Normed ring structure on the product of finitely many normed rings, using the sup norm.

Equations
source
instance Pi.nonUnitalSeminormedCommRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NonUnitalSeminormedCommRing (π i)] :
NonUnitalSeminormedCommRing ((i : ι) → π i)

Non-unital seminormed commutative ring structure on the product of finitely many non-unital seminormed commutative rings, using the sup norm.

Equations
source
instance Pi.nonUnitalNormedCommRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NonUnitalNormedCommRing (π i)] :
NonUnitalNormedCommRing ((i : ι) → π i)

Normed commutative ring structure on the product of finitely many non-unital normed commutative rings, using the sup norm.

Equations
source
instance Pi.seminormedCommRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedCommRing (π i)] :
SeminormedCommRing ((i : ι) → π i)

Seminormed commutative ring structure on the product of finitely many seminormed commutative rings, using the sup norm.

Equations
source
instance Pi.normedCommutativeRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NormedCommRing (π i)] :
NormedCommRing ((i : ι) → π i)

Normed commutative ring structure on the product of finitely many normed commutative rings, using the sup norm.

Equations
source
@[instance 100]
instance semi_normed_ring_top_monoid {α : Type u_1} [NonUnitalSeminormedRing α] :
ContinuousMul α
Equations
  • ⋯ = ⋯
source
@[instance 100]
instance semi_normed_top_ring {α : Type u_1} [NonUnitalSeminormedRing α] :
TopologicalRing α

A seminormed ring is a topological ring.

Equations
  • ⋯ = ⋯
source
theorem antilipschitzWith_mul_left {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) :
AntilipschitzWith ‖a‖₊⁻¹ fun (x : α) => a * x
source
theorem antilipschitzWith_mul_right {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) :
AntilipschitzWith ‖a‖₊⁻¹ fun (x : α) => x * a
source
@[simp]
theorem DilationEquiv.mulLeft_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) :
(DilationEquiv.mulLeft a ha).symm x = a⁻¹ * x
source
@[simp]
theorem DilationEquiv.mulLeft_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) :
(DilationEquiv.mulLeft a ha) x = a * x
source
def DilationEquiv.mulLeft {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) :
α ≃ᵈ α

Multiplication by a nonzero element a on the left as a DilationEquiv of a normed division ring.

Equations
Instances For
    source
    @[simp]
    theorem DilationEquiv.mulRight_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) :
    (DilationEquiv.mulRight a ha) x = x * a
    source
    @[simp]
    theorem DilationEquiv.mulRight_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) :
    (DilationEquiv.mulRight a ha).symm x = x * a⁻¹
    source
    def DilationEquiv.mulRight {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) :
    α ≃ᵈ α

    Multiplication by a nonzero element a on the right as a DilationEquiv of a normed division ring.

    Equations
    Instances For
      source
      @[simp]
      theorem Filter.comap_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) :
      Filter.comap (fun (x : α) => a * x) (Bornology.cobounded α) = Bornology.cobounded α
      source
      @[simp]
      theorem Filter.map_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) :
      Filter.map (fun (x : α) => a * x) (Bornology.cobounded α) = Bornology.cobounded α
      source
      @[simp]
      theorem Filter.comap_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) :
      Filter.comap (fun (x : α) => x * a) (Bornology.cobounded α) = Bornology.cobounded α
      source
      @[simp]
      theorem Filter.map_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) :
      Filter.map (fun (x : α) => x * a) (Bornology.cobounded α) = Bornology.cobounded α
      source
      theorem Filter.tendsto_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) :
      Filter.Tendsto (fun (x : α) => a * x) (Bornology.cobounded α) (Bornology.cobounded α)

      Multiplication on the left by a nonzero element of a normed division ring tends to infinity at infinity.

      source
      theorem Filter.tendsto_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) :
      Filter.Tendsto (fun (x : α) => x * a) (Bornology.cobounded α) (Bornology.cobounded α)

      Multiplication on the right by a nonzero element of a normed division ring tends to infinity at infinity.

      source
      @[simp]
      theorem Filter.inv_cobounded₀ {α : Type u_1} [NormedDivisionRing α] :
      (Bornology.cobounded α)⁻¹ = nhdsWithin 0 {0}ᶜ
      source
      @[simp]
      theorem Filter.inv_nhdsWithin_ne_zero {α : Type u_1} [NormedDivisionRing α] :
      (nhdsWithin 0 {0}ᶜ)⁻¹ = Bornology.cobounded α
      source
      theorem Filter.tendsto_inv₀_cobounded' {α : Type u_1} [NormedDivisionRing α] :
      Filter.Tendsto Inv.inv (Bornology.cobounded α) (nhdsWithin 0 {0}ᶜ)
      source
      theorem Filter.tendsto_inv₀_cobounded {α : Type u_1} [NormedDivisionRing α] :
      Filter.Tendsto Inv.inv (Bornology.cobounded α) (nhds 0)
      source
      theorem Filter.tendsto_inv₀_nhdsWithin_ne_zero {α : Type u_1} [NormedDivisionRing α] :
      Filter.Tendsto Inv.inv (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)
      source
      @[instance 100]
      instance NormedDivisionRing.to_hasContinuousInv₀ {α : Type u_1} [NormedDivisionRing α] :
      HasContinuousInv₀ α
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance NormedDivisionRing.to_topologicalDivisionRing {α : Type u_1} [NormedDivisionRing α] :
      TopologicalDivisionRing α

      A normed division ring is a topological division ring.

      Equations
      • ⋯ = ⋯
      source
      theorem IsOfFinOrder.norm_eq_one {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : IsOfFinOrder a) :
      ‖a‖ = 1
      source
      @[simp]
      theorem AddChar.norm_apply {α : Type u_1} [NormedDivisionRing α] {G : Type u_4} [AddLeftCancelMonoid G] [Finite G] (ψ : AddChar G α) (x : G) :
      ‖ψ x‖ = 1
      source
      theorem NormedField.denseRange_nnnorm (α : Type u_1) [DenselyNormedField α] :
      DenseRange nnnorm
      source
      theorem NNReal.lipschitzWith_sub :
      LipschitzWith 2 fun (p : NNReal × NNReal) => p.1 - p.2
      source
      instance Int.instNormedCommRing :
      NormedCommRing ℤ
      Equations
      source
      instance Int.instNormOneClass :
      NormOneClass ℤ
      Equations
      source
      instance Rat.instNormedField :
      NormedField ℚ
      Equations
      source
      instance Rat.instDenselyNormedField :
      DenselyNormedField ℚ
      Equations