'almost everywhere' version of le_of_forall_gt

Stream: Is there code for X?

[Joris van Winden]

I proved the following lemma which is common in probability theory. It gives an epsilon of room when checking a.e. inequalities, with the epsilon being outside of the a.e. quantifier.

Before I make a PR I wanted to ask if something similar might already exist. Does it?

theorem ae_le_of_forall_gt_ae_le [LinearOrder β] [TopologicalSpace β]
    [OrderTopology β] [DenselyOrdered β] [TopologicalSpace.SeparableSpace β]
    {a : β} {f : α → β} (h : (∀ b : β, a < b → ∀ᵐ x ∂μ, f x ≤ b)) : (∀ᵐ x ∂μ, f x ≤ a)

[Yongxi Lin (Aaron)]

MeasureTheory.ae_le_const_iff_forall_gt_measure_zero

[Joris van Winden]

Thanks! I guess I will hold off then

[Joris van Winden]

Since MeasureTheory.ae_le_const_iff_forall_gt_measure_zero is a bit awkward to use directly when manipulating a.e. inequalities, I decided to open #34375 anyway. The pull request also includes le/ge versions for when the linear ordering is dense.