Differential calculus of one variable

Derivatives of real functions of one real variable: mean-value and second-derivative tests, Taylor polynomials and remainders, Borel's lemma, interchange of limits and derivatives, monotone and C^n gluing results; not nowhere-differentiable constructions (see continuity subfield).

TheoremA monotone differentiable function with discontinuous derivative#●ready to prove

There is a nondecreasing function \(f : \mathbb{R} \to \mathbb{R}\) that is differentiable at every point and whose derivative \(f'\) is not continuous.

public theorem_wanted exists_monotone_differentiable_not_continuous_deriv :
    ∃ f : ℝ → ℝ, Monotone f ∧ (∀ x : ℝ, DifferentiableAt ℝ f x) ∧ ¬ Continuous (deriv f)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_92.

TheoremA smooth function on the unit interval with some vanishing derivative at each point is a polynomial there#●ready to prove

A smooth function on the unit interval with some vanishing derivative at each point is a polynomial there. Let \(f : \mathbb{R} \to \mathbb{R}\) be infinitely differentiable on \([0, 1]\), and suppose that for every \(x \in [0, 1]\) there is an integer \(n \ge 0\) such that the \(n\)-th derivative of \(f\) within \([0, 1]\) vanishes at \(x\) (at the endpoints these derivatives are one-sided). Then there is a polynomial \(p\) with real coefficients such that \(f(x) = p(x)\) for every \(x \in [0, 1]\).

Smoothness means infinite differentiability here, not real analyticity: the source's formal statement assumed real analyticity, which reduces the problem to the identity theorem.

public theorem_wanted exists_polynomial_eq_of_forall_exists_iteratedDerivWithin_eq_zero (f : ℝ → ℝ)
    (hf : ContDiffOn ℝ ∞ f (Icc (0 : ℝ) 1))
    (hvanish : ∀ x ∈ Icc (0 : ℝ) 1, ∃ n : ℕ, iteratedDerivWithin n f (Icc (0 : ℝ) 1) x = 0) :
    ∃ p : Polynomial ℝ, ∀ x ∈ Icc (0 : ℝ) 1, f x = p.eval x
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Real functions; Functions of one variable), problem ma_proofbench_l2_81, with the change above.

TheoremAn even \(C^2\) function is a \(C^1\) function of \(x^2\)#●ready to prove

Let \(a>0\) and let \(f : \mathbb{R} \to \mathbb{R}\) be twice continuously differentiable on \([-a,a]\) with \(f(x)=f(-x)\) for all \(x\in[-a,a]\). Then there is \(g : \mathbb{R} \to \mathbb{R}\), continuously differentiable on \([0,a^2]\), with \(f(x)=g(x^2)\) for all \(x\in[-a,a]\).

public theorem_wanted exists_contDiffOn_comp_sq_of_even (a : ℝ) (ha : 0 < a)
    (f : ℝ → ℝ)
    (hf_C2 : ContDiffOn ℝ 2 f (Icc (-a) a))
    (hf_even : ∀ x : ℝ, x ∈ Icc (-a) a → f x = f (-x)) :
    ∃ g : ℝ → ℝ,
      ContDiffOn ℝ 1 g (Icc 0 (a ^ (2 : ℕ))) ∧
      ∀ x : ℝ, x ∈ Icc (-a) a → f x = g (x ^ (2 : ℕ))
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_11.

TheoremBorel's lemma#✓fully proved

For every sequence \((a_n)_{n \ge 0}\) of real numbers there is an infinitely differentiable function \(f : \mathbb{R} \to \mathbb{R}\) whose derivatives at \(0\) are \(f^{(n)}(0) = a_n\) for every \(n \ge 0\).

theorem borel_jet_real
    (a : ℕ → ℝ) :
    ∃ f : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) f ∧ ∀ n : ℕ, iteratedDeriv n f 0 = a n
Sources
  • E. Borel, Ann. Sci. Ec. Norm. Sup. (3) 12 (1895), 9-55, DOI 10.24033/asens.406.

TheoremGluing \(C^n\) functions on adjacent closed intervals#●ready to prove

Let \(E\) be a real normed space, let \(n \in \mathbb{N} \cup \{\infty\}\) and let \(a \le b \le c\) be real numbers. Let \(f, g : \mathbb{R} \to E\) be such that \(f\) is \(C^n\) on \([a, b]\) and \(g\) is \(C^n\) on \([b, c]\), and suppose that for every natural number \(k \le n\) the \(k\)-th derivative of \(f\) within \([a, b]\) and the \(k\)-th derivative of \(g\) within \([b, c]\) agree at \(b\). Then the function equal to \(f\) on \([a, b]\) and to \(g\) elsewhere is \(C^n\) on \([a, c]\).

public theorem_wanted contDiffOn_piecewise_Icc
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {n : ℕ∞} {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c)
    {f g : ℝ → E}
    (hf : ContDiffOn ℝ n f (Icc a b)) (hg : ContDiffOn ℝ n g (Icc b c))
    (hjets : ∀ k : ℕ, (k : ℕ∞) ≤ n →
      iteratedDerivWithin k f (Icc a b) b =
        iteratedDerivWithin k g (Icc b c) b) :
    ContDiffOn ℝ n (Set.piecewise (Icc a b) f g) (Icc a c)
Sources
  • https://en.wikipedia.org/wiki/Piecewise#Continuity_and_differentiability_of_piecewise_functions

TheoremOdd Taylor polynomials of the exponential have exactly one real zero#●ready to prove

For every odd positive integer \(n\), the polynomial \(1+x+x^2/2!+\cdots+x^n/n!\) has exactly one real zero.

public theorem_wanted existsUnique_sum_pow_div_factorial_eq_zero_of_odd
    (n : ℕ) (hnpos : 0 < n) (hnodd : Odd n) :
    ∃! x : ℝ, (∑ k ∈ Finset.range (n + 1), x ^ k / (Nat.factorial k)) = 0
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Polynomials, rational functions in real analysis), problem ma_proofbench_l1_19.

TheoremThe derivative of \(x^2 \sin(1/x^2)\) exists everywhere but is not integrable#●ready to prove

Let \(F : \mathbb{R} \to \mathbb{R}\) be given by \(F(x) = x^2 \sin(1/x^2)\) for \(x \ne 0\) and \(F(0) = 0\). Then \(F\) is differentiable at every real \(x\), but its derivative \(F'\) is not Lebesgue integrable on \([-1,1]\).

public theorem_wanted differentiable_and_not_integrableOn_deriv_sq_mul_sin_inv_sq
    (F : ℝ → ℝ) (h0 : F 0 = 0)
    (hF : ∀ x ≠ 0, F x = x ^ 2 * Real.sin (1 / (x ^ 2))) :
    (∀ x : ℝ, DifferentiableAt ℝ F x) ∧
      ¬ MeasureTheory.IntegrableOn (fun x : ℝ => deriv F x) (Set.Icc (-1 : ℝ) (1 : ℝ))
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_99.

TheoremThe map \(x \mapsto e^{x-1} - e^{1-x}\) has a unique fixed point#●ready to prove

There is exactly one real number \(x\) such that \(e^{x-1} - e^{1-x} = x\).

public theorem_wanted existsUnique_exp_sub_one_sub_exp_one_sub_eq_self :
    ∃! x : ℝ, (Real.exp (x - 1) - Real.exp (1 - x)) = x
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_59.
1 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.