Skip to content

[Merged by Bors] - refactor(Probability/Kernel/CondCdf): mv tendsto_of_antitone #10046

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - refactor(Probability/Kernel/CondCdf): mv tendsto_of_antitone #10046

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d963210
refactor(Probability/Kernel/CondCdf): mv tendsto_of_antitone
mo271 Jan 26, 2024
361f44a
move next to tendsto_of_monotone
mo271 Jan 27, 2024
1bc733e
Merge branch 'master' into mo271/mv_from_prob_kernel5
mo271 Jan 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 0 additions & 7 deletions Mathlib/Probability/Kernel/CondCdf.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,13 +87,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 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 β]
Expand Down
6 changes: 6 additions & 0 deletions Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down