Normed fields

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

Some useful results that relate the topology of the normed field to the discrete topology include:

• discreteTopology_or_nontriviallyNormedField
• discreteTopology_of_bddAbove_range_norm

theorem Filter.Tendsto.zero_mul_isBoundedUnder_le {α : Type u_1} {ι : Type u_3} [NonUnitalSeminormedRing α] {f g : ι → α} {l : Filter ι} (hf : Tendsto f l (nhds 0)) (hg : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l ((fun (x : α) => ‖x‖) ∘ g)) : Tendsto (fun (x : ι) => f x * g x) l (nhds 0)

theorem Filter.isBoundedUnder_le_mul_tendsto_zero {α : Type u_1} {ι : Type u_3} [NonUnitalSeminormedRing α] {f g : ι → α} {l : Filter ι} (hf : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)) (hg : Tendsto g l (nhds 0)) : Tendsto (fun (x : ι) => f x * g x) l (nhds 0)

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

• Pi.nonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

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

• Pi.seminormedRing = SeminormedRing.mk ⋯ ⋯

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

• Pi.nonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

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

• Pi.normedRing = NormedRing.mk ⋯ ⋯

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

• Pi.nonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

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

• Pi.nonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

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

• Pi.seminormedCommRing = SeminormedCommRing.mk ⋯

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

• Pi.normedCommutativeRing = NormedCommRing.mk ⋯

@[instance 100]

instance NonUnitalSeminormedRing.toContinuousMul {α : Type u_1} [NonUnitalSeminormedRing α] : ContinuousMul α

@[instance 100]

instance NonUnitalSeminormedRing.toIsTopologicalRing {α : Type u_1} [NonUnitalSeminormedRing α] : IsTopologicalRing α

A seminormed ring is a topological ring.

instance SeparationQuotient.instNonUnitalNormedRing {α : Type u_1} [NonUnitalSeminormedRing α] : NonUnitalNormedRing (SeparationQuotient α)

Equations

• SeparationQuotient.instNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

instance SeparationQuotient.instNonUnitalNormedCommRing {α : Type u_1} [NonUnitalSeminormedCommRing α] : NonUnitalNormedCommRing (SeparationQuotient α)

Equations

• SeparationQuotient.instNonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

instance SeparationQuotient.instNormedRing {α : Type u_1} [SeminormedRing α] : NormedRing (SeparationQuotient α)

Equations

• SeparationQuotient.instNormedRing = NormedRing.mk ⋯ ⋯

instance SeparationQuotient.instNormedCommRing {α : Type u_1} [SeminormedCommRing α] : NormedCommRing (SeparationQuotient α)

Equations

• SeparationQuotient.instNormedCommRing = NormedCommRing.mk ⋯

instance SeparationQuotient.instNormOneClass {α : Type u_1} [SeminormedAddCommGroup α] [One α] [NormOneClass α] : NormOneClass (SeparationQuotient α)

theorem antilipschitzWith_mul_left {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : AntilipschitzWith ‖a‖₊⁻¹ fun (x : α) => a * x

theorem antilipschitzWith_mul_right {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : AntilipschitzWith ‖a‖₊⁻¹ fun (x : α) => x * a

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

• DilationEquiv.mulLeft a ha = { toEquiv := Equiv.mulLeft₀ a ha, edist_eq' := ⋯ }

@[simp]

theorem DilationEquiv.mulLeft_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) : (mulLeft a ha) x = a * x

@[simp]

theorem DilationEquiv.mulLeft_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) : (mulLeft a ha).symm x = a⁻¹ * x

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

• DilationEquiv.mulRight a ha = { toEquiv := Equiv.mulRight₀ a ha, edist_eq' := ⋯ }

@[simp]

theorem DilationEquiv.mulRight_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) : (mulRight a ha) x = x * a

@[simp]

theorem DilationEquiv.mulRight_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) : (mulRight a ha).symm x = x * a⁻¹

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Filter.tendsto_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : 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.

theorem Filter.tendsto_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : 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.

@[simp]

theorem Filter.inv_cobounded₀ {α : Type u_1} [NormedDivisionRing α] : (Bornology.cobounded α)⁻¹ = nhdsWithin 0 {0}ᶜ

@[simp]

theorem Filter.inv_nhdsWithin_ne_zero {α : Type u_1} [NormedDivisionRing α] : (nhdsWithin 0 {0}ᶜ)⁻¹ = Bornology.cobounded α

theorem Filter.tendsto_inv₀_cobounded' {α : Type u_1} [NormedDivisionRing α] : Tendsto Inv.inv (Bornology.cobounded α) (nhdsWithin 0 {0}ᶜ)

theorem Filter.tendsto_inv₀_cobounded {α : Type u_1} [NormedDivisionRing α] : Tendsto Inv.inv (Bornology.cobounded α) (nhds 0)

theorem Filter.tendsto_inv₀_nhdsWithin_ne_zero {α : Type u_1} [NormedDivisionRing α] : Tendsto Inv.inv (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)

@[instance 100]

instance NormedDivisionRing.to_hasContinuousInv₀ {α : Type u_1} [NormedDivisionRing α] : HasContinuousInv₀ α

@[instance 100]

instance NormedDivisionRing.to_topologicalDivisionRing {α : Type u_1} [NormedDivisionRing α] : TopologicalDivisionRing α

A normed division ring is a topological division ring.

theorem IsOfFinOrder.norm_eq_one {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : IsOfFinOrder a) : ‖a‖ = 1

@[simp]

theorem AddChar.norm_apply {α : Type u_1} [NormedDivisionRing α] {G : Type u_4} [AddLeftCancelMonoid G] [Finite G] (ψ : AddChar G α) (x : G) : ‖ψ x‖ = 1

theorem NormedField.tendsto_norm_inv_nhdsNE_zero_atTop {α : Type u_1} [NormedDivisionRing α] : Filter.Tendsto (fun (x : α) => ‖x⁻¹‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop

@[deprecated NormedField.tendsto_norm_inv_nhdsNE_zero_atTop (since := "2024-12-22")]

theorem NormedField.tendsto_norm_inverse_nhdsWithin_0_atTop {α : Type u_1} [NormedDivisionRing α] : Filter.Tendsto (fun (x : α) => ‖x⁻¹‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop

Alias of NormedField.tendsto_norm_inv_nhdsNE_zero_atTop.

theorem NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop {α : Type u_1} [NormedDivisionRing α] {m : ℤ} (hm : m < 0) : Filter.Tendsto (fun (x : α) => ‖x ^ m‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop

@[deprecated NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop (since := "2024-12-22")]

theorem NormedField.tendsto_norm_zpow_nhdsWithin_0_atTop {α : Type u_1} [NormedDivisionRing α] {m : ℤ} (hm : m < 0) : Filter.Tendsto (fun (x : α) => ‖x ^ m‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop

Alias of NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop.

theorem NormedField.discreteTopology_or_nontriviallyNormedField (𝕜 : Type u_4) [h : NormedField 𝕜] : DiscreteTopology 𝕜 ∨ Nonempty { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }

A normed field is either nontrivially normed or has a discrete topology. In the discrete topology case, all the norms are 1, by norm_eq_one_iff_ne_zero_of_discrete. The nontrivially normed field instance is provided by a subtype with a proof that the forgetful inheritance to the existing NormedField instance is definitionally true. This allows one to have the new NontriviallyNormedField instance without data clashes.

theorem NormedField.discreteTopology_of_bddAbove_range_norm {𝕜 : Type u_4} [NormedField 𝕜] (h : BddAbove (Set.range fun (k : 𝕜) => ‖k‖)) : DiscreteTopology 𝕜

theorem NormedField.denseRange_nnnorm (α : Type u_1) [DenselyNormedField α] : DenseRange nnnorm

@[simp]

theorem NormedField.continuousAt_zpow {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {n : ℤ} {x : 𝕜} : ContinuousAt (fun (x : 𝕜) => x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n

@[simp]

theorem NormedField.continuousAt_inv {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {x : 𝕜} : ContinuousAt Inv.inv x ↔ x ≠ 0

theorem NNReal.lipschitzWith_sub : LipschitzWith 2 fun (p : NNReal × NNReal) => p.1 - p.2

instance Int.instNormedCommRing : NormedCommRing ℤ

Equations

• Int.instNormedCommRing = NormedCommRing.mk ⋯

instance Int.instNormOneClass : NormOneClass ℤ

instance Rat.instNormedField : NormedField ℚ

Equations

• Rat.instNormedField = NormedField.mk ⋯ Rat.instNormedField.proof_1

instance Rat.instDenselyNormedField : DenselyNormedField ℚ

Equations

• Rat.instDenselyNormedField = DenselyNormedField.mk Rat.instDenselyNormedField.proof_1

theorem NormedField.completeSpace_iff_isComplete_closedBall {K : Type u_4} [NormedField K] : CompleteSpace K ↔ IsComplete (Metric.closedBall 0 1)