Documentation

Books.IntroductiontoRealAnalysisVolumeI_JiriLebl_2025.Chapters.Chap03.section02

def continuousAtInSet (S : Set ) (f : S) (c : S) :

Definition 3.2.1. A function f : S → ℝ is continuous at a point c ∈ S if for every ε > 0 there exists δ > 0 such that whenever x ∈ S satisfies |x - c| < δ, then |f x - f c| < ε. A function is continuous on S if it is continuous at every point of S.

Equations
Instances For
    def continuousOnSet (S : Set ) (f : S) :

    A function f : S → ℝ is continuous on S when it is continuous at every point of S.

    Equations
    Instances For
      theorem continuousAtInSet_iff (S : Set ) (f : S) (c : S) :

      The epsilon-delta continuity at a point agrees with mathlib's notion of continuity for subtype domains.

      theorem continuousOnSet_iff (S : Set ) (f : S) :

      Continuity on a set agrees with mathlib's Continuous for functions defined on a subtype of .

      theorem proposition_3_2_2 (S : Set ) (f : S) (c : S) :
      (cclosure (S \ {c})ContinuousAt f c) (c closure (S \ {c}) → (ContinuousAt f c Filter.Tendsto f (nhds c) (nhds (f c)))) (ContinuousAt f c ∀ (u : S), Filter.Tendsto (fun (n : ) => (u n)) Filter.atTop (nhds c)Filter.Tendsto (fun (n : ) => f (u n)) Filter.atTop (nhds (f c)))

      Proposition 3.2.2. For a function f : S → ℝ on a set S ⊆ ℝ and a point c ∈ S: (i) if c is not a cluster point of S, then f is continuous at c; (ii) if c is a cluster point of S, then f is continuous at c if and only if \lim_{x \to c} f x = f c; (iii) f is continuous at c if and only if for every sequence (x_n) ⊆ S with x_n → c, one has f (x_n) → f c.

      theorem subtype_pos_ne_zero (x : { x : // 0 < x }) :
      x 0

      Elements of the positive real subtype are nonzero.

      theorem continuousAt_inv_subtype (c : { x : // 0 < x }) :
      ContinuousAt (fun (x : { x : // 0 < x }) => (↑x)⁻¹) c

      The reciprocal map is continuous at every point of (0, ∞).

      theorem example_3_2_3 :
      Continuous fun (x : { x : // 0 < x }) => (↑x)⁻¹

      Example 3.2.3. The reciprocal function f : (0, ∞) → ℝ given by f x = 1 / x is continuous on its domain.

      Proposition 3.2.4. A real polynomial f(x) = a_d x^d + a_{d-1} x^{d-1} + ⋯ + a_1 x + a_0 defines a continuous function ℝ → ℝ.

      theorem proposition_3_2_5 {S : Set } {f g : S} {c : S} (hf : ContinuousAt f c) (hg : ContinuousAt g c) (h0 : ∀ (x : S), g x 0) :
      ContinuousAt (fun (x : S) => f x + g x) c ContinuousAt (fun (x : S) => f x - g x) c ContinuousAt (fun (x : S) => f x * g x) c ContinuousAt (fun (x : S) => f x / g x) c

      Proposition 3.2.5. If f, g : S → ℝ are continuous at c ∈ S, then: (i) the sum x ↦ f x + g x is continuous at c; (ii) the difference x ↦ f x - g x is continuous at c; (iii) the product x ↦ f x * g x is continuous at c; (iv) if additionally g x ≠ 0 for all x ∈ S, the quotient x ↦ f x / g x is continuous at c.

      theorem sin_is_continuous :
      Continuous fun (x : ) => Real.sin x

      Example 3.2.6. The sine and cosine functions on are continuous. The book justifies this using trigonometric identities and the estimates |sin x| ≤ |x|, |cos x| ≤ 1, and |sin x| ≤ 1.

      theorem example_3_2_6 :
      (Continuous fun (x : ) => Real.sin x) Continuous fun (x : ) => Real.cos x
      theorem comp_continuousAt_helper {A B : Set } {f : B} {g : AB} {c : A} (hf : ContinuousAt f (g c)) (hg : ContinuousAt g c) :
      ContinuousAt (fun (x : A) => f (g x)) c

      Helper lemma for Proposition 3.2.7: composing hf and hg gives the desired continuity conclusion.

      theorem composition_continuousAt {A B : Set } {f : B} {g : AB} {c : A} (hg : ContinuousAt g c) (hf : ContinuousAt f (g c)) :
      ContinuousAt (fun (x : A) => f (g x)) c

      Proposition 3.2.7. If g : A → B is continuous at c ∈ A and f : B → ℝ is continuous at g c, then the composition f ∘ g : A → ℝ is continuous at c.

      theorem continuousOn_inv_Ioi :
      ContinuousOn (fun (x : ) => 1 / x) (Set.Ioi 0)

      The reciprocal map is continuous on (0, ∞) when regarded as a function ℝ → ℝ.

      theorem continuousOn_sin_inv :
      ContinuousOn (fun (x : ) => Real.sin (1 / x)) (Set.Ioi 0)

      Composing the reciprocal with the sine function yields a continuous function on (0, ∞).

      theorem example_3_2_8 :
      ContinuousOn (fun (x : ) => Real.sin (1 / x) ^ 2) (Set.Ioi 0)

      Example 3.2.8. The function x ↦ (sin (1 / x))^2 is continuous on the open interval (0, ∞).

      theorem proposition_3_2_9 {S : Set } {f : S} {c : S} (h : ∃ (u : S), Filter.Tendsto (fun (n : ) => (u n)) Filter.atTop (nhds c) ¬Filter.Tendsto (fun (n : ) => f (u n)) Filter.atTop (nhds (f c))) :

      Proposition 3.2.9. If there exists a sequence (x_n) in S converging to c such that (f (x_n)) does not converge to f c, then f is discontinuous at c.

      theorem neg_one_pow_even_real (m : ) :
      (-1) ^ (2 * m) = 1

      Explicit values of even powers of -1 in .

      theorem neg_one_pow_odd_real (m : ) :
      (-1) ^ (2 * m + 1) = -1

      Explicit values of odd powers of -1 in .

      noncomputable def jumpDiscontinuity (x : ) :

      Example 3.2.10. The function f : ℝ → ℝ given by f x = -1 for x < 0 and f x = 1 for x ≥ 0 has a jump discontinuity at 0. The left-limit along x_n = -1 / n is -1, the right-limit along x_n = 1 / n is 1, and along the alternating sequence x_n = (-1)^n / n the values oscillate and diverge.

      Equations
      Instances For
        theorem jumpDiscontinuity_of_neg {x : } (hx : x < 0) :
        noncomputable def dirichlet (x : ) :

        Example 3.2.11. The Dirichlet function f : ℝ → ℝ defined by f x = 1 when x is rational and f x = 0 when x is irrational is discontinuous at every real number.

        Equations
        Instances For
          theorem dirichlet_value_rational {x : } (hx : ∃ (q : ), q = x) :
          theorem dirichlet_value_irrational {x : } (hx : ¬∃ (q : ), q = x) :
          theorem dirichlet_irrational_seq_at_rational {c : } (hc : ∃ (q : ), q = c) :
          ∃ (u : ), Filter.Tendsto u Filter.atTop (nhds c) ∀ (n : ), Irrational (u n)
          theorem dirichlet_rational_seq_at_irrational {c : } (hc : Irrational c) :
          ∃ (v : ), Filter.Tendsto v Filter.atTop (nhds c) ∀ (n : ), ∃ (q : ), q = v n
          noncomputable def popcorn (x : ) :

          Example 3.2.12. The popcorn (Thomae) function on (0, 1) is defined by f (m / k) = 1 / k when m, k ∈ ℕ are coprime and m / k is in lowest terms, and f x = 0 when x is irrational. It is continuous at every irrational c ∈ (0, 1) and discontinuous at every rational c ∈ (0, 1).

          Equations
          Instances For
            theorem finite_small_denom_rationals (K : ) :
            {x : | x Set.Icc 0 1 ∃ (q : ), q = x q.den K}.Finite
            theorem popcorn_discontinuous_at_rational {c : } (hc0 : 0 < c) (hc1 : c < 1) (hc : ∃ (q : ), q = c) :
            theorem popcorn_continuous_at_irrational {c : } (hc0 : 0 < c) (hc1 : c < 1) (hc : Irrational c) :
            noncomputable def removableDiscontinuityExample (x : ) :

            Example 3.2.13. Define g : ℝ → ℝ by g x = 0 for x ≠ 0 and g 0 = 1. Then g is not continuous at 0 but it is continuous at every other point. The point 0 is a removable discontinuity since redefining g 0 = 0 would make the function continuous. Let A = {0} and B = ℝ \ {0}; the restriction g |_ A is continuous even though g fails to be continuous at 0, while g |_ B (and g on B) is continuous.

            Equations
            Instances For