From 37e6cb83c15cedae097e177aa9841e99bdba67f6 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Fri, 26 Jan 2024 23:46:40 +0100 Subject: [PATCH 1/2] refactor(Probability/Kernel/CondCdf): mv ofReal_cinfi --- Mathlib/Probability/Kernel/CondCdf.lean | 15 --------------- Mathlib/Topology/Instances/ENNReal.lean | 14 ++++++++++++++ 2 files changed, 14 insertions(+), 15 deletions(-) diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean index 2d223aba3e6ac..96b7d7a740469 100644 --- a/Mathlib/Probability/Kernel/CondCdf.lean +++ b/Mathlib/Probability/Kernel/CondCdf.lean @@ -115,21 +115,6 @@ theorem tendsto_of_antitone {ι α : Type*} [Preorder ι] [TopologicalSpace α] @tendsto_of_monotone ι αᵒᵈ _ _ _ _ _ h_mono #align tendsto_of_antitone tendsto_of_antitone --- todo: move to data/real/ennreal -theorem ENNReal.ofReal_cinfi (f : α → ℝ) [Nonempty α] : - ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i) := by - by_cases hf : BddBelow (range f) - · exact - Monotone.map_ciInf_of_continuousAt ENNReal.continuous_ofReal.continuousAt - (fun i j hij => ENNReal.ofReal_le_ofReal hij) hf - · symm - rw [Real.iInf_of_not_bddBelow hf, ENNReal.ofReal_zero, ← ENNReal.bot_eq_zero, iInf_eq_bot] - obtain ⟨y, hy_mem, hy_neg⟩ := not_bddBelow_iff.mp hf 0 - obtain ⟨i, rfl⟩ := mem_range.mpr hy_mem - refine' fun x hx => ⟨i, _⟩ - rwa [ENNReal.ofReal_of_nonpos hy_neg.le] -#align ennreal.of_real_cinfi ENNReal.ofReal_cinfi - -- todo: move to measure_theory/measurable_space /-- Monotone convergence for an infimum over a directed family and indexed by a countable type -/ theorem lintegral_iInf_directed_of_measurable {mα : MeasurableSpace α} [Countable β] diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index 4b3ab3bee3e7d..ccad25f5f7027 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal.lean @@ -283,6 +283,20 @@ protected theorem tendsto_nhds {f : Filter α} {u : α → ℝ≥0∞} {a : ℝ simp only [nhds_of_ne_top ha, tendsto_iInf, tendsto_principal] #align ennreal.tendsto_nhds ENNReal.tendsto_nhds +theorem ofReal_cinfi (f : α → ℝ) [Nonempty α] : + ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i) := by + by_cases hf : BddBelow (range f) + · exact + Monotone.map_ciInf_of_continuousAt ENNReal.continuous_ofReal.continuousAt + (fun i j hij => ENNReal.ofReal_le_ofReal hij) hf + · symm + rw [Real.iInf_of_not_bddBelow hf, ENNReal.ofReal_zero, ← ENNReal.bot_eq_zero, iInf_eq_bot] + obtain ⟨y, hy_mem, hy_neg⟩ := not_bddBelow_iff.mp hf 0 + obtain ⟨i, rfl⟩ := mem_range.mpr hy_mem + refine' fun x hx => ⟨i, _⟩ + rwa [ENNReal.ofReal_of_nonpos hy_neg.le] +#align ennreal.of_real_cinfi ENNReal.ofReal_cinfi + protected theorem tendsto_nhds_zero {f : Filter α} {u : α → ℝ≥0∞} : Tendsto u f (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in f, u x ≤ ε := nhds_zero_basis_Iic.tendsto_right_iff From ce0304c2afc3391ba49417a7a3ec6cab097fd1fc Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sat, 27 Jan 2024 10:18:39 -0800 Subject: [PATCH 2/2] move further down --- Mathlib/Topology/Instances/ENNReal.lean | 28 ++++++++++++------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index ccad25f5f7027..db83769a108e0 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal.lean @@ -283,20 +283,6 @@ protected theorem tendsto_nhds {f : Filter α} {u : α → ℝ≥0∞} {a : ℝ simp only [nhds_of_ne_top ha, tendsto_iInf, tendsto_principal] #align ennreal.tendsto_nhds ENNReal.tendsto_nhds -theorem ofReal_cinfi (f : α → ℝ) [Nonempty α] : - ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i) := by - by_cases hf : BddBelow (range f) - · exact - Monotone.map_ciInf_of_continuousAt ENNReal.continuous_ofReal.continuousAt - (fun i j hij => ENNReal.ofReal_le_ofReal hij) hf - · symm - rw [Real.iInf_of_not_bddBelow hf, ENNReal.ofReal_zero, ← ENNReal.bot_eq_zero, iInf_eq_bot] - obtain ⟨y, hy_mem, hy_neg⟩ := not_bddBelow_iff.mp hf 0 - obtain ⟨i, rfl⟩ := mem_range.mpr hy_mem - refine' fun x hx => ⟨i, _⟩ - rwa [ENNReal.ofReal_of_nonpos hy_neg.le] -#align ennreal.of_real_cinfi ENNReal.ofReal_cinfi - protected theorem tendsto_nhds_zero {f : Filter α} {u : α → ℝ≥0∞} : Tendsto u f (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in f, u x ≤ ε := nhds_zero_basis_Iic.tendsto_right_iff @@ -722,6 +708,20 @@ theorem exists_lt_add_of_lt_add {x y z : ℝ≥0∞} (h : x < y + z) (hy : y ≠ exact ⟨y', z', hy', hz', hx⟩ #align ennreal.exists_lt_add_of_lt_add ENNReal.exists_lt_add_of_lt_add +theorem ofReal_cinfi (f : α → ℝ) [Nonempty α] : + ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i) := by + by_cases hf : BddBelow (range f) + · exact + Monotone.map_ciInf_of_continuousAt ENNReal.continuous_ofReal.continuousAt + (fun i j hij => ENNReal.ofReal_le_ofReal hij) hf + · symm + rw [Real.iInf_of_not_bddBelow hf, ENNReal.ofReal_zero, ← ENNReal.bot_eq_zero, iInf_eq_bot] + obtain ⟨y, hy_mem, hy_neg⟩ := not_bddBelow_iff.mp hf 0 + obtain ⟨i, rfl⟩ := mem_range.mpr hy_mem + refine' fun x hx => ⟨i, _⟩ + rwa [ENNReal.ofReal_of_nonpos hy_neg.le] +#align ennreal.of_real_cinfi ENNReal.ofReal_cinfi + end TopologicalSpace section Liminf