theorem Chapter11.cts_of_integ {a b : ℝ} {f : ℝ → ℝ} (hf : IntegrableOn f (BoundedInterval.Icc a b)) : ContinuousOn (fun (x : ℝ) => integ f (BoundedInterval.Icc a x)) (Set.Icc a b)

Theorem 11.9.1 (First Fundamental Theorem of Calculus).

theorem Chapter11.deriv_of_integ {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (hf : IntegrableOn f (BoundedInterval.Icc a b)) {x₀ : ℝ} (hx₀ : x₀ ∈ Set.Icc a b) (hcts : ContinuousWithinAt f (↑(BoundedInterval.Icc a b)) x₀) : HasDerivWithinAt (fun (x : ℝ) => integ f (BoundedInterval.Icc a x)) (f x₀) (Set.Icc a b) x₀

theorem Chapter11.IntegrableOn.of_f_9_8_5 : IntegrableOn Chapter9.f_9_8_5 (BoundedInterval.Icc 0 1)

Example 11.9.2

@[reducible, inline]

noncomputable abbrev Chapter11.F_11_9_2 (x : ℝ) : ℝ

Equations

• Chapter11.F_11_9_2 x = Chapter11.integ Chapter9.f_9_8_5 (Chapter11.BoundedInterval.Icc 0 x)

theorem Chapter11.ContinuousOn.of_F_11_9_2 : ContinuousOn F_11_9_2 (Set.Icc 0 1)

theorem Chapter11.DifferentiableOn.of_F_11_9_2 {x : ℝ} (hx : ¬∃ (r : ℚ), x = ↑r) (hx' : x ∈ Set.Icc 0 1) : DifferentiableWithinAt ℝ F_11_9_2 (Set.Icc 0 1) x

theorem Chapter11.DifferentiableOn.of_F_11_9_2' {q : ℚ} (hq : ↑q ∈ Set.Ioo 0 1) : ¬DifferentiableWithinAt ℝ F_11_9_2 (Set.Icc 0 1) ↑q

Exercise 11.9.1

@[reducible, inline]

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

Definition 11.9.3. We drop the requirement that x be a limit point as this makes the Lean arguments slightly cleaner

Equations

• Chapter11.AntiderivOn F f I = (DifferentiableOn ℝ F ↑I ∧ ∀ x ∈ I, HasDerivWithinAt F (f x) (↑I) x)

theorem Chapter11.AntiderivOn.mono {F f : ℝ → ℝ} {I J : BoundedInterval} (h : AntiderivOn F f I) (hIJ : J ⊆ I) : AntiderivOn F f J

theorem Chapter11.integ_eq_antideriv_sub {a b : ℝ} (h : a ≤ b) {f F : ℝ → ℝ} (hf : IntegrableOn f (BoundedInterval.Icc a b)) (hF : AntiderivOn F f (BoundedInterval.Icc a b)) : integ f (BoundedInterval.Icc a b) = F b - F a

Theorem 11.9.4 (Second Fundamental Theorem of Calculus)

@[reducible, inline]

noncomputable abbrev Chapter11.F_11_9 : ℝ → ℝ

Equations

• Chapter11.F_11_9 x = if x = 0 then 0 else x ^ 2 * Real.sin (1 / x ^ 3)

theorem Chapter11.antideriv_eq_antideriv_add_const {I : BoundedInterval} {f F G : ℝ → ℝ} (hfF : AntiderivOn F f I) (hfG : AntiderivOn G f I) : ∃ (C : ℝ), ∀ x ∈ ↑I, F x = G x + C

Lemma 11.9.5 / Exercise 11.9.2

theorem Chapter7.Series.converges_qseries' (p : ℝ) : (mk' fun (n : { n : ℤ // n ≥ 1 }) => 1 / ↑↑n ^ p).converges ↔ p > 1

Exercise 11.6.5, moved to Section 11.9

theorem Chapter7.Series.converges_qseries'' (p : ℝ) : (mk' fun (n : { n : ℤ // n ≥ 1 }) => 1 / ↑↑n ^ p).absConverges ↔ p > 1