Elementary tail bounds

Main results

• TauCeti.measureReal_le_abs_le_add: the tail event of an absolute value is the union of the upper and lower tails, so its measure is at most the sum of their measures.

theorem TauCeti.measureReal_le_abs_le_add {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → ℝ} {ε : ℝ} : μ.real {ω : Ω | ε ≤ |f ω|} ≤ μ.real {ω : Ω | ε ≤ f ω} + μ.real {ω : Ω | ε ≤ -f ω}

The measure of the event ε ≤ |f| is at most the sum of the measures of the upper tail ε ≤ f and the lower tail ε ≤ -f.