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

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

Closed
wants to merge 2 commits into from
Closed

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

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
37e6cb8
refactor(Probability/Kernel/CondCdf): mv ofReal_cinfi
mo271 Jan 26, 2024
ce0304c
move further down
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
15 changes: 0 additions & 15 deletions Mathlib/Probability/Kernel/CondCdf.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 β]
Expand Down
14 changes: 14 additions & 0 deletions Mathlib/Topology/Instances/ENNReal.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 α] :
Copy link
Contributor

Choose a reason for hiding this comment

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

The place of this lemma is not ideal. You put this between tendsto_nhds and tendsto_nhds_zero, which are two very related lemmas. Could you put it further down, where it would not break a sequence of related results?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

moved it to the end of the TopologicalSpace section.

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
Expand Down
Loading