[Merged by Bors] - feat(measure_theory): Borel-Cantelli #4166
Conversation
jcommelin
requested review from
urkud,
hrmacbeth,
PatrickMassot and
sgouezel
| @@ -111,6 +111,14 @@ lemma summable_comp_injective {β : Type*} {f : α → nnreal} (hf : summable f) | |||
| nnreal.summable_coe.1 $ | |||
| show summable ((coe ∘ f) ∘ i), from (nnreal.summable_coe.2 hf).comp_injective hi | |||
|
|
|||
| lemma summable_nat_add (f : ℕ → nnreal) (hf : summable f) (k : ℕ) : summable (λ i, f (i + k)) := | |||
There was a problem hiding this comment.
In infinite_sum.lean, you have summable_nat_add_iff that says something very similar (in fact a little bit stronger because there is an equivalence, which should also hold in nnreal), except it doesn't apply in your situation because nnreal is not an add_comm_group. Is it worth refactoring summable_nat_add_iff to let it apply in any add_left_cancel_semigroup with has_continuous_add (or whatever typeclass covers both situations uniformly)?
There was a problem hiding this comment.
I thought about this, but I'm honestly not sure whether the statement is true in an add_left_cancel_semigroup, because to state the underlying has_sum for the direction discussed here, you need some kind of subtraction. I thought about adding a type class for a sort of "weak subtraction" that is fulfilled by both add_comm_groups and things like nnreal and nat, but I came to the conclusion that it's not worth the effort.
However, maybe I'm missing something and the statement really is true in an add_left_cancel_semigroup. What do you think?
sgouezel
added
awaiting-author
TwoFX
added
awaiting-review
| @@ -111,6 +111,14 @@ lemma summable_comp_injective {β : Type*} {f : α → nnreal} (hf : summable f) | |||
| nnreal.summable_coe.1 $ | |||
| show summable ((coe ∘ f) ∘ i), from (nnreal.summable_coe.2 hf).comp_injective hi | |||
|
|
|||
| lemma summable_nat_add (f : ℕ → nnreal) (hf : summable f) (k : ℕ) : summable (λ i, f (i + k)) := | |||
github-actions
bot
added
the
ready-to-merge
```lean
lemma measure_limsup_eq_zero {s : ℕ → set α} (hs : ∀ i, is_measurable (s i))
(hs' : (∑' i, μ (s i)) ≠ ⊤) : μ (limsup at_top s) = 0
```
There is a converse statement that is also called Borel-Cantelli, but we can't state it yet, because we don't know what independent events are.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
YaelDillies
removed
the
awaiting-review
There is a converse statement that is also called Borel-Cantelli, but we can't state it yet, because we don't know what independent events are.