Lumenary.IntroCalculus

Formal library

• diff_quotient_sqtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **The difference quotient of `x²`.** For `h ≠ 0`,
  `((a + h)² − a²)/h = (2ah + h²)/h = 2a + h`. -/
  theorem diff_quotient_sq (a h : ℝ) (hh : h ≠ 0) : ((a + h) ^ 2 - a ^ 2) / h = 2 * a + h := by
    field_simp
    ring

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• tendsto_diff_quotient_sqtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Its limit is `2a`.** As `h → 0` with `h ≠ 0`, the quotient equals `2a + h`, and
  `2a + h → 2a`. The value at `h = 0` itself is never used. -/
  theorem tendsto_diff_quotient_sq (a : ℝ) :
      Tendsto (fun h => ((a + h) ^ 2 - a ^ 2) / h) (𝓝[≠] 0) (𝓝 (2 * a)) := by
    have hlin : Tendsto (fun h : ℝ => 2 * a + h) (𝓝[≠] 0) (𝓝 (2 * a)) := by
      have : Tendsto (fun h : ℝ => 2 * a + h) (𝓝 0) (𝓝 (2 * a + 0)) :=
        tendsto_const_nhds.add tendsto_id
      rw [add_zero] at this
      exact tendsto_nhdsWithin_of_tendsto_nhds this
    refine tendsto_nhdsWithin_congr (fun h hh => ?_) hlin
    exact (diff_quotient_sq a h hh).symm

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• hasDerivAt_sqtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **`(x²)′ = 2a` at every point `a`**, from the limit definition: Mathlib's `HasDerivAt` is
  equivalent (`hasDerivAt_iff_tendsto_slope_zero`) to the difference quotients tending to the
  derivative, and we computed that limit above. -/
  theorem hasDerivAt_sq (a : ℝ) : HasDerivAt (fun x : ℝ => x ^ 2) (2 * a) a := by
    rw [hasDerivAt_iff_tendsto_slope_zero]
    refine (tendsto_diff_quotient_sq a).congr (fun t => ?_)
    simp [smul_eq_mul, div_eq_inv_mul]

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• power_ruletheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **The power rule** `(xⁿ⁺¹)′ = (n + 1) xⁿ`, by induction on `n`.
  For `n = 0`, `(x¹)′ = 1`. For the step write `x^(n+2) = x^(n+1) · x` and use the product rule
  `(uv)′ = u′v + uv′`: the derivative is `(n + 1)xⁿ · x + x^(n+1) · 1 = (n + 2) x^(n+1)`.
  (We write the exponent as `n + 1` so that the rule never needs `n − 1`.) -/
  theorem power_rule (n : ℕ) (x : ℝ) :
      HasDerivAt (fun y : ℝ => y ^ (n + 1)) ((n + 1) * x ^ n) x := by
    induction n with
    | zero => simpa using hasDerivAt_id' x
    | succ k ih =>
      have h := ih.mul (hasDerivAt_id x)
      have hf : (fun y : ℝ => y ^ (k + 1 + 1)) = (fun y : ℝ => y ^ (k + 1)) * id := by
        funext y
        simp [pow_succ]
      rw [hf]
      convert h using 1
      push_cast
      simp only [id]
      ring

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• power_rule_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- The power rule from Mathlib, `hasDerivAt_pow`: `(xⁿ)′ = n xⁿ⁻¹` (with natural-number
  subtraction, so for `n = 0` it reads `(x⁰)′ = 0 · x^0 = 0`, which is still correct). -/
  theorem power_rule_library (n : ℕ) (x : ℝ) :
      HasDerivAt (fun y : ℝ => y ^ n) (n * x ^ (n - 1)) x :=
    hasDerivAt_pow n x

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• fermattheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Fermat's theorem on interior extrema:** if `f` has a local maximum or minimum at `a` and is
  differentiable there, then `f′(a) = 0`. This applies Mathlib's
  `IsLocalExtr.hasDerivAt_eq_zero`. -/
  theorem fermat {f : ℝ → ℝ} {a f' : ℝ} (hext : IsLocalExtr f a) (hd : HasDerivAt f f' a) :
      f' = 0 :=
    hext.hasDerivAt_eq_zero hd

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• cube_deriv_zerotheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- `x³` has derivative `3 · 0² = 0` at `0` (the power rule with `n = 2`). -/
  theorem cube_deriv_zero : HasDerivAt (fun x : ℝ => x ^ 3) 0 0 := by
    have h := power_rule 2 0
    norm_num at h
    exact h

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• cube_not_extremumtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **The converse of Fermat's theorem is false.** `x³` has `f′(0) = 0`, but `0` is neither a
  local maximum nor a local minimum: however small an interval around `0` we take, it contains a
  point `t > 0` with `t³ > 0 = f(0)` and the point `−t` with `(−t)³ < 0`. -/
  theorem cube_not_extremum : ¬ IsLocalExtr (fun x : ℝ => x ^ 3) 0 := by
    rintro (hmin | hmax)
    · -- A local minimum would need `x³ ≥ 0` near `0`; `x = −ε/2` breaks it.
      obtain ⟨ε, hε, h⟩ := Metric.eventually_nhds_iff.mp hmin
      have hd : dist (-(ε / 2)) 0 < ε := by
        rw [Real.dist_eq, sub_zero, abs_neg, abs_of_pos (by linarith)]
        linarith
      have := h hd
      simp only at this
      nlinarith [pow_pos (half_pos hε) 3]
    · -- A local maximum would need `x³ ≤ 0` near `0`; `x = ε/2` breaks it.
      obtain ⟨ε, hε, h⟩ := Metric.eventually_nhds_iff.mp hmax
      have hd : dist (ε / 2) 0 < ε := by
        rw [Real.dist_eq, sub_zero, abs_of_pos (by linarith)]
        linarith
      have := h hd
      simp only at this
      nlinarith [pow_pos (half_pos hε) 3]

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• limit_not_valuetheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **The limit at a point need not be the value there.** `f(x) = (x² − 1)/(x − 1)` tends to `2`
  as `x → 1`, because `f(x) = x + 1` for `x ≠ 1`. At `x = 1` the formula reads `0/0`, which is
  meaningless on paper; Lean's convention `0/0 = 0` gives `f(1) = 0` — a value that has nothing to
  do with the limit `2`. -/
  theorem limit_not_value :
      Tendsto (fun x : ℝ => (x ^ 2 - 1) / (x - 1)) (𝓝[≠] 1) (𝓝 2) ∧
        (fun x : ℝ => (x ^ 2 - 1) / (x - 1)) 1 = 0 := by
    constructor
    · have hlin : Tendsto (fun x : ℝ => x + 1) (𝓝[≠] 1) (𝓝 2) := by
        have : Tendsto (fun x : ℝ => x + 1) (𝓝 1) (𝓝 (1 + 1)) :=
          tendsto_id.add tendsto_const_nhds
        norm_num at this
        exact tendsto_nhdsWithin_of_tendsto_nhds this
      refine tendsto_nhdsWithin_congr (fun x hx => ?_) hlin
      have hx1 : x - 1 ≠ 0 := sub_ne_zero.mpr hx
      field_simp
      ring
    · norm_num

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• sum_squarestheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- `0² + 1² + ⋯ + n² = n(n + 1)(2n + 1)/6`, by induction on `n`. -/
  theorem sum_squares (n : ℕ) :
      ∑ k ∈ range (n + 1), (k : ℝ) ^ 2 = n * (n + 1) * (2 * n + 1) / 6 := by
    induction n with
    | zero => simp
    | succ m ih =>
      rw [sum_range_succ, ih]
      push_cast
      ring

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• rightSumdefDefinitionpropext, Classical.choice, Quot.sound

  /-- The **right Riemann sum** of `f(x) = x²` on `[0, 1]` with `n` strips of width `1/n`: the
  strip over `[k/n, (k + 1)/n]` has height `f((k + 1)/n)`. -/
  noncomputable def rightSum (n : ℕ) : ℝ :=
    ∑ k ∈ range n, (((k : ℝ) + 1) / n) ^ 2 * (1 / n)

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• rightSum_formulatheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **A closed form for the Riemann sum:** for `n ≥ 1`,
  `rightSum n = (1² + 2² + ⋯ + n²)/n³ = (n + 1)(2n + 1)/(6n²)`. -/
  theorem rightSum_formula (n : ℕ) (hn : n ≠ 0) :
      rightSum n = ((n : ℝ) + 1) * (2 * n + 1) / (6 * (n : ℝ) ^ 2) := by
    have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn
    have key : ∑ k ∈ range n, ((k : ℝ) + 1) ^ 2 = (n : ℝ) * (n + 1) * (2 * n + 1) / 6 := by
      have h := sum_squares n
      rw [sum_range_succ'] at h
      simpa using h
    have hsum : rightSum n = (∑ k ∈ range n, ((k : ℝ) + 1) ^ 2) / (n : ℝ) ^ 3 := by
      rw [rightSum, sum_div]
      refine sum_congr rfl (fun k _ => ?_)
      field_simp
    rw [hsum, key]
    field_simp

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• rightSum_tendstotheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **The Riemann sums converge to `1/3`.** For `n ≥ 1`,
  `(n + 1)(2n + 1)/(6n²) = (1 + 1/n)(2 + 1/n)/6`, and `1/n → 0`, so the limit is
  `(1 · 2)/6 = 1/3`: the area under `y = x²` from `0` to `1`. -/
  theorem rightSum_tendsto : Tendsto rightSum atTop (𝓝 (1 / 3)) := by
    have hlim : Tendsto (fun n : ℕ => (1 + 1 / (n : ℝ)) * (2 + 1 / (n : ℝ)) / 6) atTop
        (𝓝 ((1 + 0) * (2 + 0) / 6)) :=
      ((tendsto_const_nhds.add tendsto_one_div_atTop_nhds_zero_nat).mul
        (tendsto_const_nhds.add tendsto_one_div_atTop_nhds_zero_nat)).div_const 6
    norm_num at hlim
    refine hlim.congr' ?_
    filter_upwards [eventually_ne_atTop 0] with n hn
    have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn
    rw [rightSum_formula n hn]
    field_simp

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• ftc_squaretheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **The fundamental theorem in action:** `∫₀² x² dx = 8/3`. Since `F(x) = x³/3` has
  `F′(x) = x²`, the integral is `F(2) − F(0) = 8/3`. This applies Mathlib's fundamental theorem
  `intervalIntegral.integral_eq_sub_of_hasDerivAt`. -/
  theorem ftc_square : ∫ x in (0 : ℝ)..2, x ^ 2 = 8 / 3 := by
    have hF : ∀ x ∈ Set.uIcc (0 : ℝ) 2, HasDerivAt (fun y : ℝ => y ^ 3 / 3) (x ^ 2) x := by
      intro x _
      have h := (hasDerivAt_pow 3 x).div_const 3
      convert h using 1
      norm_num
    have hint : IntervalIntegrable (fun x : ℝ => x ^ 2) MeasureTheory.volume 0 2 :=
      (continuous_pow 2).intervalIntegrable 0 2
    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF hint]
    norm_num

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• integral_sq_unittheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- `∫₀¹ x² dx = 1/3`, the limit of the Riemann sums above, from Mathlib's `integral_pow`. -/
  theorem integral_sq_unit : ∫ x in (0 : ℝ)..1, x ^ 2 = 1 / 3 := by
    rw [integral_pow]
    norm_num

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

• integral_sin_signedtheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Integrals are signed.** `∫₀^{2π} sin x dx = cos 0 − cos 2π = 0`: the area above the axis
  on `[0, π]` cancels the area below it on `[π, 2π]`. This applies Mathlib's `integral_sin`. -/
  theorem integral_sin_signed : ∫ x in (0 : ℝ)..(2 * Real.pi), Real.sin x = 0 := by
    rw [integral_sin]
    simp

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/IntroCalculus.leanTry it in the Lean web editor

Formal exercises

Each exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.

/-- Simplify the difference quotient of `x²`. Hint: `field_simp` clears the denominator `h`
(it uses `hh : h ≠ 0`), and `ring` finishes. -/
theorem diff_quotient_sq (a h : ℝ) (hh : h ≠ 0) : ((a + h) ^ 2 - a ^ 2) / h = 2 * a + h := by
  sorry

/-- **The difference quotient of `x²`.** For `h ≠ 0`,
`((a + h)² − a²)/h = (2ah + h²)/h = 2a + h`. -/
theorem diff_quotient_sq (a h : ℝ) (hh : h ≠ 0) : ((a + h) ^ 2 - a ^ 2) / h = 2 * a + h := by
  field_simp
  ring

/-- Prove the formula for the sum of the first squares by induction.
Hint: `induction n with | zero => simp | succ m ih => ?_`; in the step use `sum_range_succ`,
then `ih`, `push_cast` and `ring`. -/
theorem sum_squares (n : ℕ) :
    ∑ k ∈ range (n + 1), (k : ℝ) ^ 2 = n * (n + 1) * (2 * n + 1) / 6 := by
  sorry

/-- `0² + 1² + ⋯ + n² = n(n + 1)(2n + 1)/6`, by induction on `n`. -/
theorem sum_squares (n : ℕ) :
    ∑ k ∈ range (n + 1), (k : ℝ) ^ 2 = n * (n + 1) * (2 * n + 1) / 6 := by
  induction n with
  | zero => simp
  | succ m ih =>
    rw [sum_range_succ, ih]
    push_cast
    ring