Topological structure on EReal

We prove basic properties of the topology on EReal.

Main results

• Real.toEReal : ℝ → EReal is an open embedding
• ENNReal.toEReal : ℝ≥0∞ → EReal is a closed embedding
• The addition on EReal is continuous except at (⊥, ⊤) and at (⊤, ⊥).
• Negation is a homeomorphism on EReal.

Implementation

Most proofs are adapted from the corresponding proofs on ℝ≥0∞.

Real coercion

theorem EReal.isEmbedding_coe : Topology.IsEmbedding Real.toEReal

theorem EReal.isOpenEmbedding_coe : Topology.IsOpenEmbedding Real.toEReal

theorem EReal.tendsto_coe {α : Type u_2} {f : Filter α} {m : α → ℝ} {a : ℝ} : Filter.Tendsto (fun (a : α) => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)

theorem continuous_coe_real_ereal : Continuous Real.toEReal

theorem EReal.continuous_coe_iff {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} : (Continuous fun (a : α) => ↑(f a)) ↔ Continuous f

theorem EReal.nhds_coe {r : ℝ} : nhds ↑r = Filter.map Real.toEReal (nhds r)

theorem EReal.nhds_coe_coe {r p : ℝ} : nhds (↑r, ↑p) = Filter.map (fun (p : ℝ × ℝ) => (↑p.1, ↑p.2)) (nhds (r, p))

theorem EReal.tendsto_toReal {a : EReal} (ha : a ≠ ⊤) (h'a : a ≠ ⊥) : Filter.Tendsto toReal (nhds a) (nhds a.toReal)

theorem EReal.continuousOn_toReal : ContinuousOn toReal {⊥, ⊤}ᶜ

def EReal.neBotTopHomeomorphReal : ↑{⊥, ⊤}ᶜ ≃ₜ ℝ

The set of finite EReal numbers is homeomorphic to ℝ.

ENNReal coercion

theorem EReal.isEmbedding_coe_ennreal : Topology.IsEmbedding ENNReal.toEReal

theorem EReal.isClosedEmbedding_coe_ennreal : Topology.IsClosedEmbedding ENNReal.toEReal

theorem EReal.tendsto_coe_ennreal {α : Type u_2} {f : Filter α} {m : α → ENNReal} {a : ENNReal} : Filter.Tendsto (fun (a : α) => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)

theorem continuous_coe_ennreal_ereal : Continuous ENNReal.toEReal

theorem EReal.continuous_coe_ennreal_iff {α : Type u_1} [TopologicalSpace α] {f : α → ENNReal} : (Continuous fun (a : α) => ↑(f a)) ↔ Continuous f

Neighborhoods of infinity

theorem EReal.nhds_top : nhds ⊤ = ⨅ (a : EReal), ⨅ (_ : a ≠ ⊤), Filter.principal (Set.Ioi a)

theorem EReal.nhds_top_basis : (nhds ⊤).HasBasis (fun (x : ℝ) => True) fun (x : ℝ) => Set.Ioi ↑x

theorem EReal.nhds_top' : nhds ⊤ = ⨅ (a : ℝ), Filter.principal (Set.Ioi ↑a)

theorem EReal.mem_nhds_top_iff {s : Set EReal} : s ∈ nhds ⊤ ↔ ∃ (y : ℝ), Set.Ioi ↑y ⊆ s

theorem EReal.tendsto_nhds_top_iff_real {α : Type u_2} {m : α → EReal} {f : Filter α} : Filter.Tendsto m f (nhds ⊤) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a

theorem EReal.nhds_bot : nhds ⊥ = ⨅ (a : EReal), ⨅ (_ : a ≠ ⊥), Filter.principal (Set.Iio a)

theorem EReal.nhds_bot_basis : (nhds ⊥).HasBasis (fun (x : ℝ) => True) fun (x : ℝ) => Set.Iio ↑x

theorem EReal.nhds_bot' : nhds ⊥ = ⨅ (a : ℝ), Filter.principal (Set.Iio ↑a)

theorem EReal.mem_nhds_bot_iff {s : Set EReal} : s ∈ nhds ⊥ ↔ ∃ (y : ℝ), Set.Iio ↑y ⊆ s

theorem EReal.tendsto_nhds_bot_iff_real {α : Type u_2} {m : α → EReal} {f : Filter α} : Filter.Tendsto m f (nhds ⊥) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x

theorem EReal.nhdsWithin_top : nhdsWithin ⊤ {⊤}ᶜ = Filter.map Real.toEReal Filter.atTop

theorem EReal.nhdsWithin_bot : nhdsWithin ⊥ {⊥}ᶜ = Filter.map Real.toEReal Filter.atBot

@[simp]

theorem EReal.tendsto_coe_nhds_top_iff {α : Type u_1} {f : α → ℝ} {l : Filter α} : Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhds ⊤) ↔ Filter.Tendsto f l Filter.atTop

theorem EReal.tendsto_coe_atTop : Filter.Tendsto Real.toEReal Filter.atTop (nhds ⊤)

@[simp]

theorem EReal.tendsto_coe_nhds_bot_iff {α : Type u_1} {f : α → ℝ} {l : Filter α} : Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhds ⊥) ↔ Filter.Tendsto f l Filter.atBot

theorem EReal.tendsto_coe_atBot : Filter.Tendsto Real.toEReal Filter.atBot (nhds ⊥)

theorem EReal.tendsto_toReal_atTop : Filter.Tendsto toReal (nhdsWithin ⊤ {⊤}ᶜ) Filter.atTop

theorem EReal.tendsto_toReal_atBot : Filter.Tendsto toReal (nhdsWithin ⊥ {⊥}ᶜ) Filter.atBot

toENNReal

theorem EReal.continuous_toENNReal : Continuous toENNReal

theorem Continuous.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {f : α → EReal} (hf : Continuous f) : Continuous fun (x : α) => (f x).toENNReal

theorem ContinuousOn.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {s : Set α} {f : α → EReal} (hf : ContinuousOn f s) : ContinuousOn (fun (x : α) => (f x).toENNReal) s

theorem ContinuousWithinAt.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {f : α → EReal} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (fun (x : α) => (f x).toENNReal) s x

theorem ContinuousAt.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {f : α → EReal} {x : α} (hf : ContinuousAt f x) : ContinuousAt (fun (x : α) => (f x).toENNReal) x

Infs and Sups

theorem EReal.add_iInf_le_iInf_add {α : Type u_2} {u v : α → EReal} : (⨅ (x : α), u x) + ⨅ (x : α), v x ≤ ⨅ (x : α), (u + v) x

theorem EReal.iSup_add_le_add_iSup {α : Type u_2} {u v : α → EReal} : ⨆ (x : α), (u + v) x ≤ (⨆ (x : α), u x) + ⨆ (x : α), v x

Liminfs and Limsups

theorem EReal.liminf_neg {α : Type u_3} {f : Filter α} {v : α → EReal} : Filter.liminf (-v) f = -Filter.limsup v f

theorem EReal.limsup_neg {α : Type u_3} {f : Filter α} {v : α → EReal} : Filter.limsup (-v) f = -Filter.liminf v f

theorem EReal.le_liminf_add {α : Type u_3} {f : Filter α} {u v : α → EReal} : Filter.liminf u f + Filter.liminf v f ≤ Filter.liminf (u + v) f

theorem EReal.limsup_add_le {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.limsup u f ≠ ⊥ ∨ Filter.limsup v f ≠ ⊤) (h' : Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ ⊥) : Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f

theorem EReal.le_limsup_add {α : Type u_3} {f : Filter α} {u v : α → EReal} : Filter.limsup u f + Filter.liminf v f ≤ Filter.limsup (u + v) f

theorem EReal.liminf_add_le {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.limsup u f ≠ ⊥ ∨ Filter.liminf v f ≠ ⊤) (h' : Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ ⊥) : Filter.liminf (u + v) f ≤ Filter.limsup u f + Filter.liminf v f

theorem EReal.limsup_add_bot_of_ne_top {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.limsup u f = ⊥) (h' : Filter.limsup v f ≠ ⊤) : Filter.limsup (u + v) f = ⊥

theorem EReal.limsup_add_le_of_le {α : Type u_3} {f : Filter α} {u v : α → EReal} {a b : EReal} (ha : Filter.limsup u f < a) (hb : Filter.limsup v f ≤ b) : Filter.limsup (u + v) f ≤ a + b

theorem EReal.liminf_add_gt_of_gt {α : Type u_3} {f : Filter α} {u v : α → EReal} {a b : EReal} (ha : a < Filter.liminf u f) (hb : b < Filter.liminf v f) : a + b < Filter.liminf (u + v) f

theorem EReal.liminf_add_top_of_ne_bot {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.liminf u f = ⊤) (h' : Filter.liminf v f ≠ ⊥) : Filter.liminf (u + v) f = ⊤

theorem EReal.limsup_const_mul_of_nonneg_of_ne_top {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal} (h₁ : 0 ≤ c) (h₂ : c ≠ ⊤) : Filter.limsup (fun (x : α) => c * u x) f = c * Filter.limsup u f

theorem EReal.limsup_const_mul_of_nonpos_of_ne_bot {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal} (h₁ : c ≤ 0) (h₂ : c ≠ ⊥) : Filter.limsup (fun (x : α) => c * u x) f = c * Filter.liminf u f

theorem EReal.liminf_const_mul_of_nonneg_of_ne_top {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal} (h₁ : 0 ≤ c) (h₂ : c ≠ ⊤) : Filter.liminf (fun (x : α) => c * u x) f = c * Filter.liminf u f

theorem EReal.liminf_const_mul_of_nonpos_of_ne_bot {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal} (h₁ : c ≤ 0) (h₂ : c ≠ ⊥) : Filter.liminf (fun (x : α) => c * u x) f = c * Filter.limsup u f

theorem EReal.le_limsup_mul {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : ∃ᶠ (x : α) in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) : Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f

theorem EReal.limsup_mul_le {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : ∃ᶠ (x : α) in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) (h₁ : Filter.limsup u f ≠ 0 ∨ Filter.limsup v f ≠ ⊤) (h₂ : Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ 0) : Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f

theorem EReal.le_liminf_mul {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) : Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (u * v) f

theorem EReal.liminf_mul_le {α : Type u_3} {f : Filter α} {u v : α → EReal} [f.NeBot] (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) (h₁ : Filter.limsup u f ≠ 0 ∨ Filter.liminf v f ≠ ⊤) (h₂ : Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ 0) : Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f

Continuity of addition

theorem EReal.continuousAt_add_coe_coe (a b : ℝ) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (↑a, ↑b)

theorem EReal.continuousAt_add_top_coe (a : ℝ) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊤, ↑a)

theorem EReal.continuousAt_add_coe_top (a : ℝ) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (↑a, ⊤)

theorem EReal.continuousAt_add_top_top : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊤, ⊤)

theorem EReal.continuousAt_add_bot_coe (a : ℝ) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊥, ↑a)

theorem EReal.continuousAt_add_coe_bot (a : ℝ) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (↑a, ⊥)

theorem EReal.continuousAt_add_bot_bot : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊥, ⊥)

theorem EReal.continuousAt_add {p : EReal × EReal} (h : p.1 ≠ ⊤ ∨ p.2 ≠ ⊥) (h' : p.1 ≠ ⊥ ∨ p.2 ≠ ⊤) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) p

The addition on EReal is continuous except where it doesn't make sense (i.e., at (⊥, ⊤) and at (⊤, ⊥)).

theorem EReal.lowerSemicontinuous_add : LowerSemicontinuous fun (p : EReal × EReal) => p.1 + p.2

Continuity of multiplication

theorem EReal.continuousAt_mul {p : EReal × EReal} (h₁ : p.1 ≠ 0 ∨ p.2 ≠ ⊥) (h₂ : p.1 ≠ 0 ∨ p.2 ≠ ⊤) (h₃ : p.1 ≠ ⊥ ∨ p.2 ≠ 0) (h₄ : p.1 ≠ ⊤ ∨ p.2 ≠ 0) : ContinuousAt (fun (p : EReal × EReal) => p.1 * p.2) p

The multiplication on EReal is continuous except at indeterminacies (i.e. whenever one value is zero and the other infinite).

theorem EReal.tendsto_mul {a b : EReal} (h₁ : a ≠ 0 ∨ b ≠ ⊥) (h₂ : a ≠ 0 ∨ b ≠ ⊤) (h₃ : a ≠ ⊥ ∨ b ≠ 0) (h₄ : a ≠ ⊤ ∨ b ≠ 0) : Filter.Tendsto (fun (p : EReal × EReal) => p.1 * p.2) (nhds (a, b)) (nhds (a * b))

theorem EReal.Tendsto.mul {α : Type u_2} {f : Filter α} {ma mb : α → EReal} {a b : EReal} (hma : Filter.Tendsto ma f (nhds a)) (hmb : Filter.Tendsto mb f (nhds b)) (h₁ : a ≠ 0 ∨ b ≠ ⊥) (h₂ : a ≠ 0 ∨ b ≠ ⊤) (h₃ : a ≠ ⊥ ∨ b ≠ 0) (h₄ : a ≠ ⊤ ∨ b ≠ 0) : Filter.Tendsto (fun (x : α) => ma x * mb x) f (nhds (a * b))

theorem EReal.Tendsto.const_mul {α : Type u_2} {f : Filter α} {m : α → EReal} {a b : EReal} (hm : Filter.Tendsto m f (nhds b)) (h₁ : a ≠ ⊥ ∨ b ≠ 0) (h₂ : a ≠ ⊤ ∨ b ≠ 0) : Filter.Tendsto (fun (b : α) => a * m b) f (nhds (a * b))

theorem EReal.Tendsto.mul_const {α : Type u_2} {f : Filter α} {m : α → EReal} {a b : EReal} (hm : Filter.Tendsto m f (nhds a)) (h₁ : a ≠ 0 ∨ b ≠ ⊥) (h₂ : a ≠ 0 ∨ b ≠ ⊤) : Filter.Tendsto (fun (x : α) => m x * b) f (nhds (a * b))