theorem Chapter11.integ_of_uniform_cts {I : BoundedInterval} {f : ℝ → ℝ} (hf : UniformContinuousOn f ↑I) : IntegrableOn f I

Theorem 11.5.1

theorem Chapter11.integ_of_cts {a b : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f ↑(BoundedInterval.Icc a b)) : IntegrableOn f (BoundedInterval.Icc a b)

Corollary 11.5.2

theorem Chapter11.integ_of_bdd_cts {I : BoundedInterval} {f : ℝ → ℝ} (hbound : Chapter9.BddOn f ↑I) (hf : ContinuousOn f ↑I) : IntegrableOn f I

Proposition 11.5.3

@[reducible, inline]

abbrev Chapter11.PiecewiseContinuousOn (f : ℝ → ℝ) (I : BoundedInterval) : Prop

Definition 11.5.4

Equations

• Chapter11.PiecewiseContinuousOn f I = ∃ (P : Chapter11.Partition I), ∀ J ∈ P.intervals, ContinuousOn f ↑J

@[reducible, inline]

noncomputable abbrev Chapter11.f_11_5_5 : ℝ → ℝ

Example 11.5.5

Equations

• Chapter11.f_11_5_5 x = if x < 2 then x ^ 2 else if x = 2 then 7 else x ^ 3

theorem Chapter11.integ_of_bdd_piecewise_cts {I : BoundedInterval} {f : ℝ → ℝ} (hbound : Chapter9.BddOn f ↑I) (hf : PiecewiseContinuousOn f I) : IntegrableOn f I

Proposition 11.5.6 / Exercise 11.5.1

theorem Chapter11.integ_zero {a b : ℝ} (hab : a < b) (f : ℝ → ℝ) (hf : ContinuousOn f ↑(BoundedInterval.Icc a b)) (hnonneg : MajorizesOn f (fun (x : ℝ) => 0) (BoundedInterval.Icc a b)) (hinteg : integ f (BoundedInterval.Icc a b) = 0) (x : ℝ) : x ∈ BoundedInterval.Icc a b → f x = 0

Exercise 11.5.2