Skip to content
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

Jump to bottom

[Merged by Bors] - refactor(Probability/Kernel/CondCdf): mv some theorems #10036

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - refactor(Probability/Kernel/CondCdf): mv some theorems #10036

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d719abc
chore(Probability/Kernel/CondCdf): mv some theorems
mo271 Jan 26, 2024
9f27b53
Update Mathlib/Probability/Kernel/CondCdf.lean
mo271 Jan 26, 2024
0b9169b
Merge branch 'master' into mo271/mv_from_prob_kernel
mo271 Jan 27, 2024
5d5226c
add sections
mo271 Jan 27, 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
22 changes: 21 additions & 1 deletion Mathlib/Logic/Encodable/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -655,7 +655,11 @@ theorem rel_sequence {r : β → β → Prop} {f : α → β} (hf : Directed r f
exact (Classical.choose_spec (hf _ a)).2
#align directed.rel_sequence Directed.rel_sequence

variable [Preorder β] {f : α → β} (hf : Directed (· ≤ ·) f)
variable [Preorder β] {f : α → β}

section

variable (hf : Directed (· ≤ ·) f)

theorem sequence_mono : Monotone (f ∘ hf.sequence f) :=
monotone_nat_of_le_succ <| hf.sequence_mono_nat
Expand All @@ -665,6 +669,22 @@ theorem le_sequence (a : α) : f a ≤ f (hf.sequence f (encode a + 1)) :=
hf.rel_sequence a
#align directed.le_sequence Directed.le_sequence

end

section

variable (hf : Directed (· ≥ ·) f)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please put sections around sequence_mono and le_sequence on one hand, and around sequence_anti and sequence_le on the other hand, in order to restrict the scope of the variable declarations?

By the way, thanks a lot for moving these theorems. I left those post-port tasks and should have done them a while ago.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

sections added.


theorem sequence_anti : Antitone (f ∘ hf.sequence f) :=
antitone_nat_of_succ_le <| hf.sequence_mono_nat
#align directed.sequence_anti Directed.sequence_anti

theorem sequence_le (a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f a :=
hf.rel_sequence a
#align directed.sequence_le Directed.sequence_le

end

end Directed

section Quotient
Expand Down
16 changes: 1 addition & 15 deletions Mathlib/Probability/Kernel/CondCdf.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ Copyright (c) 2023 Rémy Degenne. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémy Degenne
-/
import Mathlib.Logic.Encodable.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.MeasureTheory.Measure.Stieltjes
import Mathlib.MeasureTheory.Decomposition.RadonNikodym
Expand Down Expand Up @@ -52,21 +53,6 @@ section AuxLemmasToBeMoved

variable {α β ι : Type*}

namespace Directed

-- todo after the port: move this to logic.encodable.basic near sequence_mono
variable [Encodable α] [Inhabited α] [Preorder β] {f : α → β} (hf : Directed (· ≥ ·) f)

theorem sequence_anti : Antitone (f ∘ hf.sequence f) :=
antitone_nat_of_succ_le <| hf.sequence_mono_nat
#align directed.sequence_anti Directed.sequence_anti

theorem sequence_le (a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f a :=
hf.rel_sequence a
#align directed.sequence_le Directed.sequence_le

end Directed

theorem Real.iUnion_Iic_rat : ⋃ r : ℚ, Iic (r : ℝ) = univ := by
ext1 x
simp only [mem_iUnion, mem_Iic, mem_univ, iff_true_iff]
Expand Down
Loading