Source indexedlemma · leanprover/lean4:v4.32.0

ae_disjoint_central_tail

PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:1001 to 1006

Mathematical statement

Exact Lean statement

lemma ae_disjoint_central_tail {δ : ℝ} :
    MeasureTheory.AEDisjoint MeasureTheory.volume (Set.Icc (-δ) δ) (Set.Icc (-Real.pi) (-δ) ∪ Set.Icc δ Real.pi)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ae_disjoint_central_tail {δ : ℝ} :    MeasureTheory.AEDisjoint MeasureTheory.volume (Set.Icc (-δ) δ) (Set.Icc (-Real.pi) (-δ) ∪ Set.Icc δ Real.pi) := by      -- The intersection of the central interval and the tail regions consists of the points $\{-\delta, \delta\}$, which have measure zero.      have h_inter : (Set.Icc (-δ) δ) ∩ ((Set.Icc (-Real.pi) (-δ)) ∪ (Set.Icc δ Real.pi)) ⊆ {-δ, δ} := by        grind;      exact MeasureTheory.measure_mono_null h_inter ( by exact MeasureTheory.measure_union_null ( MeasureTheory.measure_singleton _ ) ( MeasureTheory.measure_singleton _ ) )