From e8bfb678dad1331ef34cf9531144b5295b96ece9 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sun, 28 Jan 2024 09:07:45 +0000 Subject: [PATCH] refactor(Probability/Kernel/CondCdf): mv ofReal_cinfi (#10044) Co-authored-by: Moritz Firsching --- 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 49eaad73a699e..9aa4764acb5fa 100644 --- a/Mathlib/Probability/Kernel/CondCdf.lean +++ b/Mathlib/Probability/Kernel/CondCdf.lean @@ -108,21 +108,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..db83769a108e0 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal.lean @@ -708,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