def TaoRiemannIntegrableOn (I : Set ℝ) (f : ℝ → ℝ) : Prop

Tao's book-level predicate asserting that f is Riemann integrable on a bounded interval I.

noncomputable def riemannIntegralOn (I : Set ℝ) (f : ℝ → ℝ) : ℝ

The Riemann integral of f over a bounded interval I.

theorem helperForProposition_8_13_integrableOn_of_riemann {I : Set ℝ} {f : ℝ → ℝ} (hriemann : TaoRiemannIntegrableOn I f) : MeasureTheory.IntegrableOn f I MeasureTheory.volume

Helper for Proposition 8.13: unpacking TaoRiemannIntegrableOn yields IntegrableOn.

theorem helperForProposition_8_13_aemeasurable_of_riemann {I : Set ℝ} {f : ℝ → ℝ} (hriemann : TaoRiemannIntegrableOn I f) : AEMeasurable f (MeasureTheory.volume.restrict I)

Helper for Proposition 8.13: a Riemann-integrable function is a.e.-measurable on I.

theorem proposition_8_13 {I : Set ℝ} (hinterval : I.OrdConnected) (hbounded : Bornology.IsBounded I) {f : ℝ → ℝ} (hriemann : TaoRiemannIntegrableOn I f) : AEMeasurable f (MeasureTheory.volume.restrict I) ∧ MeasureTheory.IntegrableOn f I MeasureTheory.volume ∧ ∫ (x : ℝ) in I, f x = riemannIntegralOn I f

Proposition 8.13: Let I ⊆ ℝ be a bounded interval, and let f : I → ℝ be Riemann integrable. Then f is Lebesgue measurable and Lebesgue integrable on I, and the Lebesgue integral on I equals the Riemann integral on I.

theorem helperForProposition_8_14_rationalRange_measure_zero : MeasureTheory.volume (Set.range Rat.cast) = 0

Helper for Proposition 8.14: the set of rational real numbers has Lebesgue measure zero.

theorem helperForProposition_8_14_ae_zero_on_interval : ((Set.range Rat.cast).indicator fun (x : ℝ) => 1) =ᵐ[MeasureTheory.volume.restrict (Set.Icc 0 1)] fun (x : ℝ) => 0

Helper for Proposition 8.14: the Dirichlet function is almost everywhere zero on [0,1].

theorem helperForProposition_8_14_integrableOn : MeasureTheory.IntegrableOn ((Set.range Rat.cast).indicator fun (x : ℝ) => 1) (Set.Icc 0 1) MeasureTheory.volume

Helper for Proposition 8.14: the Dirichlet function is integrable on [0,1].

theorem helperForProposition_8_14_integral_eq_zero : ∫ (x : ℝ) in Set.Icc 0 1, (Set.range Rat.cast).indicator (fun (x : ℝ) => 1) x = 0

Helper for Proposition 8.14: the integral of the Dirichlet function over [0,1] is zero.

theorem proposition_8_14 : have f := (Set.range Rat.cast).indicator fun (x : ℝ) => 1; MeasureTheory.IntegrableOn f (Set.Icc 0 1) MeasureTheory.volume ∧ ∫ (x : ℝ) in Set.Icc 0 1, f x = 0

Proposition 8.14: Define f : [0,1] → ℝ by f(x) = 1 for rational x and f(x) = 0 for irrational x. Then f is Lebesgue integrable on [0,1] and ∫_[0,1] f dμ = 0, where μ is Lebesgue measure.