Mathlib.Topology.Algebra.Ring.Real

Module docstring

{"# Topological algebra properties of ℝ

This file defines topological field/(semi)ring structures on the (extended) (nonnegative) reals and shows the algebraic operations are (uniformly) continuous.

It also includes a bit of more general topological theory of the reals, needed to define the structures and prove continuity. ","Instances for the following typeclasses are defined:

IsTopologicalSemiring ℝ≥0
ContinuousSub ℝ≥0
HasContinuousInv₀ ℝ≥0 (continuity of x⁻¹ away from 0)
ContinuousSMul ℝ≥0 α (whenever α has a continuous MulAction ℝ α)

Everything is inherited from the corresponding structures on the reals. "}

instNoncompactSpaceReal instance

: NoncompactSpace ℝ

Full source

instance : NoncompactSpace ℝ := Int.isClosedEmbedding_coe_real.noncompactSpace

Noncompactness of the Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a noncompact space.

Real.uniformContinuous_add theorem

: UniformContinuous fun p : ℝ × ℝ => p.1 + p.2

Full source

theorem Real.uniformContinuous_add : UniformContinuous fun p : ℝℝ × ℝ => p.1 + p.2 :=
  Metric.uniformContinuous_iff.2 fun _ε ε0 =>
    let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma abs ε0
    ⟨δ, δ0, fun _ _ h =>
      let ⟨h₁, h₂⟩ := max_lt_iff.1 h
      Hδ h₁ h₂⟩

Uniform Continuity of Real Addition

Informal description

The addition operation $(x, y) \mapsto x + y$ on the real numbers $\mathbb{R}$ is uniformly continuous.

Real.uniformContinuous_neg theorem

: UniformContinuous (@Neg.neg ℝ _)

Full source

theorem Real.uniformContinuous_neg : UniformContinuous (@Neg.neg ℝ _) :=
  Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨_, ε0, fun _ _ h => by simpa only [abs_sub_comm, Real.dist_eq, neg_sub_neg] using h⟩

Uniform Continuity of Real Negation

Informal description

The negation operation $x \mapsto -x$ on the real numbers $\mathbb{R}$ is uniformly continuous.

instIsUniformAddGroupReal instance

: IsUniformAddGroup ℝ

Full source

instance : IsUniformAddGroup ℝ :=
  IsUniformAddGroup.mk' Real.uniformContinuous_add Real.uniformContinuous_neg

Uniform Additive Group Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a uniform additive group, meaning the addition operation $+ : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$ and the negation operation $- : \mathbb{R} \to \mathbb{R}$ are uniformly continuous with respect to the uniform structure induced by the metric on $\mathbb{R}$.

Real.uniformContinuous_const_mul theorem

{x : ℝ} : UniformContinuous (x * ·)

Full source

theorem Real.uniformContinuous_const_mul {x : ℝ} : UniformContinuous (x * ·) :=
  uniformContinuous_of_continuousAt_zero (DistribMulAction.toAddMonoidHom ℝ x)
    (continuous_const_smul x).continuousAt

Uniform Continuity of Scalar Multiplication by a Fixed Real Number

Informal description

For any real number $x$, the function $y \mapsto x \cdot y$ is uniformly continuous on $\mathbb{R}$.

instIsTopologicalAddGroupReal instance

: IsTopologicalAddGroup ℝ

Full source

instance : IsTopologicalAddGroup ℝ := by infer_instance

The Topological Additive Group Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a topological additive group, meaning the addition operation $+ : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$ and the negation operation $- : \mathbb{R} \to \mathbb{R}$ are continuous with respect to the order topology on $\mathbb{R}$.

instIsTopologicalRingReal instance

: IsTopologicalRing ℝ

Full source

instance : IsTopologicalRing ℝ := inferInstance

The Topological Ring Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a topological ring, meaning the addition and multiplication operations are continuous with respect to the order topology on $\mathbb{R}$.

instIsTopologicalDivisionRingReal instance

: IsTopologicalDivisionRing ℝ

Full source

instance : IsTopologicalDivisionRing ℝ := inferInstance

Topological Division Ring Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ form a topological division ring, meaning they are equipped with a topology where the ring operations (addition and multiplication) are continuous, and the inversion operation $x \mapsto x^{-1}$ is continuous at every nonzero $x \in \mathbb{R}$.

EReal.instContinuousNeg instance

: ContinuousNeg EReal

Full source

instance : ContinuousNeg EReal := ⟨negOrderIso.continuous⟩

Continuity of Negation on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ are equipped with a continuous negation operation, where the map $x \mapsto -x$ is continuous with respect to the order topology on $\overline{\mathbb{R}}$.

NNReal.instIsTopologicalSemiring instance

: IsTopologicalSemiring ℝ≥0

Full source

instance : IsTopologicalSemiring ℝ≥0 where
  toContinuousAdd := continuousAdd_induced toRealHom
  toContinuousMul := continuousMul_induced toRealHom

Topological Semiring Structure on Nonnegative Reals

Informal description

The nonnegative real numbers $\mathbb{R}_{\geq 0}$ form a topological semiring, meaning the addition and multiplication operations are continuous with respect to the topology induced from $\mathbb{R}$.

NNReal.instContinuousSub instance

: ContinuousSub ℝ≥0

Full source

instance : ContinuousSub ℝ≥0 :=
  ⟨((continuous_coe.fst'.sub continuous_coe.snd').max continuous_const).subtype_mk _⟩

Continuous Subtraction on Nonnegative Real Numbers

Informal description

The nonnegative real numbers $\mathbb{R}_{\geq 0}$ are equipped with a continuous subtraction operation.

NNReal.instHasContinuousInv₀ instance

: HasContinuousInv₀ ℝ≥0

Full source

instance : HasContinuousInv₀ ℝ≥0 := inferInstance

Continuous Inversion on Nonzero Nonnegative Reals

Informal description

The nonnegative real numbers $\mathbb{R}_{\geq 0}$ have a continuous inversion operation at all nonzero points. That is, the function $x \mapsto x^{-1}$ is continuous on $\mathbb{R}_{\geq 0} \setminus \{0\}$.

NNReal.instContinuousSMulOfReal instance

[TopologicalSpace α] [MulAction ℝ α] [ContinuousSMul ℝ α] : ContinuousSMul ℝ≥0 α

Full source

instance [TopologicalSpace α] [MulAction ℝ α] [ContinuousSMul ℝ α] :
    ContinuousSMul ℝ≥0 α where
  continuous_smul := continuous_induced_dom.fst'.smul continuous_snd

Continuous Scalar Multiplication by Nonnegative Reals

Informal description

For any topological space $\alpha$ with a continuous scalar multiplication action by $\mathbb{R}$, the nonnegative real numbers $\mathbb{R}_{\geq 0}$ also induce a continuous scalar multiplication action on $\alpha$. This means that the scalar multiplication operation $\mathbb{R}_{\geq 0} \times \alpha \to \alpha$ is jointly continuous.

ENNReal.isEmbedding_coe theorem

: IsEmbedding ((↑) : ℝ≥0 → ℝ≥0∞)

Full source

theorem isEmbedding_coe : IsEmbedding ((↑) : ℝ≥0 → ℝ≥0∞) :=
  coe_strictMono.isEmbedding_of_ordConnected <| by rw [range_coe']; exact ordConnected_Iio

Topological Embedding of Nonnegative Reals into Extended Nonnegative Reals

Informal description

The canonical inclusion map $\iota \colon \mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ is a topological embedding, where $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equipped with the order topology.

ENNReal.tendsto_coe theorem

 {f : Filter α} {m : α → ℝ≥0} {a : ℝ≥0} : Tendsto (fun a => (m a : ℝ≥0∞)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a)

Full source

@[simp, norm_cast]
theorem tendsto_coe {f : Filter α} {m : α → ℝ≥0} {a : ℝ≥0} :
    TendstoTendsto (fun a => (m a : ℝ≥0∞)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a) :=
  isEmbedding_coe.tendsto_nhds_iff.symm

Limit Characterization of the Inclusion Map from Nonnegative Reals to Extended Nonnegative Reals

Informal description

Let $f$ be a filter on a type $\alpha$, $m \colon \alpha \to \mathbb{R}_{\geq 0}$ a function, and $a \in \mathbb{R}_{\geq 0}$. The composition $\lambda a, (m a : \mathbb{R}_{\geq 0} \cup \{\infty\})$ tends to the neighborhood filter of $a$ (as an element of $\mathbb{R}_{\geq 0} \cup \{\infty\}$) along $f$ if and only if $m$ tends to the neighborhood filter of $a$ (as an element of $\mathbb{R}_{\geq 0}$) along $f$. In other words: $$\lim_{f} (m : \mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}) = a \iff \lim_{f} m = a.$$

ENNReal.isOpenEmbedding_coe theorem

: IsOpenEmbedding ((↑) : ℝ≥0 → ℝ≥0∞)

Full source

theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℝ≥0 → ℝ≥0∞) :=
  ⟨isEmbedding_coe, by rw [range_coe']; exact isOpen_Iio⟩

Open Embedding Property of Nonnegative Reals in Extended Nonnegative Reals

Informal description

The canonical inclusion map $\iota \colon \mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ is an open topological embedding, where $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equipped with the order topology. This means that $\iota$ is injective, continuous, and maps open sets in $\mathbb{R}_{\geq 0}$ to open sets in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.nhds_coe_coe theorem

 {r p : ℝ≥0} : 𝓝 ((r : ℝ≥0∞), (p : ℝ≥0∞)) = (𝓝 (r, p)).map fun p : ℝ≥0 × ℝ≥0 => (↑p.1, ↑p.2)

Full source

theorem nhds_coe_coe {r p : ℝ≥0} :
    𝓝 ((r : ℝ≥0∞), (p : ℝ≥0∞)) = (𝓝 (r, p)).map fun p : ℝ≥0ℝ≥0 × ℝ≥0 => (↑p.1, ↑p.2) :=
  ((isOpenEmbedding_coe.prodMap isOpenEmbedding_coe).map_nhds_eq (r, p)).symm

Neighborhood Filter Preservation for Pairs in Extended Nonnegative Reals

Informal description

For any two nonnegative real numbers $r$ and $p$, the neighborhood filter of the pair $(r, p)$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the pushforward of the neighborhood filter of $(r, p)$ in $\mathbb{R}_{\geq 0} \times \mathbb{R}_{\geq 0}$ under the canonical inclusion map $(x, y) \mapsto (x, y)$.

ENNReal.instContinuousAdd instance

: ContinuousAdd ℝ≥0∞

Full source

instance : ContinuousAdd ℝ≥0∞ := by
  refine ⟨continuous_iff_continuousAt.2 ?_⟩
  rintro ⟨_ | a, b⟩
  · exact tendsto_nhds_top_mono' continuousAt_fst fun p => le_add_right le_rfl
  rcases b with (_ | b)
  · exact tendsto_nhds_top_mono' continuousAt_snd fun p => le_add_left le_rfl
  simp only [ContinuousAt, some_eq_coe, nhds_coe_coe, ← coe_add, tendsto_map'_iff,
    Function.comp_def, tendsto_coe, tendsto_add]

Continuity of Addition on Extended Nonnegative Reals

Informal description

The addition operation on the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is continuous with respect to the order topology.

ENNReal.instContinuousInv instance

: ContinuousInv ℝ≥0∞

Full source

instance : ContinuousInv ℝ≥0∞ := ⟨OrderIso.invENNReal.continuous⟩

Continuity of Inversion on Extended Nonnegative Reals

Informal description

The inversion operation $x \mapsto x^{-1}$ on the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is continuous with respect to the order topology. Here, the inversion is defined by: - $x^{-1} = \frac{1}{x}$ for $x \in \mathbb{R}_{>0}$, - $0^{-1} = \infty$, - $\infty^{-1} = 0$.