Mathlib.Topology.Instances.EReal.Lemmas

EReal.isEmbedding_coe theorem

: IsEmbedding ((↑) : ℝ → EReal)

Full source

theorem isEmbedding_coe : IsEmbedding ((↑) : ℝ → EReal) :=
  coe_strictMono.isEmbedding_of_ordConnected <| by rw [range_coe_eq_Ioo]; exact ordConnected_Ioo

Topological Embedding of Reals into Extended Reals

Informal description

The canonical embedding from the real numbers $\mathbb{R}$ to the extended real numbers $\overline{\mathbb{R}}$ is an embedding in the topological sense. That is, the map $x \mapsto x$ is both injective and induces a homeomorphism between $\mathbb{R}$ and its image in $\overline{\mathbb{R}}$ with the subspace topology.

EReal.isOpenEmbedding_coe theorem

: IsOpenEmbedding ((↑) : ℝ → EReal)

Full source

theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℝ → EReal) :=
  ⟨isEmbedding_coe, by simp only [range_coe_eq_Ioo, isOpen_Ioo]⟩

Open Embedding of Reals into Extended Reals

Informal description

The canonical embedding from the real numbers $\mathbb{R}$ to the extended real numbers $\overline{\mathbb{R}}$ is an open embedding. That is, the map $x \mapsto x$ is both injective, continuous, and maps open sets in $\mathbb{R}$ to open sets in $\overline{\mathbb{R}}$ (with respect to the subspace topology).

EReal.tendsto_coe theorem

 {α : Type*} {f : Filter α} {m : α → ℝ} {a : ℝ} : Tendsto (fun a => (m a : EReal)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a)

Full source

@[norm_cast]
theorem tendsto_coe {α : Type*} {f : Filter α} {m : α → ℝ} {a : ℝ} :
    TendstoTendsto (fun a => (m a : EReal)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a) :=
  isEmbedding_coe.tendsto_nhds_iff.symm

Convergence of Real-Valued Functions via Extended Real Embedding

Informal description

For any type $\alpha$, filter $f$ on $\alpha$, function $m \colon \alpha \to \mathbb{R}$, and real number $a$, the function $m$ tends to $a$ with respect to the filter $f$ if and only if the composition of $m$ with the canonical embedding $\mathbb{R} \hookrightarrow \overline{\mathbb{R}}$ tends to the embedded value of $a$ in $\overline{\mathbb{R}}$ with respect to the same filter $f$.

continuous_coe_real_ereal theorem

: Continuous ((↑) : ℝ → EReal)

Full source

theorem _root_.continuous_coe_real_ereal : Continuous ((↑) : ℝ → EReal) :=
  isEmbedding_coe.continuous

Continuity of the Real-to-Extended-Real Embedding

Informal description

The canonical embedding from the real numbers $\mathbb{R}$ to the extended real numbers $\overline{\mathbb{R}}$, given by $x \mapsto x$, is continuous with respect to the order topology on $\overline{\mathbb{R}}$.

EReal.continuous_coe_iff theorem

{f : α → ℝ} : (Continuous fun a => (f a : EReal)) ↔ Continuous f

Full source

theorem continuous_coe_iff {f : α → ℝ} : (Continuous fun a => (f a : EReal)) ↔ Continuous f :=
  isEmbedding_coe.continuous_iff.symm

Continuity of Real-Valued Functions via Extended Real Embedding

Informal description

For any function $f \colon \alpha \to \mathbb{R}$, the composition of $f$ with the canonical embedding $\mathbb{R} \to \overline{\mathbb{R}}$ is continuous if and only if $f$ is continuous. In other words, the map $f$ is continuous precisely when its extension to the extended reals is continuous.

EReal.nhds_coe theorem

{r : ℝ} : 𝓝 (r : EReal) = (𝓝 r).map (↑)

Full source

theorem nhds_coe {r : ℝ} : 𝓝 (r : EReal) = (𝓝 r).map (↑) :=
  (isOpenEmbedding_coe.map_nhds_eq r).symm

Neighborhood Filter of Real Numbers in Extended Reals via Canonical Embedding

Informal description

For any real number $r$, the neighborhood filter of $r$ in the extended real numbers $\overline{\mathbb{R}}$ is the image under the canonical embedding $\mathbb{R} \to \overline{\mathbb{R}}$ of the neighborhood filter of $r$ in $\mathbb{R}$. In other words, $\mathcal{N}(r : \overline{\mathbb{R}}) = (\mathcal{N}(r)).\text{map}(x \mapsto x)$.

EReal.nhds_coe_coe theorem

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

Full source

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

Neighborhood Filter of Real Pair in Extended Reals via Canonical Embedding

Informal description

For any real numbers $r$ and $p$, the neighborhood filter of the pair $(r, p)$ in the extended real numbers $\overline{\mathbb{R}} \times \overline{\mathbb{R}}$ is equal to the image under the canonical embedding of the neighborhood filter of $(r, p)$ in $\mathbb{R} \times \mathbb{R}$. In other words, $\mathcal{N}((r, p)) = \text{map} \, (\lambda (x, y). (x, y)) \, \mathcal{N}((r, p))$.

EReal.tendsto_toReal theorem

{a : EReal} (ha : a ≠ ⊤) (h'a : a ≠ ⊥) : Tendsto EReal.toReal (𝓝 a) (𝓝 a.toReal)

Full source

theorem tendsto_toReal {a : EReal} (ha : a ≠ ⊤) (h'a : a ≠ ⊥) :
    Tendsto EReal.toReal (𝓝 a) (𝓝 a.toReal) := by
  lift a to ℝ using ⟨ha, h'a⟩
  rw [nhds_coe, tendsto_map'_iff]
  exact tendsto_id

Continuity of the Extended Real to Real Conversion at Finite Points

Informal description

For any extended real number $a \in \overline{\mathbb{R}}$ such that $a \neq \top$ and $a \neq \bot$, the function $\text{toReal} : \overline{\mathbb{R}} \to \mathbb{R}$ is continuous at $a$. Specifically, the limit of $\text{toReal}(x)$ as $x$ approaches $a$ in $\overline{\mathbb{R}}$ is equal to $\text{toReal}(a)$ in $\mathbb{R}$.

EReal.continuousOn_toReal theorem

: ContinuousOn EReal.toReal ({⊥, ⊤}ᶜ : Set EReal)

Full source

theorem continuousOn_toReal : ContinuousOn EReal.toReal ({⊥, ⊤}{⊥, ⊤}ᶜ : Set EReal) := fun _a ha =>
  ContinuousAt.continuousWithinAt (tendsto_toReal (mt Or.inr ha) (mt Or.inl ha))

Continuity of Extended Real to Real Conversion on Finite Points

Informal description

The function $\text{toReal} : \overline{\mathbb{R}} \to \mathbb{R}$ is continuous on the set of finite extended real numbers, i.e., on $\overline{\mathbb{R}} \setminus \{\bot, \top\}$.

EReal.neBotTopHomeomorphReal definition

: ({⊥, ⊤}ᶜ : Set EReal) ≃ₜ ℝ

Full source

/-- The set of finite `EReal` numbers is homeomorphic to `ℝ`. -/
def neBotTopHomeomorphReal : ({⊥, ⊤}ᶜ : Set EReal) ≃ₜ ℝ where
  toEquiv := neTopBotEquivReal
  continuous_toFun := continuousOn_iff_continuous_restrict.1 continuousOn_toReal
  continuous_invFun := continuous_coe_real_ereal.subtype_mk _

Homeomorphism between finite extended reals and reals

Informal description

The set of finite extended real numbers (i.e., $\overline{\mathbb{R}} \setminus \{\bot, \top\}$) is homeomorphic to $\mathbb{R}$. The homeomorphism is given by the restriction of the canonical embedding $\mathbb{R} \to \overline{\mathbb{R}}$ and its inverse, which maps finite extended reals to their corresponding real values.

EReal.isEmbedding_coe_ennreal theorem

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

Full source

theorem isEmbedding_coe_ennreal : IsEmbedding ((↑) : ℝ≥0∞ → EReal) :=
  coe_ennreal_strictMono.isEmbedding_of_ordConnected <| by
    rw [range_coe_ennreal]; exact ordConnected_Ici

Embedding of Extended Non-Negative Reals into Extended Reals

Informal description

The canonical embedding from the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ to the extended real numbers $\overline{\mathbb{R}}$ is a topological embedding. That is, the subspace topology induced by this embedding coincides with the order topology on $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

EReal.isClosedEmbedding_coe_ennreal theorem

: IsClosedEmbedding ((↑) : ℝ≥0∞ → EReal)

Full source

theorem isClosedEmbedding_coe_ennreal : IsClosedEmbedding ((↑) : ℝ≥0∞ → EReal) :=
  ⟨isEmbedding_coe_ennreal, by rw [range_coe_ennreal]; exact isClosed_Ici⟩

Closed Embedding of Extended Non-Negative Reals into Extended Reals

Informal description

The canonical embedding from the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ to the extended real numbers $\overline{\mathbb{R}}$ is a closed topological embedding. That is, the subspace topology induced by this embedding coincides with the order topology on $\mathbb{R}_{\geq 0} \cup \{\infty\}$, and the image of any closed set under this embedding is closed in $\overline{\mathbb{R}}$.

EReal.tendsto_coe_ennreal theorem

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

Full source

@[norm_cast]
theorem tendsto_coe_ennreal {α : Type*} {f : Filter α} {m : α → ℝ≥0∞} {a : ℝ≥0∞} :
    TendstoTendsto (fun a => (m a : EReal)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a) :=
  isEmbedding_coe_ennreal.tendsto_nhds_iff.symm

Limit Preservation under Embedding of Extended Non-Negative Reals into Extended Reals

Informal description

For any type $\alpha$, filter $f$ on $\alpha$, function $m : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, and extended non-negative real number $a$, the limit of the composition of $m$ with the embedding $\mathbb{R}_{\geq 0} \cup \{\infty\} \hookrightarrow \overline{\mathbb{R}}$ tends to the embedded value of $a$ in $\overline{\mathbb{R}}$ if and only if the limit of $m$ tends to $a$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

continuous_coe_ennreal_ereal theorem

: Continuous ((↑) : ℝ≥0∞ → EReal)

Full source

theorem _root_.continuous_coe_ennreal_ereal : Continuous ((↑) : ℝ≥0∞ → EReal) :=
  isEmbedding_coe_ennreal.continuous

Continuity of the Embedding from Extended Non-Negative Reals to Extended Reals

Informal description

The canonical embedding from the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ to the extended real numbers $\overline{\mathbb{R}}$ is continuous.

EReal.continuous_coe_ennreal_iff theorem

{f : α → ℝ≥0∞} : (Continuous fun a => (f a : EReal)) ↔ Continuous f

Full source

theorem continuous_coe_ennreal_iff {f : α → ℝ≥0∞} :
    (Continuous fun a => (f a : EReal)) ↔ Continuous f :=
  isEmbedding_coe_ennreal.continuous_iff.symm

Continuity Criterion for Extended Non-Negative Real-Valued Functions via Embedding

Informal description

For any function $f \colon \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, the composition of $f$ with the canonical embedding $\mathbb{R}_{\geq 0} \cup \{\infty\} \hookrightarrow \overline{\mathbb{R}}$ is continuous if and only if $f$ is continuous.

EReal.nhds_top theorem

: 𝓝 (⊤ : EReal) = ⨅ (a) (_ : a ≠ ⊤), 𝓟 (Ioi a)

Full source

theorem nhds_top : 𝓝 (⊤ : EReal) = ⨅ (a) (_ : a ≠ ⊤), 𝓟 (Ioi a) :=
  nhds_top_order.trans <| by simp only [lt_top_iff_ne_top]

Neighborhood Filter at Infinity in Extended Real Numbers

Informal description

The neighborhood filter at $\top$ (positive infinity) in the extended real numbers $\overline{\mathbb{R}}$ is equal to the infimum over all $a \neq \top$ of the principal filters generated by the open intervals $(a, \infty)$.

EReal.nhds_top_basis theorem

: (𝓝 (⊤ : EReal)).HasBasis (fun _ : ℝ ↦ True) (Ioi ·)

Full source

nonrec theorem nhds_top_basis : (𝓝 (⊤ : EReal)).HasBasis (fun _ : ℝ ↦ True) (Ioi ·) := by
  refine (nhds_top_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, coe_lt_top _, Subset.rfl⟩
  rcases exists_rat_btwn_of_lt hx with ⟨y, hxy, -⟩
  exact ⟨_, trivial, Ioi_subset_Ioi hxy.le⟩

Basis for Neighborhoods at Infinity in Extended Real Numbers

Informal description

The neighborhood filter at $\top$ (positive infinity) in the extended real numbers $\overline{\mathbb{R}}$ has a basis consisting of all right-infinite open intervals $(a, \infty)$ where $a$ is a real number.

EReal.nhds_top' theorem

: 𝓝 (⊤ : EReal) = ⨅ a : ℝ, 𝓟 (Ioi ↑a)

Full source

theorem nhds_top' : 𝓝 (⊤ : EReal) = ⨅ a : ℝ, 𝓟 (Ioi ↑a) := nhds_top_basis.eq_iInf

Neighborhood Filter Characterization at Positive Infinity in Extended Real Numbers

Informal description

The neighborhood filter at positive infinity $\top$ in the extended real numbers $\overline{\mathbb{R}}$ is equal to the infimum over all real numbers $a$ of the principal filters generated by the open intervals $(a, \infty)$, where $a$ is considered as an element of $\overline{\mathbb{R}}$ via the canonical embedding.

EReal.mem_nhds_top_iff theorem

{s : Set EReal} : s ∈ 𝓝 (⊤ : EReal) ↔ ∃ y : ℝ, Ioi (y : EReal) ⊆ s

Full source

theorem mem_nhds_top_iff {s : Set EReal} : s ∈ 𝓝 (⊤ : EReal)s ∈ 𝓝 (⊤ : EReal) ↔ ∃ y : ℝ, Ioi (y : EReal) ⊆ s :=
  nhds_top_basis.mem_iff.trans <| by simp only [true_and]

Characterization of Neighborhoods at Positive Infinity in Extended Real Numbers

Informal description

A subset $s$ of the extended real numbers $\overline{\mathbb{R}}$ is a neighborhood of $\top$ (positive infinity) if and only if there exists a real number $y$ such that the open interval $(y, \infty)$ is contained in $s$.

EReal.tendsto_nhds_top_iff_real theorem

{α : Type*} {m : α → EReal} {f : Filter α} : Tendsto m f (𝓝 ⊤) ↔ ∀ x : ℝ, ∀ᶠ a in f, ↑x < m a

Full source

theorem tendsto_nhds_top_iff_real {α : Type*} {m : α → EReal} {f : Filter α} :
    TendstoTendsto m f (𝓝 ⊤) ↔ ∀ x : ℝ, ∀ᶠ a in f, ↑x < m a :=
  nhds_top_basis.tendsto_right_iff.trans <| by simp only [true_implies, mem_Ioi]

Characterization of Convergence to Positive Infinity in Extended Reals

Informal description

A function $m : \alpha \to \overline{\mathbb{R}}$ tends to $\top$ (positive infinity) in the filter $f$ if and only if for every real number $x$, the set $\{a \in \alpha \mid x < m(a)\}$ is eventually in $f$.

EReal.nhds_bot theorem

: 𝓝 (⊥ : EReal) = ⨅ (a) (_ : a ≠ ⊥), 𝓟 (Iio a)

Full source

theorem nhds_bot : 𝓝 (⊥ : EReal) = ⨅ (a) (_ : a ≠ ⊥), 𝓟 (Iio a) :=
  nhds_bot_order.trans <| by simp only [bot_lt_iff_ne_bot]

Neighborhood Filter at $-\infty$ in Extended Real Numbers

Informal description

The neighborhood filter at $-\infty$ in the extended real numbers $\overline{\mathbb{R}}$ is equal to the infimum over all $a \neq -\infty$ of the principal filters generated by the left-infinite right-open intervals $(-\infty, a)$.

EReal.nhds_bot_basis theorem

: (𝓝 (⊥ : EReal)).HasBasis (fun _ : ℝ ↦ True) (Iio ·)

Full source

theorem nhds_bot_basis : (𝓝 (⊥ : EReal)).HasBasis (fun _ : ℝ ↦ True) (Iio ·) := by
  refine (_root_.nhds_bot_basis (α := EReal)).to_hasBasis (fun x hx => ?_)
    fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩
  rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩
  exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩

Basis for Neighborhoods at $-\infty$ in Extended Reals

Informal description

The neighborhood filter at $-\infty$ in the extended real numbers $\overline{\mathbb{R}}$ has a basis consisting of all left-infinite right-open intervals $(-\infty, a)$ where $a$ is a real number.

EReal.nhds_bot' theorem

: 𝓝 (⊥ : EReal) = ⨅ a : ℝ, 𝓟 (Iio ↑a)

Full source

theorem nhds_bot' : 𝓝 (⊥ : EReal) = ⨅ a : ℝ, 𝓟 (Iio ↑a) :=
  nhds_bot_basis.eq_iInf

Neighborhood Filter at $-\infty$ as Infimum of Principal Filters

Informal description

The neighborhood filter at $-\infty$ in the extended real numbers $\overline{\mathbb{R}}$ is equal to the infimum over all real numbers $a$ of the principal filters generated by the left-infinite intervals $(-\infty, a]$.

EReal.mem_nhds_bot_iff theorem

{s : Set EReal} : s ∈ 𝓝 (⊥ : EReal) ↔ ∃ y : ℝ, Iio (y : EReal) ⊆ s

Full source

theorem mem_nhds_bot_iff {s : Set EReal} : s ∈ 𝓝 (⊥ : EReal)s ∈ 𝓝 (⊥ : EReal) ↔ ∃ y : ℝ, Iio (y : EReal) ⊆ s :=
  nhds_bot_basis.mem_iff.trans <| by simp only [true_and]

Characterization of Neighborhoods at $-\infty$ in Extended Reals

Informal description

A subset $s$ of the extended real numbers $\overline{\mathbb{R}}$ is a neighborhood of $-\infty$ if and only if there exists a real number $y$ such that the left-infinite interval $(-\infty, y)$ is contained in $s$.

EReal.tendsto_nhds_bot_iff_real theorem

{α : Type*} {m : α → EReal} {f : Filter α} : Tendsto m f (𝓝 ⊥) ↔ ∀ x : ℝ, ∀ᶠ a in f, m a < x

Full source

theorem tendsto_nhds_bot_iff_real {α : Type*} {m : α → EReal} {f : Filter α} :
    TendstoTendsto m f (𝓝 ⊥) ↔ ∀ x : ℝ, ∀ᶠ a in f, m a < x :=
  nhds_bot_basis.tendsto_right_iff.trans <| by simp only [true_implies, mem_Iio]

Characterization of Convergence to $-\infty$ in Extended Reals

Informal description

Let $\alpha$ be a type, $m : \alpha \to \overline{\mathbb{R}}$ be a function, and $f$ be a filter on $\alpha$. The function $m$ tends to $-\infty$ along the filter $f$ if and only if for every real number $x$, the set $\{a \in \alpha \mid m(a) < x\}$ is eventually in $f$.

EReal.nhdsWithin_top theorem

: 𝓝[≠] (⊤ : EReal) = (atTop).map Real.toEReal

Full source

lemma nhdsWithin_top : 𝓝[≠] (⊤ : EReal) = (atTop).map Real.toEReal := by
  apply (nhdsWithin_hasBasis nhds_top_basis_Ici _).ext (atTop_basis.map Real.toEReal)
  · simp only [EReal.image_coe_Ici, true_and]
    intro x hx
    by_cases hx_bot : x = ⊥
    · simp [hx_bot]
    lift x to ℝ using ⟨hx.ne_top, hx_bot⟩
    refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
    simp [h1, h2.ne_top]
  · simp only [EReal.image_coe_Ici, true_implies]
    refine fun x ↦ ⟨x, ⟨EReal.coe_lt_top x, fun x ⟨(h1 : _ ≤ x), h2⟩ ↦ ?_⟩⟩
    simp [h1, Ne.lt_top' fun a ↦ h2 a.symm]

Neighborhoods of Infinity in Extended Reals: $\mathcal{N}_{\neq}(\top) = \text{Real.toEReal}_*(\text{atTop})$

Informal description

The neighborhood filter of $\top$ (positive infinity) in the extended real numbers $\overline{\mathbb{R}}$, restricted to the punctured neighborhood (excluding $\top$ itself), is equal to the image under the embedding $\mathbb{R} \to \overline{\mathbb{R}}$ of the filter of neighborhoods of $+\infty$ in $\mathbb{R}$.

EReal.nhdsWithin_bot theorem

: 𝓝[≠] (⊥ : EReal) = (atBot).map Real.toEReal

Full source

lemma nhdsWithin_bot : 𝓝[≠] (⊥ : EReal) = (atBot).map Real.toEReal := by
  apply (nhdsWithin_hasBasis nhds_bot_basis_Iic _).ext (atBot_basis.map Real.toEReal)
  · simp only [EReal.image_coe_Iic, Set.subset_compl_singleton_iff, Set.mem_Ioc, lt_self_iff_false,
      bot_le, and_true, not_false_eq_true, true_and]
    intro x hx
    by_cases hx_top : x = ⊤
    · simp [hx_top]
    lift x to ℝ using ⟨hx_top, hx.ne_bot⟩
    refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
    simp [h2, h1.ne_bot]
  · simp only [EReal.image_coe_Iic, true_implies]
    refine fun x ↦ ⟨x, ⟨EReal.bot_lt_coe x, fun x ⟨(h1 : x ≤ _), h2⟩ ↦ ?_⟩⟩
    simp [h1, Ne.bot_lt' fun a ↦ h2 a.symm]

Punctured Neighborhood Characterization at $-\infty$ in Extended Reals

Informal description

The punctured neighborhood filter around $-\infty$ in the extended real numbers $\overline{\mathbb{R}}$ (excluding $-\infty$ itself) is equal to the image under the embedding $\mathbb{R} \to \overline{\mathbb{R}}$ of the filter of neighborhoods of $-\infty$ in $\mathbb{R}$.

EReal.tendsto_toReal_atTop theorem

: Tendsto EReal.toReal (𝓝[≠] ⊤) atTop

Full source

lemma tendsto_toReal_atTop : Tendsto EReal.toReal (𝓝[≠] ⊤) atTop := by
  rw [nhdsWithin_top, tendsto_map'_iff]
  exact tendsto_id

Limit Behavior of Extended Real to Real Conversion at Positive Infinity

Informal description

The function `EReal.toReal`, which maps extended real numbers to real numbers (with `⊤` and `⊥` mapped to some appropriate values), tends to $+\infty$ as its argument approaches $\top$ (positive infinity) within the punctured neighborhood (excluding $\top$ itself).

EReal.tendsto_toReal_atBot theorem

: Tendsto EReal.toReal (𝓝[≠] ⊥) atBot

Full source

lemma tendsto_toReal_atBot : Tendsto EReal.toReal (𝓝[≠] ⊥) atBot := by
  rw [nhdsWithin_bot, tendsto_map'_iff]
  exact tendsto_id

Limit of `toReal` at $-\infty$ in Extended Reals is $-\infty$

Informal description

The function `EReal.toReal`, which maps extended real numbers to real numbers (sending $-\infty$ and $+\infty$ to some fixed values), tends to $-\infty$ as its argument approaches $-\infty$ in the punctured neighborhood filter (i.e., excluding $-\infty$ itself).

EReal.continuous_toENNReal theorem

: Continuous EReal.toENNReal

Full source

lemma continuous_toENNReal : Continuous EReal.toENNReal := by
  refine continuous_iff_continuousAt.mpr fun x ↦ ?_
  by_cases h_top : x = ⊤
  · simp only [ContinuousAt, h_top, toENNReal_top]
    refine ENNReal.tendsto_nhds_top fun n ↦ ?_
    filter_upwards [eventually_gt_nhds (coe_lt_top n)] with y hy
    exact toENNReal_coe (x := n) ▸ toENNReal_lt_toENNReal (coe_ennreal_nonneg _) hy
  refine ContinuousOn.continuousAt ?_ (compl_singleton_mem_nhds_iff.mpr h_top)
  refine (continuousOn_of_forall_continuousAt fun x hx ↦ ?_).congr (fun _ h ↦ toENNReal_of_ne_top h)
  by_cases h_bot : x = ⊥
  · refine tendsto_nhds_of_eventually_eq ?_
    rw [h_bot, nhds_bot_basis.eventually_iff]
    simp [toReal_bot, ENNReal.ofReal_zero, ENNReal.ofReal_eq_zero, true_and]
    exact ⟨0, fun _ hx ↦ toReal_nonpos hx.le⟩
  refine ENNReal.continuous_ofReal.continuousAt.comp' <| continuousOn_toReal.continuousAt
    <| (toFinite _).isClosed.compl_mem_nhds ?_
  simp_all only [mem_compl_iff, mem_singleton_iff, mem_insert_iff, or_self, not_false_eq_true]

Continuity of the Extended Real to Extended Non-Negative Real Function

Informal description

The function $\text{toENNReal} : \overline{\mathbb{R}} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, which maps extended real numbers to extended non-negative real numbers, is continuous with respect to the order topologies on both spaces.

Continuous.ereal_toENNReal theorem

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

Full source

@[fun_prop]
lemma _root_.Continuous.ereal_toENNReal {α : Type*} [TopologicalSpace α] {f : α → EReal}
    (hf : Continuous f) :
    Continuous fun x => (f x).toENNReal :=
  continuous_toENNReal.comp hf

Continuity of Composition with Extended Real to Extended Non-Negative Real Function

Informal description

Let $\alpha$ be a topological space and $f : \alpha \to \overline{\mathbb{R}}$ be a continuous function. Then the composition $\text{toENNReal} \circ f : \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, defined by $x \mapsto \text{toENNReal}(f(x))$, is also continuous.

ContinuousOn.ereal_toENNReal theorem

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

Full source

@[fun_prop]
lemma _root_.ContinuousOn.ereal_toENNReal {α : Type*} [TopologicalSpace α] {s : Set α}
    {f : α → EReal} (hf : ContinuousOn f s) :
    ContinuousOn (fun x => (f x).toENNReal) s :=
  continuous_toENNReal.comp_continuousOn hf

Continuity of Extended Real to Non-Negative Extended Real Composition on Subsets

Informal description

Let $X$ be a topological space, $s \subseteq X$ a subset, and $f \colon X \to \overline{\mathbb{R}}$ a function that is continuous on $s$. Then the composition $x \mapsto \text{toENNReal}(f(x))$ is also continuous on $s$, where $\text{toENNReal} \colon \overline{\mathbb{R}} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ is the canonical extension of the real numbers to non-negative extended reals.

ContinuousWithinAt.ereal_toENNReal theorem

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

Full source

@[fun_prop]
lemma _root_.ContinuousWithinAt.ereal_toENNReal {α : Type*} [TopologicalSpace α] {f : α → EReal}
    {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) :
    ContinuousWithinAt (fun x => (f x).toENNReal) s x :=
  continuous_toENNReal.continuousAt.comp_continuousWithinAt hf

Continuity Within a Set of the Extended Real to Extended Non-Negative Real Function

Informal description

Let $\alpha$ be a topological space, $f : \alpha \to \overline{\mathbb{R}}$ be a function, $s \subseteq \alpha$ be a subset, and $x \in \alpha$. If $f$ is continuous within $s$ at $x$, then the function $x \mapsto \text{toENNReal}(f(x))$ is also continuous within $s$ at $x$.

ContinuousAt.ereal_toENNReal theorem

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

Full source

@[fun_prop]
lemma _root_.ContinuousAt.ereal_toENNReal {α : Type*} [TopologicalSpace α] {f : α → EReal}
    {x : α} (hf : ContinuousAt f x) :
    ContinuousAt (fun x => (f x).toENNReal) x :=
  continuous_toENNReal.continuousAt.comp hf

Continuity of Extended Real to Extended Non-Negative Real Function at a Point

Informal description

Let $X$ be a topological space and $f : X \to \overline{\mathbb{R}}$ be a function. If $f$ is continuous at a point $x \in X$, then the function $x \mapsto \text{toENNReal}(f(x))$ is also continuous at $x$, where $\text{toENNReal} : \overline{\mathbb{R}} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ maps extended real numbers to extended non-negative real numbers.

EReal.add_iInf_le_iInf_add theorem

: (⨅ x, u x) + ⨅ x, v x ≤ ⨅ x, (u + v) x

Full source

lemma add_iInf_le_iInf_add : (⨅ x, u x) + ⨅ x, v x ≤ ⨅ x, (u + v) x :=
  le_iInf fun i ↦ add_le_add (iInf_le u i) (iInf_le v i)

Infimum Sum Inequality in Extended Reals

Informal description

For any family of extended real numbers $(u_x)_{x \in X}$ and $(v_x)_{x \in X}$, the sum of their infima is less than or equal to the infimum of their pointwise sums, i.e., \[ \left(\inf_{x} u_x\right) + \left(\inf_{x} v_x\right) \leq \inf_{x} (u_x + v_x). \]

EReal.iSup_add_le_add_iSup theorem

: ⨆ x, (u + v) x ≤ (⨆ x, u x) + ⨆ x, v x

Full source

lemma iSup_add_le_add_iSup : ⨆ x, (u + v) x ≤ (⨆ x, u x) + ⨆ x, v x :=
  iSup_le fun i ↦ add_le_add (le_iSup u i) (le_iSup v i)

Supremum of Sum is Bounded by Sum of Suprema in Extended Reals

Informal description

For any family of extended real-valued functions $u$ and $v$, the supremum of their pointwise sum is less than or equal to the sum of their suprema, i.e., \[ \sup_x (u(x) + v(x)) \leq \sup_x u(x) + \sup_x v(x). \]

EReal.liminf_neg theorem

: liminf (-v) f = -limsup v f

Full source

lemma liminf_neg : liminf (- v) f = - limsup v f :=
  EReal.negOrderIsoEReal.negOrderIso.limsup_apply.symm

Limit Inferior of Negation Equals Negation of Limit Superior in Extended Reals

Informal description

For any function $v$ and filter $f$, the limit inferior of $-v$ with respect to $f$ is equal to the negation of the limit superior of $v$ with respect to $f$, i.e., \[ \liminf_{f} (-v) = -\limsup_{f} v. \]

EReal.limsup_neg theorem

: limsup (-v) f = -liminf v f

Full source

lemma limsup_neg : limsup (- v) f = - liminf v f :=
  EReal.negOrderIsoEReal.negOrderIso.liminf_apply.symm

Limit Superior of Negation Equals Negation of Limit Inferior

Informal description

For any function $v$ and any filter $f$, the limit superior of $-v$ is equal to the negation of the limit inferior of $v$, i.e., \[ \limsup (-v) f = -\liminf v f. \]

EReal.le_liminf_add theorem

: (liminf u f) + (liminf v f) ≤ liminf (u + v) f

Full source

lemma le_liminf_add : (liminf u f) + (liminf v f) ≤ liminf (u + v) f := by
  refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
  exact c_ab.trans (add_lt_add a_x b_x)

Inequality for Limit Inferior of Sums: $\liminf u + \liminf v \leq \liminf (u + v)$

Informal description

For any functions $u$ and $v$ and any filter $f$, the sum of the limit inferior of $u$ and the limit inferior of $v$ is less than or equal to the limit inferior of the sum $u + v$, i.e., $$(\liminf u f) + (\liminf v f) \leq \liminf (u + v) f.$$

EReal.limsup_add_le theorem

 (h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤) (h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥) :
  limsup (u + v) f ≤ (limsup u f) + (limsup v f)

Full source

lemma limsup_add_le (h : limsuplimsup u f ≠ ⊥limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤) (h' : limsuplimsup u f ≠ ⊤limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥) :
    limsup (u + v) f ≤ (limsup u f) + (limsup v f) := by
  refine le_add_of_forall_gt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x
  exact (add_lt_add a_x b_x).trans c_ab

Inequality for Limit Superior of Sums: $\limsup (u + v) \leq \limsup u + \limsup v$

Informal description

For any functions $u$ and $v$ and any filter $f$, if either the limit superior of $u$ is not $-\infty$ or the limit superior of $v$ is not $+\infty$, and either the limit superior of $u$ is not $+\infty$ or the limit superior of $v$ is not $-\infty$, then the limit superior of the sum $u + v$ is less than or equal to the sum of the limit superiors of $u$ and $v$, i.e., $$\limsup (u + v) f \leq (\limsup u f) + (\limsup v f).$$

EReal.le_limsup_add theorem

: (limsup u f) + (liminf v f) ≤ limsup (u + v) f

Full source

lemma le_limsup_add : (limsup u f) + (liminf v f) ≤ limsup (u + v) f :=
  add_le_of_forall_lt fun _ a_u _ b_v ↦ (le_limsup_iff).2 fun _ c_ab ↦
    (((frequently_lt_of_lt_limsup) a_u).and_eventually ((eventually_lt_of_lt_liminf) b_v)).mono
    fun _ ab_x ↦ c_ab.trans (add_lt_add ab_x.1 ab_x.2)

Inequality for Limit Superior of Sums: $\limsup u + \liminf v \leq \limsup (u + v)$

Informal description

For any functions $u$ and $v$ and any filter $f$, the sum of the limit superior of $u$ and the limit inferior of $v$ is less than or equal to the limit superior of the sum $u + v$.

EReal.liminf_add_le theorem

 (h : limsup u f ≠ ⊥ ∨ liminf v f ≠ ⊤) (h' : limsup u f ≠ ⊤ ∨ liminf v f ≠ ⊥) :
  liminf (u + v) f ≤ (limsup u f) + (liminf v f)

Full source

lemma liminf_add_le (h : limsuplimsup u f ≠ ⊥limsup u f ≠ ⊥ ∨ liminf v f ≠ ⊤) (h' : limsuplimsup u f ≠ ⊤limsup u f ≠ ⊤ ∨ liminf v f ≠ ⊥) :
    liminf (u + v) f ≤ (limsup u f) + (liminf v f) :=
  le_add_of_forall_gt h h' fun _ a_u _ b_v ↦ (liminf_le_iff).2 fun _ c_ab ↦
    (((frequently_lt_of_liminf_lt) b_v).and_eventually ((eventually_lt_of_limsup_lt) a_u)).mono
    fun _ ab_x ↦ (add_lt_add ab_x.2 ab_x.1).trans c_ab

Inequality for Limit Inferior of Sums: $\liminf (u + v) \leq \limsup u + \liminf v$

Informal description

For any functions $u$ and $v$ and any filter $f$, if either the limit superior of $u$ is not $-\infty$ or the limit inferior of $v$ is not $+\infty$, and either the limit superior of $u$ is not $+\infty$ or the limit inferior of $v$ is not $-\infty$, then the limit inferior of the sum $u + v$ is less than or equal to the sum of the limit superior of $u$ and the limit inferior of $v$, i.e., \[ \liminf (u + v) \leq (\limsup u) + (\liminf v). \]

EReal.limsup_add_bot_of_ne_top theorem

(h : limsup u f = ⊥) (h' : limsup v f ≠ ⊤) : limsup (u + v) f = ⊥

Full source

lemma limsup_add_bot_of_ne_top (h : limsup u f = ⊥) (h' : limsuplimsup v f ≠ ⊤) :
    limsup (u + v) f = ⊥ := by
  apply le_bot_iff.1 ((limsup_add_le (.inr h') _).trans _)
  · rw [h]; exact .inl bot_ne_top
  · rw [h, bot_add]

Limit Superior of Sum is $-\infty$ When One Term's Limit Superior is $-\infty$ and the Other's is Not $+\infty$

Informal description

For any functions $u$ and $v$ and any filter $f$, if the limit superior of $u$ with respect to $f$ is $-\infty$ and the limit superior of $v$ with respect to $f$ is not $+\infty$, then the limit superior of the sum $u + v$ with respect to $f$ is $-\infty$.

EReal.limsup_add_le_of_le theorem

{a b : EReal} (ha : limsup u f < a) (hb : limsup v f ≤ b) : limsup (u + v) f ≤ a + b

Full source

lemma limsup_add_le_of_le {a b : EReal} (ha : limsup u f < a) (hb : limsup v f ≤ b) :
    limsup (u + v) f ≤ a + b := by
  rcases eq_top_or_lt_top b with rfl | h
  · rw [add_top_of_ne_bot ha.ne_bot]; exact le_top
  · exact (limsup_add_le (.inr (hb.trans_lt h).ne) (.inl ha.ne_top)).trans (add_le_add ha.le hb)

Upper Bound for Limit Superior of Sums: $\limsup (u + v) \leq a + b$

Informal description

For any extended real numbers $a$ and $b$, if the limit superior of $u$ with respect to filter $f$ is strictly less than $a$ and the limit superior of $v$ with respect to $f$ is less than or equal to $b$, then the limit superior of the sum $u + v$ with respect to $f$ is less than or equal to $a + b$.

EReal.liminf_add_gt_of_gt theorem

{a b : EReal} (ha : a < liminf u f) (hb : b < liminf v f) : a + b < liminf (u + v) f

Full source

lemma liminf_add_gt_of_gt {a b : EReal} (ha : a < liminf u f) (hb : b < liminf v f) :
    a + b < liminf (u + v) f :=
  (add_lt_add ha hb).trans_le le_liminf_add

Strict Lower Bound for Limit Inferior of Sums: $a + b < \liminf (u + v)$

Informal description

For any extended real numbers $a$ and $b$, if $a$ is less than the limit inferior of $u$ with respect to filter $f$ and $b$ is less than the limit inferior of $v$ with respect to $f$, then $a + b$ is less than the limit inferior of $u + v$ with respect to $f$, i.e., $$a + b < \liminf (u + v) f.$$

EReal.liminf_add_top_of_ne_bot theorem

(h : liminf u f = ⊤) (h' : liminf v f ≠ ⊥) : liminf (u + v) f = ⊤

Full source

lemma liminf_add_top_of_ne_bot (h : liminf u f = ⊤) (h' : liminfliminf v f ≠ ⊥) :
    liminf (u + v) f = ⊤ := by
  apply top_le_iff.1 (le_trans _ le_liminf_add)
  rw [h, top_add_of_ne_bot h']

Limit Inferior of Sum is Top When One Term is Top and the Other is Not Bottom

Informal description

Let $u$ and $v$ be functions and $f$ be a filter. If the limit inferior of $u$ with respect to $f$ is $\top$ (i.e., $\liminf u f = \top$) and the limit inferior of $v$ with respect to $f$ is not $\bot$ (i.e., $\liminf v f \neq \bot$), then the limit inferior of the sum $u + v$ with respect to $f$ is $\top$ (i.e., $\liminf (u + v) f = \top$).

EReal.le_limsup_mul theorem

(hu : ∃ᶠ x in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) : limsup u f * liminf v f ≤ limsup (u * v) f

Full source

lemma le_limsup_mul (hu : ∃ᶠ x in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) :
    limsup u f * liminf v f ≤ limsup (u * v) f := by
  rcases f.eq_or_neBot with rfl | _
  · rw [limsup_bot, limsup_bot, liminf_bot, bot_mul_top]
  have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu
  have uv0 : 0 ≤ limsup (u * v) f :=
    le_limsup_of_frequently_lele_limsup_of_frequently_le <| (hu.and_eventually hv).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv
  refine mul_le_of_forall_lt_of_nonneg u0 uv0 fun a ha b hb ↦ (le_limsup_iff).2 fun c c_ab ↦ ?_
  refine (((frequently_lt_of_lt_limsup) (mem_Ioo.1 ha).2).and_eventually
    <| (eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2).and
    <| hv).mono fun x ⟨xa, ⟨xb, vx⟩⟩ ↦ ?_
  exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))

Inequality Relating Limit Superior and Limit Inferior of Products

Informal description

Let $u$ and $v$ be functions such that $u(x) \geq 0$ frequently in the filter $f$ and $v(x) \geq 0$ eventually in $f$. Then the product of the limit superior of $u$ and the limit inferior of $v$ is less than or equal to the limit superior of the product function $u \cdot v$: \[ \limsup_{f} u \cdot \liminf_{f} v \leq \limsup_{f} (u \cdot v). \]

EReal.limsup_mul_le theorem

 (hu : ∃ᶠ x in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) (h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤)
  (h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0) : limsup (u * v) f ≤ limsup u f * limsup v f

Full source

lemma limsup_mul_le (hu : ∃ᶠ x in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v)
    (h₁ : limsuplimsup u f ≠ 0limsup u f ≠ 0 ∨ limsup v f ≠ ⊤) (h₂ : limsuplimsup u f ≠ ⊤limsup u f ≠ ⊤ ∨ limsup v f ≠ 0) :
    limsup (u * v) f ≤ limsup u f * limsup v f := by
  rcases f.eq_or_neBot with rfl | _
  · rw [limsup_bot]; exact bot_le
  have u_0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu
  replace h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤ := h₁.imp_left fun h ↦ lt_of_le_of_ne u_0 h.symm
  replace h₂ : limsuplimsup u f ≠ ⊤limsup u f ≠ ⊤ ∨ 0 < limsup v f :=
    h₂.imp_right fun h ↦ lt_of_le_of_ne (le_limsup_of_frequently_le hv.frequently) h.symm
  refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v, hv]
    with x x_a x_b v_0
  apply lt_of_le_of_lt _ c_ab
  rcases lt_or_ge (u x) 0 with hux | hux
  · apply (mul_nonpos_iff.2 (.inr ⟨hux.le, v_0⟩)).trans
    exact mul_nonneg (u_0.trans a_u.le) (v_0.trans x_b.le)
  · exact mul_le_mul x_a.le x_b.le v_0 (hux.trans x_a.le)

Upper Bound for Limsup of Product of Extended Real-Valued Functions

Informal description

Let $u$ and $v$ be functions with values in the extended real numbers $\overline{\mathbb{R}}$, and let $f$ be a filter. Suppose that: 1. $u$ is frequently nonnegative (i.e., $\exists^\infty x \in f, 0 \leq u(x)$), 2. $v$ is eventually nonnegative (i.e., $0 \leq v(x)$ for $f$-almost all $x$), 3. Either $\limsup u \neq 0$ or $\limsup v \neq \top$, 4. Either $\limsup u \neq \top$ or $\limsup v \neq 0$. Then the limsup of the product $u \cdot v$ satisfies: \[ \limsup (u \cdot v) \leq (\limsup u) \cdot (\limsup v). \]

EReal.le_liminf_mul theorem

(hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) : liminf u f * liminf v f ≤ liminf (u * v) f

Full source

lemma le_liminf_mul (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) :
    liminf u f * liminf v f ≤ liminf (u * v) f := by
  apply mul_le_of_forall_lt_of_nonneg ((le_liminf_of_le) hu)
    <| (le_liminf_of_le) ((hu.and hv).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0)
  refine fun a ha b hb ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_lt_liminf (mem_Ioo.1 ha).2,
    eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2] with x xa xb
  exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))

Inequality for Limit Inferior of Products: $\liminf u \cdot \liminf v \leq \liminf (u \cdot v)$ under Nonnegativity

Informal description

For any filter $f$ and functions $u, v$ such that $0 \leq u(x)$ and $0 \leq v(x)$ eventually at $f$, the product of the limit inferior of $u$ and the limit inferior of $v$ is less than or equal to the limit inferior of the product $u \cdot v$ at $f$.

EReal.liminf_mul_le theorem

 [NeBot f] (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) (h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤)
  (h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0) : liminf (u * v) f ≤ limsup u f * liminf v f

Full source

lemma liminf_mul_le [NeBot f] (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v)
    (h₁ : limsuplimsup u f ≠ 0limsup u f ≠ 0 ∨ liminf v f ≠ ⊤) (h₂ : limsuplimsup u f ≠ ⊤limsup u f ≠ ⊤ ∨ liminf v f ≠ 0) :
    liminf (u * v) f ≤ limsup u f * liminf v f := by
  replace h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤ := by
    refine h₁.imp_left fun h ↦ lt_of_le_of_ne ?_ h.symm
    exact le_of_eq_of_le (limsup_const 0).symm (limsup_le_limsup hu)
  replace h₂ : limsuplimsup u f ≠ ⊤limsup u f ≠ ⊤ ∨ 0 < liminf v f := by
    refine h₂.imp_right fun h ↦ lt_of_le_of_ne ?_ h.symm
    exact le_of_eq_of_le (liminf_const 0).symm (liminf_le_liminf hv)
  refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (liminf_le_iff).2 fun c c_ab ↦ ?_
  refine (((frequently_lt_of_liminf_lt) b_v).and_eventually <| (eventually_lt_of_limsup_lt a_u).and
    <| hu.and hv).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_
  exact (mul_le_mul x_u.le x_v.le v_0 (u_0.trans x_u.le)).trans_lt c_ab

Inequality for liminf of product in extended reals

Informal description

Let $f$ be a non-trivial filter, and let $u$, $v$ be functions such that $0 \leq u$ and $0 \leq v$ eventually along $f$. If either $\limsup f u \neq 0$ or $\liminf f v \neq \top$, and either $\limsup f u \neq \top$ or $\liminf f v \neq 0$, then the following inequality holds for the extended real numbers: \[ \liminf f (u \cdot v) \leq (\limsup f u) \cdot (\liminf f v) \]

EReal.continuousAt_add_coe_coe theorem

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

Full source

theorem continuousAt_add_coe_coe (a b : ℝ) :
    ContinuousAt (fun p : ERealEReal × EReal => p.1 + p.2) (a, b) := by
  simp only [ContinuousAt, nhds_coe_coe, ← coe_add, tendsto_map'_iff, Function.comp_def,
    tendsto_coe, tendsto_add]

Continuity of Addition at Real Points in Extended Reals

Informal description

For any real numbers $a$ and $b$, the addition function $(x, y) \mapsto x + y$ is continuous at the point $(a, b)$ in the extended real numbers $\overline{\mathbb{R}} \times \overline{\mathbb{R}}$.

EReal.continuousAt_add_top_coe theorem

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

Full source

theorem continuousAt_add_top_coe (a : ℝ) :
    ContinuousAt (fun p : ERealEReal × EReal => p.1 + p.2) (⊤, a) := by
  simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_coe]
  refine fun r ↦ ((lt_mem_nhds (coe_lt_top (r - (a - 1)))).prod_nhds
    (lt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| sub_one_lt _)).mono fun _ h ↦ ?_
  simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

Continuity of Addition at $(\infty, a)$ in Extended Reals

Informal description

For any real number $a$, the addition function $(x, y) \mapsto x + y$ is continuous at the point $(\infty, a)$ in the extended real numbers $\overline{\mathbb{R}} \times \overline{\mathbb{R}}$.

EReal.continuousAt_add_coe_top theorem

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

Full source

theorem continuousAt_add_coe_top (a : ℝ) :
    ContinuousAt (fun p : ERealEReal × EReal => p.1 + p.2) (a, ⊤) := by
  simpa only [add_comm, Function.comp_def, ContinuousAt, Prod.swap]
    using Tendsto.comp (continuousAt_add_top_coe a) (continuous_swap.tendsto ((a : EReal), ⊤))

Continuity of Addition at $(a, \infty)$ in Extended Reals

Informal description

For any real number $a$, the addition function $(x, y) \mapsto x + y$ is continuous at the point $(a, \infty)$ in the extended real numbers $\overline{\mathbb{R}} \times \overline{\mathbb{R}}$.

EReal.continuousAt_add_top_top theorem

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

Full source

theorem continuousAt_add_top_top : ContinuousAt (fun p : ERealEReal × EReal => p.1 + p.2) (⊤, ⊤) := by
  simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]
  refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds
    (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_
  simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2

Continuity of Addition at $(\infty, \infty)$ in Extended Reals

Informal description

The addition operation on the extended real numbers $\overline{\mathbb{R}}$ is continuous at the point $(\top, \top)$, where $\top$ denotes positive infinity.

EReal.continuousAt_add_bot_coe theorem

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

Full source

theorem continuousAt_add_bot_coe (a : ℝ) :
    ContinuousAt (fun p : ERealEReal × EReal => p.1 + p.2) (⊥, a) := by
  simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
  refine fun r ↦ ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds
    (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono fun _ h ↦ ?_
  simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

Continuity of Addition at $(-\infty, a)$ in Extended Real Numbers

Informal description

For any real number $a \in \mathbb{R}$, the addition operation on the extended real numbers $\overline{\mathbb{R}}$ is continuous at the point $(-\infty, a)$, where $-\infty$ is the bottom element of $\overline{\mathbb{R}}$.

EReal.continuousAt_add_coe_bot theorem

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

Full source

theorem continuousAt_add_coe_bot (a : ℝ) :
    ContinuousAt (fun p : ERealEReal × EReal => p.1 + p.2) (a, ⊥) := by
  simpa only [add_comm, Function.comp_def, ContinuousAt, Prod.swap]
    using Tendsto.comp (continuousAt_add_bot_coe a) (continuous_swap.tendsto ((a : EReal), ⊥))

Continuity of Addition at $(a, -\infty)$ in Extended Real Numbers

Informal description

For any real number $a \in \mathbb{R}$, the addition operation on the extended real numbers $\overline{\mathbb{R}}$ is continuous at the point $(a, -\infty)$, where $-\infty$ is the bottom element of $\overline{\mathbb{R}}$.

EReal.continuousAt_add_bot_bot theorem

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

Full source

theorem continuousAt_add_bot_bot : ContinuousAt (fun p : ERealEReal × EReal => p.1 + p.2) (⊥, ⊥) := by
  simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
  refine fun r ↦ ((gt_mem_nhds (bot_lt_coe 0)).prod_nhds
    (gt_mem_nhds <| bot_lt_coe r)).mono fun _ h ↦ ?_
  simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2

Continuity of Addition at $(-\infty, -\infty)$ in Extended Real Numbers

Informal description

The addition operation on extended real numbers is continuous at the point $(\bot, \bot)$, where $\bot$ denotes $-\infty$.

EReal.continuousAt_add theorem

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

Full source

/-- The addition on `EReal` is continuous except where it doesn't make sense (i.e., at `(⊥, ⊤)`
and at `(⊤, ⊥)`). -/
theorem continuousAt_add {p : ERealEReal × EReal} (h : p.1 ≠ ⊤p.1 ≠ ⊤ ∨ p.2 ≠ ⊥) (h' : p.1 ≠ ⊥p.1 ≠ ⊥ ∨ p.2 ≠ ⊤) :
    ContinuousAt (fun p : ERealEReal × EReal => p.1 + p.2) p := by
  rcases p with ⟨x, y⟩
  induction x <;> induction y
  · exact continuousAt_add_bot_bot
  · exact continuousAt_add_bot_coe _
  · simp at h'
  · exact continuousAt_add_coe_bot _
  · exact continuousAt_add_coe_coe _ _
  · exact continuousAt_add_coe_top _
  · simp at h
  · exact continuousAt_add_top_coe _
  · exact continuousAt_add_top_top

Continuity of Addition on Extended Reals Except at $(\infty, -\infty)$ and $(-\infty, \infty)$

Informal description

Let $p = (x, y)$ be a pair of extended real numbers in $\overline{\mathbb{R}} \times \overline{\mathbb{R}}$. If either $x \neq \infty$ or $y \neq -\infty$, and either $x \neq -\infty$ or $y \neq \infty$, then the addition function $(x, y) \mapsto x + y$ is continuous at $p$.

EReal.continuousAt_mul theorem

 {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

Full source

/-- The multiplication on `EReal` is continuous except at indeterminacies
(i.e. whenever one value is zero and the other infinite). -/
theorem continuousAt_mul {p : ERealEReal × EReal} (h₁ : p.1 ≠ 0p.1 ≠ 0 ∨ p.2 ≠ ⊥)
    (h₂ : p.1 ≠ 0p.1 ≠ 0 ∨ p.2 ≠ ⊤) (h₃ : p.1 ≠ ⊥p.1 ≠ ⊥ ∨ p.2 ≠ 0) (h₄ : p.1 ≠ ⊤p.1 ≠ ⊤ ∨ p.2 ≠ 0) :
    ContinuousAt (fun p : ERealEReal × EReal ↦ p.1 * p.2) p := by
  rcases p with ⟨x, y⟩
  induction x <;> induction y
  · exact continuousAt_mul_symm3 continuousAt_mul_top_top
  · simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₃
    exact continuousAt_mul_symm1 (continuousAt_mul_top_ne_zero h₃)
  · exact EReal.neg_top ▸ continuousAt_mul_symm1 continuousAt_mul_top_top
  · simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₁
    exact continuousAt_mul_symm2 (continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₁))
  · exact continuousAt_mul_coe_coe _ _
  · simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₂
    exact continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₂)
  · exact continuousAt_mul_symm2 continuousAt_mul_top_top
  · simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₄
    exact continuousAt_mul_top_ne_zero h₄
  · exact continuousAt_mul_top_top

Continuity of Extended Real Multiplication Away from Indeterminate Cases

Informal description

Let $p = (x, y)$ be a pair of extended real numbers in $\overline{\mathbb{R}} \times \overline{\mathbb{R}}$. The multiplication function $(x, y) \mapsto x \cdot y$ is continuous at $p$ provided that: 1. Either $x \neq 0$ or $y \neq -\infty$, 2. Either $x \neq 0$ or $y \neq +\infty$, 3. Either $x \neq -\infty$ or $y \neq 0$, 4. Either $x \neq +\infty$ or $y \neq 0$. In other words, multiplication is continuous at all points except where one coordinate is zero and the other is infinite (in either direction).

EReal.lowerSemicontinuous_add theorem

: LowerSemicontinuous fun p : EReal × EReal ↦ p.1 + p.2

Full source

lemma lowerSemicontinuous_add : LowerSemicontinuous fun p : ERealEReal × EReal ↦ p.1 + p.2 := by
  intro x y
  by_cases hx₁ : x.1 = ⊥
  · simp [hx₁]
  by_cases hx₂ : x.2 = ⊥
  · simp [hx₂]
  · exact continuousAt_add (.inr hx₂) (.inl hx₁) |>.lowerSemicontinuousAt _

Lower Semicontinuity of Addition on Extended Real Numbers

Informal description

The addition function $(x, y) \mapsto x + y$ on extended real numbers $\overline{\mathbb{R}} \times \overline{\mathbb{R}}$ is lower semicontinuous.

Mathlib.Topology.Instances.EReal.Lemmas

Main results

Implementation