Existence from almost always and non-zero measure

Stream: Is there code for X?

[Oliver Nash]

Do we have something like this anywhere:

import measure_theory.measure.measure_space

open set filter measure_theory

lemma exists_of_measure_ne_zero_of_ae {α : Type*} [measurable_space α] {μ : measure α}
  {S : set α} (hS : μ S ≠ 0) {p : α → Prop} (hp : ∀ᵐ x ∂μ.restrict S, p x) :
  ∃ x, x ∈ S ∧ p x :=
begin
  obtain ⟨t, ht₁ : μ.restrict S tᶜ = 0, ht₂⟩ := eventually_iff_exists_mem.mp hp,
  have hst : (S ∩ t).nonempty,
  { contrapose! hS,
    rw [not_nonempty_iff_eq_empty, inter_comm, ← bot_eq_empty, ← inf_eq_inter, ← disjoint_iff,
      ← sdiff_eq_self_iff_disjoint, diff_eq_compl_inter] at hS,
    rw [← hS, ← measure.restrict_apply₀ (null_measurable_set.of_null ht₁), ht₁], },
  obtain ⟨x, hx₁, hx₂⟩ := hst,
  exact ⟨x, hx₁, ht₂ x hx₂⟩,
end

[Anatole Dedecker]

The key lemma is docs#measure_theory.ae_restrict_ne_bot

[Anatole Dedecker]

Then you can apply docs#filter.eventually.exists

[Anatole Dedecker]

Oh and if you want the fact that x ∈ S you also need docs#ae_restrict_mem

[Anatole Dedecker]

Oh but my proof needs S to be measurable

[Anatole Dedecker]

Ok here's a proof without assuming that S is measurable :

import measure_theory.measure.measure_space

open set filter measure_theory

lemma exists_of_measure_ne_zero_of_ae {α : Type*} [measurable_space α] {μ : measure α}
  {S : set α} (hS : μ S ≠ 0) {p : α → Prop} (hp : ∀ᵐ x ∂μ.restrict S, p x) :
  ∃ x, x ∈ S ∧ p x :=
begin
  rw [← measure.restrict_apply_self, ← frequently_ae_mem_iff] at hS,
  exact (hS.and_eventually hp).exists
end

[Oliver Nash]

Thanks @Anatole Dedecker this is exactly what I wanted. I just tried quite hard and I can even find a way to golf this :-)

[Oliver Nash]

I just made this a PR: #15812