From d96321039c313a40308dc9eadff256926f437d16 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sat, 27 Jan 2024 00:17:33 +0100 Subject: [PATCH 1/2] refactor(Probability/Kernel/CondCdf): mv tendsto_of_antitone --- Mathlib/Probability/Kernel/CondCdf.lean | 7 ------- Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean | 6 ++++++ 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean index 2d223aba3e6ac..cd5a19902b51a 100644 --- a/Mathlib/Probability/Kernel/CondCdf.lean +++ b/Mathlib/Probability/Kernel/CondCdf.lean @@ -108,13 +108,6 @@ theorem atTop_le_nhds_top {α : Type*} [TopologicalSpace α] [LinearOrder α] [O @atBot_le_nhds_bot αᵒᵈ _ _ _ _ #align at_top_le_nhds_top atTop_le_nhds_top --- todo: move to topology/algebra/order/monotone_convergence -theorem tendsto_of_antitone {ι α : Type*} [Preorder ι] [TopologicalSpace α] - [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Antitone f) : - Tendsto f atTop atBot ∨ ∃ l, Tendsto f atTop (𝓝 l) := - @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 diff --git a/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean b/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean index 6c16cd2a12183..44d86d16c7542 100644 --- a/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean +++ b/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean @@ -310,6 +310,12 @@ theorem iInf_eq_of_tendsto {α} [TopologicalSpace α] [CompleteLinearOrder α] [ tendsto_nhds_unique (tendsto_atTop_iInf hf) #align infi_eq_of_tendsto iInf_eq_of_tendsto +theorem tendsto_of_antitone {ι α : Type*} [Preorder ι] [TopologicalSpace α] + [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Antitone f) : + Tendsto f atTop atBot ∨ ∃ l, Tendsto f atTop (𝓝 l) := + @tendsto_of_monotone ι αᵒᵈ _ _ _ _ _ h_mono +#align tendsto_of_antitone tendsto_of_antitone + theorem iSup_eq_iSup_subseq_of_monotone {ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α] {l : Filter ι₁} [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Monotone f) (hφ : Tendsto φ l atTop) : ⨆ i, f i = ⨆ i, f (φ i) := From 361f44ad1dd68fbae294209ae0c132b632c06752 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sat, 27 Jan 2024 10:22:59 -0800 Subject: [PATCH 2/2] move next to tendsto_of_monotone --- .../Topology/Algebra/Order/MonotoneConvergence.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean b/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean index 44d86d16c7542..6ba1a6eee4ada 100644 --- a/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean +++ b/Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean @@ -227,6 +227,12 @@ theorem tendsto_of_monotone {ι α : Type*} [Preorder ι] [TopologicalSpace α] else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H #align tendsto_of_monotone tendsto_of_monotone +theorem tendsto_of_antitone {ι α : Type*} [Preorder ι] [TopologicalSpace α] + [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Antitone f) : + Tendsto f atTop atBot ∨ ∃ l, Tendsto f atTop (𝓝 l) := + @tendsto_of_monotone ι αᵒᵈ _ _ _ _ _ h_mono +#align tendsto_of_antitone tendsto_of_antitone + theorem tendsto_iff_tendsto_subseq_of_monotone {ι₁ ι₂ α : Type*} [SemilatticeSup ι₁] [Preorder ι₂] [Nonempty ι₁] [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [NoMaxOrder α] {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α} (hf : Monotone f) @@ -310,12 +316,6 @@ theorem iInf_eq_of_tendsto {α} [TopologicalSpace α] [CompleteLinearOrder α] [ tendsto_nhds_unique (tendsto_atTop_iInf hf) #align infi_eq_of_tendsto iInf_eq_of_tendsto -theorem tendsto_of_antitone {ι α : Type*} [Preorder ι] [TopologicalSpace α] - [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Antitone f) : - Tendsto f atTop atBot ∨ ∃ l, Tendsto f atTop (𝓝 l) := - @tendsto_of_monotone ι αᵒᵈ _ _ _ _ _ h_mono -#align tendsto_of_antitone tendsto_of_antitone - theorem iSup_eq_iSup_subseq_of_monotone {ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α] {l : Filter ι₁} [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Monotone f) (hφ : Tendsto φ l atTop) : ⨆ i, f i = ⨆ i, f (φ i) :=