Documentation

Books.IntroductiontoRealAnalysisVolumeI_JiriLebl_2025.Chapters.Chap06.section02

def example6_2_1_fn (n : ) (x : ) :

Example 6.2.1: For each n, define fₙ : [0,1] → ℝ by fₙ(x) = 1 - n x when x < 1 / n and fₙ(x) = 0 when x ≥ 1 / n. Each fₙ is continuous, the pointwise limit is the function that is 1 at 0 and 0 for x > 0, and this limit is not continuous at 0.

Equations
Instances For

    The pointwise limit function in Example 6.2.1, equal to 1 at 0 and 0 elsewhere.

    Equations
    Instances For

      The sequence example6_2_1_fn n consists of continuous functions.

      theorem tendsto_example6_2_1_fn_of_pos {x : } (hx : 0 < x) :

      For any x > 0, the sequence example6_2_1_fn n x converges to 0.

      At x = 0, the sequence example6_2_1_fn n 0 converges to 1.

      The pointwise limit of example6_2_1_fn on [0, 1] is the function that is 1 at 0 and 0 elsewhere, and this limit function is not continuous at 0.

      theorem continuous_of_uniformLimit {S : Set } {f : S} {fSeq : S} (hcont : ∀ (n : ), Continuous (fSeq n)) (hlim : TendstoUniformly fSeq f Filter.atTop) :

      Theorem 6.2.2: If fₙ : S → ℝ is a sequence of continuous functions that converges uniformly to f : S → ℝ, then f is continuous.

      def example6_2_3_fn (n : ) (x : ) :

      Example 6.2.3: The sequence of piecewise linear functions fₙ : [0,1] → ℝ given by fₙ(0) = 0, fₙ(x) = (n + 1) - (n + 1)² x for 0 < x < 1 / (n + 1), and fₙ(x) = 0 for x ≥ 1 / (n + 1) is Riemann integrable with integral 1 / 2. The pointwise limit on [0,1] is the zero function, so lim_{n → ∞} ∫₀¹ fₙ = 1/2 while ∫₀¹ (lim_{n → ∞} fₙ) = 0.

      Equations
      Instances For
        theorem example6_2_3_integral_half (n : ) :
        (x : ) in 0..1, example6_2_3_fn n x = 1 / 2

        Each example6_2_3_fn n has integral 1/2 on the interval (0, 1].

        For any x ∈ [0,1], the sequence example6_2_3_fn n x converges to 0.

        theorem example6_2_3_integral_limit_ne_limit_integral :
        Filter.Tendsto (fun (n : ) => (x : ) in 0..1, example6_2_3_fn n x) Filter.atTop (nhds (1 / 2)) (∀ xSet.Icc 0 1, Filter.Tendsto (fun (n : ) => example6_2_3_fn n x) Filter.atTop (nhds 0)) 1 / 2 (x : ) in 0..1, 0

        The integrals of example6_2_3_fn n converge to 1/2, while the integral of the pointwise limit is 0, showing that pointwise convergence alone does not allow interchanging limit and integral.

        theorem integral_interval_tendsto_of_uniform_limit {a b : } {f : } {fSeq : } (hint : ∀ (n : ), IntervalIntegrable (fSeq n) MeasureTheory.volume a b) (hlim : TendstoUniformlyOn fSeq f Filter.atTop (Set.Icc a b)) (hab : a b) :
        IntervalIntegrable f MeasureTheory.volume a b Filter.Tendsto (fun (n : ) => (x : ) in a..b, fSeq n x) Filter.atTop (nhds ( (x : ) in a..b, f x))

        Theorem 6.2.4: If fₙ : [a, b] → ℝ is a sequence of Riemann integrable functions converging uniformly to f : [a, b] → ℝ, then f is Riemann integrable and the integral of the limit equals the limit of the integrals.

        theorem example6_2_5_abs_diff_le (n : ) (x : ) :
        |(n.succ * x + Real.sin (n.succ * x ^ 2)) / n.succ - x| 1 / n.succ
        theorem example6_2_5_tendsto_uniformlyOn :
        TendstoUniformlyOn (fun (n : ) (x : ) => (n.succ * x + Real.sin (n.succ * x ^ 2)) / n.succ) (fun (x : ) => x) Filter.atTop (Set.Icc 0 1)
        theorem example6_2_5_intervalIntegrable (n : ) :
        IntervalIntegrable (fun (x : ) => (n.succ * x + Real.sin (n.succ * x ^ 2)) / n.succ) MeasureTheory.volume 0 1
        theorem example6_2_5_integral_id :
        (x : ) in 0..1, x = 1 / 2
        theorem example6_2_5_integral_limit :
        Filter.Tendsto (fun (n : ) => (x : ) in 0..1, (n.succ * x + Real.sin (n.succ * x ^ 2)) / n.succ) Filter.atTop (nhds (1 / 2))

        Example 6.2.5: For fₙ(x) = ((n x) + sin (n x²)) / n on [0,1], the functions converge uniformly to x, so the integrals converge to the integral of the limit. Therefore lim_{n → ∞} ∫₀¹ ((n x + sin (n x²)) / n) = 1 / 2.

        def example6_2_6_fn (n : ) (x : ) :

        Example 6.2.6: The functions fₙ : [0, 1] → ℝ are 1 at rationals whose reduced denominator is at most n and 0 otherwise. Each fₙ is Riemann integrable with integral 0, the sequence converges pointwise to the Dirichlet function that is 1 on and 0 on irrationals, and this limit is not Riemann integrable.

        Equations
        Instances For

          The pointwise limit in Example 6.2.6 is the Dirichlet function, equal to 1 on rational points and 0 on irrational points.

          Equations
          Instances For

            Each function in the sequence from Example 6.2.6 is Riemann integrable on [0, 1] with integral 0.

            The sequence example6_2_6_fn n converges pointwise to the Dirichlet function on [0, 1].

            The Dirichlet function on [0, 1] is not Riemann integrable.

            def example6_2_7_fn (n : ) (x : ) :

            Example 6.2.7: The functions fₙ : [0,1] → ℝ are given by fₙ(x) = 0 for x < 1 / (n + 1) and fₙ(x) = 1 / x otherwise. Each fₙ is bounded on [0, 1] by n + 1, but the pointwise limit f(x) = 0 for x = 0 and f(x) = 1 / x otherwise is unbounded.

            Equations
            Instances For

              The pointwise limit function in Example 6.2.7, equal to 0 at 0 and 1 / x for x ≠ 0.

              Equations
              Instances For
                theorem example6_2_7_fn_bounded (n : ) (x : ) :
                x Set.Icc 0 1|example6_2_7_fn n x| n.succ

                Each function from Example 6.2.7 is bounded on [0, 1] by n + 1.

                The sequence in Example 6.2.7 converges pointwise on [0, 1] to the function that is 0 at 0 and 1 / x elsewhere.

                theorem example6_2_7_limit_unbounded :
                ¬∃ (C : ), xSet.Icc 0 1, |example6_2_7_limit x| C

                The pointwise limit in Example 6.2.7 is unbounded on [0, 1].

                def example6_2_8_fn (n : ) (x : ) :

                Example 6.2.8: The functions fₙ(x) = sin ((n + 1) x) / (n + 1) converge uniformly to 0, whose derivative is 0. The derivatives fₙ'(x) = cos ((n + 1) x) do not converge pointwise: at π they oscillate between 1 and -1, and at 0 they are constantly 1, not approaching 0.

                Equations
                Instances For
                  theorem example6_2_8_abs_le (n : ) (x : ) :
                  theorem example6_2_8_uniform_tendsto_zero :
                  TendstoUniformly (fun (n : ) (x : ) => example6_2_8_fn n x) (fun (x : ) => 0) Filter.atTop

                  The sequence from Example 6.2.8 converges uniformly to the zero function.

                  theorem example6_2_8_deriv_limit (x : ) :
                  deriv (fun (x : ) => 0) x = 0

                  The derivative of the uniform limit in Example 6.2.8 is identically zero.

                  theorem example6_2_8_deriv (n : ) (x : ) :
                  deriv (fun (y : ) => example6_2_8_fn n y) x = Real.cos (n.succ * x)

                  Each function in Example 6.2.8 has derivative cos ((n + 1) x).

                  At π, the derivatives in Example 6.2.8 oscillate and do not converge.

                  theorem example6_2_8_deriv_at_zero :
                  Filter.Tendsto (fun (n : ) => deriv (fun (y : ) => example6_2_8_fn n y) 0) Filter.atTop (nhds 1)

                  At 0, the derivatives in Example 6.2.8 are constantly 1, so the sequence does not approach 0.

                  def example6_2_9_fn (n : ) (x : ) :

                  Example 6.2.9: Let fₙ(x) = 1 / (1 + n x²). For x ≠ 0, fₙ(x) converges to 0, while fₙ(0) converges to 1, so the pointwise limit is not continuous at 0. The derivatives are fₙ'(x) = - 2 n x / (1 + n x²)², which converge pointwise to 0 but not uniformly on any interval containing 0. The limit function fails to be differentiable at 0.

                  Equations
                  Instances For

                    Pointwise limit function in Example 6.2.9, equal to 1 at 0 and 0 elsewhere.

                    Equations
                    Instances For

                      For x ≠ 0, example6_2_9_fn n x converges to 0 as n → ∞.

                      At x = 0, the sequence example6_2_9_fn n 0 converges to 1.

                      The pointwise limit of Example 6.2.9 is not continuous at 0.

                      theorem example6_2_9_deriv (n : ) (x : ) :
                      deriv (fun (y : ) => example6_2_9_fn n y) x = -2 * n.succ * x / (1 + n.succ * x ^ 2) ^ 2

                      Derivative formula for the functions in Example 6.2.9.

                      theorem example6_2_9_deriv_tendsto_zero (x : ) :
                      Filter.Tendsto (fun (n : ) => deriv (fun (y : ) => example6_2_9_fn n y) x) Filter.atTop (nhds 0)

                      For every x, the derivatives in Example 6.2.9 converge pointwise to 0.

                      theorem example6_2_9_deriv_not_uniform :
                      ¬∃ (a : ) (b : ), a < 0 0 < b TendstoUniformlyOn (fun (n : ) (x : ) => deriv (fun (y : ) => example6_2_9_fn n y) x) (fun (x : ) => 0) Filter.atTop (Set.Icc a b)

                      The derivatives from Example 6.2.9 do not converge uniformly on any interval containing 0.

                      The pointwise limit in Example 6.2.9 is not differentiable at 0.

                      theorem uniform_limit_of_uniform_deriv {a b : } (fSeq : ) (g : ) (c : ) (hcont : ∀ (n : ), ContDiffOn 1 (fSeq n) (Set.Icc a b)) (hderiv : TendstoUniformlyOn (fun (n : ) (x : ) => derivWithin (fSeq n) (Set.Icc a b) x) g Filter.atTop (Set.Icc a b)) (hc : c Set.Icc a b) (hval : ∃ (l : ), Filter.Tendsto (fun (n : ) => fSeq n c) Filter.atTop (nhds l)) :
                      ∃ (f : ), ContDiffOn 1 f (Set.Icc a b) TendstoUniformlyOn fSeq f Filter.atTop (Set.Icc a b) xSet.Icc a b, derivWithin f (Set.Icc a b) x = g x

                      Theorem 6.2.10: Let I be a bounded interval and let fₙ : I → ℝ be continuously differentiable functions. If the derivatives fₙ' converge uniformly on I to g and the sequence of values fₙ(c) converges for some c ∈ I, then fₙ converges uniformly on I to a continuously differentiable function f with derivative f' = g.

                      theorem powerSeries_uniform_on_compact {a : } {c : } {ρ r : } (hr : 0 < r) (hrρ : r < ρ) (hconv : xSet.Icc (a - ρ) (a + ρ), Summable fun (n : ) => c n * (x - a) ^ n) :
                      TendstoUniformlyOn (fun (N : ) (x : ) => nFinset.range N, c n * (x - a) ^ n) (fun (x : ) => ∑' (n : ), c n * (x - a) ^ n) Filter.atTop (Set.Icc (a - r) (a + r))

                      Proposition 6.2.11: A power series ∑ cₙ (x - a)^n with radius of convergence ρ > 0 converges uniformly on [a - r, a + r] for every 0 < r < ρ. As a consequence, the sum defines a continuous function on the open interval where the series converges (or on all of if ρ = ∞).

                      theorem powerSeries_sum_continuous {a : } {c : } {ρ : } (hconv : xSet.Ioo (a - ρ) (a + ρ), Summable fun (n : ) => c n * (x - a) ^ n) :
                      ContinuousOn (fun (x : ) => ∑' (n : ), c n * (x - a) ^ n) (Set.Ioo (a - ρ) (a + ρ))

                      A convergent power series ∑ cₙ (x - a)^n defines a continuous function on the open interval of convergence, or on all of when the radius is infinite.

                      @[simp]
                      theorem abs_nat_succ_real (n : ) :
                      |n.succ| = n.succ
                      theorem integral_powerSeries_eq_series {a ρ : } {c : } ( : 0 < ρ) (hconv : xSet.Ioo (a - ρ) (a + ρ), Summable fun (n : ) => c n * (x - a) ^ n) (x : ) :
                      x Set.Ioo (a - ρ) (a + ρ) (t : ) in a..x, ∑' (n : ), c n * (t - a) ^ n = ∑' (n : ), c n / n.succ * (x - a) ^ n.succ

                      Corollary 6.2.12: For a convergent power series ∑_{n=0}^∞ cₙ (x - a)^n with radius of convergence ρ > 0, if I is the interval (a - ρ, a + ρ) (or when ρ = ∞) and f denotes the limit, then for every x ∈ I one has ∫ₐˣ f = ∑_{n=1}^∞ (c_{n-1} / n) (x - a)^n, and the radius of convergence of the latter series is at least ρ.

                      theorem deriv_powerSeries_eq_series {a ρ : } {c : } (hconv : xSet.Ioo (a - ρ) (a + ρ), Summable fun (n : ) => c n * (x - a) ^ n) (x : ) :
                      x Set.Ioo (a - ρ) (a + ρ)DifferentiableAt (fun (y : ) => ∑' (n : ), c n * (y - a) ^ n) x deriv (fun (y : ) => ∑' (n : ), c n * (y - a) ^ n) x = ∑' (n : ), n.succ * c n.succ * (x - a) ^ n Summable fun (n : ) => n.succ * c n.succ * (x - a) ^ n

                      Corollary 6.2.13: For a convergent power series ∑_{n=0}^∞ cₙ (x - a)^n with radius of convergence ρ > 0, let I = (a - ρ, a + ρ). If f is its sum on I, then f is differentiable on I and f' (x) = ∑_{n=0}^∞ (n + 1) c_{n+1} (x - a)^n, whose radius of convergence is also ρ.

                      Example 6.2.14: The power series ∑ x^n / n! has infinite radius of convergence, so it defines a function f(x) = ∑ x^n / n! on all real numbers. It satisfies f(0) = 1, differentiates term by term to give f' = f, and coincides with the usual exponential function.

                      Equations
                      Instances For
                        theorem example6_2_14_summable (x : ) :
                        Summable fun (n : ) => x ^ n / n.factorial
                        theorem example6_2_15_series_closed_form {x : } (hx : x Set.Ioo (-1) 1) :
                        ∑' (n : ), n.succ * x ^ n.succ = x / (1 - x) ^ 2

                        Example 6.2.15: For x ∈ (-1, 1), the series ∑_{n=1}^∞ n x^n converges to x / (1 - x)^2, obtained by differentiating the geometric series and multiplying by x.