Documentation

Analysis.Section_11_9

Analysis I, Section 11.9: The two fundamental theorems of calculus #

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

source
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)

source
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₀
source
theorem Chapter11.IntegrableOn.of_f_9_8_5 :
IntegrableOn Chapter9.f_9_8_5 (BoundedInterval.Icc 0 1)

Example 11.9.2

source
@[reducible, inline]
noncomputable abbrev Chapter11.F_11_9_2 (x : ℝ) :
ℝ
Equations
Instances For
    source
    theorem Chapter11.ContinuousOn.of_F_11_9_2 :
    ContinuousOn F_11_9_2 (Set.Icc 0 1)
    source
    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
    source
    theorem Chapter11.DifferentiableOn.of_F_11_9_2' {q : ℚ} (hq : ↑q ∈ Set.Icc 0 1) :
    ¬DifferentiableWithinAt ℝ F_11_9_2 (Set.Icc 0 1) ↑q

    Exercise 11.9.1

    source
    @[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
    Instances For
      source
      theorem Chapter11.AntiderivOn.mono {F f : ℝ → ℝ} {I J : BoundedInterval} (h : AntiderivOn F f I) (hIJ : J ⊆ I) :
      AntiderivOn F f J
      source
      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)

      source
      @[reducible, inline]
      noncomputable abbrev Chapter11.F_11_9 :
      ℝ → ℝ
      Equations
      Instances For
        source
        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

        source
        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

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