Physlib.Mathematics.Trigonometry.Tanh

Imports

/-
Copyright (c) 2025 Afiq Hatta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Afiq Hatta
-/
module

public import Mathlib.Topology.Algebra.Polynomial
public import Mathlib.Analysis.Calculus.Deriv.Polynomial
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
public import Mathlib.Analysis.Distribution.TemperateGrowth

Properties of Tanh

We want to prove that the reflectionless potential is a Schwartz map. This means proving that pointwise multiplication of a Schwartz map with tanh is a Schwartz map. This means we need to prove that all derivatives of tanh are bounded and continuous, so that the nth derivative of a function multiplied by tanh decays faster than any polynomial.

TODO

Add these to mathlib eventually

Fill in the proofs for the properties of tanh

@[expose] public section

The derivative of tanh(x) is 1 - tanh(x)^2


lemma deriv_tanh : deriv Real.tanh = fun x => 1 - Real.tanh x ^ 2 := by⊢ deriv tanh = fun x => 1 - tanh x ^ 2
  have h: deriv (sinh / cosh) = fun x => 1 - Real.tanh x ^ 2 := by
    funext xx:ℝ⊢ deriv (sinh / cosh) x = 1 - tanh x ^ 2h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2
    rw [deriv_div,x:ℝ⊢ (deriv sinh x * cosh x - sinh x * deriv cosh x) / cosh x ^ 2 = 1 - tanh x ^ 2hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0x:ℝ⊢ (cosh x * cosh x - sinh x * sinh x) / cosh x ^ 2 = 1 - tanh x ^ 2hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2 Real.deriv_sinh,x:ℝ⊢ (cosh x * cosh x - sinh x * deriv cosh x) / cosh x ^ 2 = 1 - tanh x ^ 2hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0x:ℝ⊢ (cosh x * cosh x - sinh x * sinh x) / cosh x ^ 2 = 1 - tanh x ^ 2hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2 Real.deriv_coshx:ℝ⊢ (cosh x * cosh x - sinh x * sinh x) / cosh x ^ 2 = 1 - tanh x ^ 2hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0x:ℝ⊢ (cosh x * cosh x - sinh x * sinh x) / cosh x ^ 2 = 1 - tanh x ^ 2hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2]x:ℝ⊢ (cosh x * cosh x - sinh x * sinh x) / cosh x ^ 2 = 1 - tanh x ^ 2hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2
    field_simpx:ℝ⊢ cosh x ^ 2 - sinh x ^ 2 = cosh x ^ 2 * (1 - tanh x ^ 2)hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2
    rw [sq,x:ℝ⊢ cosh x * cosh x - sinh x ^ 2 = cosh x * cosh x * (1 - tanh x ^ 2)hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0x:ℝ⊢ cosh x * cosh x - sinh x * sinh x = cosh x * cosh x * (1 - (sinh x / cosh x) ^ 2)hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2 sq,x:ℝ⊢ cosh x * cosh x - sinh x * sinh x = cosh x * cosh x * (1 - tanh x ^ 2)hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0x:ℝ⊢ cosh x * cosh x - sinh x * sinh x = cosh x * cosh x * (1 - (sinh x / cosh x) ^ 2)hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2 tanh_eq_sinh_div_coshx:ℝ⊢ cosh x * cosh x - sinh x * sinh x = cosh x * cosh x * (1 - (sinh x / cosh x) ^ 2)hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0x:ℝ⊢ cosh x * cosh x - sinh x * sinh x = cosh x * cosh x * (1 - (sinh x / cosh x) ^ 2)hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2]x:ℝ⊢ cosh x * cosh x - sinh x * sinh x = cosh x * cosh x * (1 - (sinh x / cosh x) ^ 2)hcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2
    field_simphcx:ℝ⊢ DifferentiableAt ℝ sinh xhdx:ℝ⊢ DifferentiableAt ℝ cosh xhxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2
    ·hcx:ℝ⊢ DifferentiableAt ℝ sinh xh:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2 apply Real.differentiable_sinhAll goals completed! 🐙h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2
    ·hdx:ℝ⊢ DifferentiableAt ℝ cosh xh:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2 apply Real.differentiable_coshAll goals completed! 🐙h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2
    ·hxx:ℝ⊢ cosh x ≠ 0h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2 exact ne_of_gt (Real.cosh_pos x)h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2⊢ deriv tanh = fun x => 1 - tanh x ^ 2
  have h': Real.tanh = (sinh / cosh) := by
    funext xh:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2x:ℝ⊢ tanh x = (sinh / cosh) xh:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2h':tanh = sinh / cosh⊢ deriv tanh = fun x => 1 - tanh x ^ 2
    rw [Pi.div_apply,h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2x:ℝ⊢ tanh x = sinh x / cosh xh:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2h':tanh = sinh / cosh⊢ deriv tanh = fun x => 1 - tanh x ^ 2 tanh_eq_sinh_div_coshh:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2x:ℝ⊢ sinh x / cosh x = sinh x / cosh xh:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2h':tanh = sinh / cosh⊢ deriv tanh = fun x => 1 - tanh x ^ 2]h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2h':tanh = sinh / cosh⊢ deriv tanh = fun x => 1 - tanh x ^ 2h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2h':tanh = sinh / cosh⊢ deriv tanh = fun x => 1 - tanh x ^ 2
  nth_rewrite 1 [h']h:deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2h':tanh = sinh / cosh⊢ deriv (sinh / cosh) = fun x => 1 - tanh x ^ 2
  apply hAll goals completed! 🐙

Tanh(x) is n times continuously differentiable for all n


lemma contDiff_tanh {n : ℕ} : ContDiff ℝ n tanh := byn:ℕ⊢ ContDiff ℝ (↑n) tanh
  have hdiv : ContDiff ℝ n (fun x => Real.sinh x / Real.cosh x) := by
    apply ContDiff.divhfn:ℕ⊢ ContDiff ℝ (↑n) sinhhgn:ℕ⊢ ContDiff ℝ (↑n) coshh0n:ℕ⊢ ∀ (x : ℝ), cosh x ≠ 0n:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh x⊢ ContDiff ℝ (↑n) tanh
    ·hfn:ℕ⊢ ContDiff ℝ (↑n) sinhn:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh x⊢ ContDiff ℝ (↑n) tanh exact contDiff_sinhAll goals completed! 🐙n:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh x⊢ ContDiff ℝ (↑n) tanh
    ·hgn:ℕ⊢ ContDiff ℝ (↑n) coshn:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh x⊢ ContDiff ℝ (↑n) tanh exact contDiff_coshAll goals completed! 🐙n:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh x⊢ ContDiff ℝ (↑n) tanh
    ·h0n:ℕ⊢ ∀ (x : ℝ), cosh x ≠ 0n:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh x⊢ ContDiff ℝ (↑n) tanh intro xh0n:ℕx:ℝ⊢ cosh x ≠ 0n:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh x⊢ ContDiff ℝ (↑n) tanh
      exact ne_of_gt (Real.cosh_pos x)n:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh x⊢ ContDiff ℝ (↑n) tanhn:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh x⊢ ContDiff ℝ (↑n) tanh
  conv =>n:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh x| ContDiff ℝ (↑n) tanh
    enter [3, x]n:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh xx:ℝ| tanh x
    rw [tanh_eq_sinh_div_cosh]n:ℕhdiv:ContDiff ℝ ↑n fun x => sinh x / cosh xx:ℝ| sinh x / cosh x
  exact hdivAll goals completed! 🐙

The nth derivative of Tanh(x) is a polynomial of Tanh(x)


lemma iteratedDeriv_tanh_is_polynomial_of_tanh (n : ℕ) : ∃ P : Polynomial ℝ, ∀ x,
    iteratedDeriv n Real.tanh x = P.eval (Real.tanh x) := byn:ℕ⊢ ∃ P, ∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) P
  induction n with
  | zero =>zero⊢ ∃ P, ∀ (x : ℝ), iteratedDeriv 0 tanh x = Polynomial.eval (tanh x) P
    rw [iteratedDeriv_zerozero⊢ ∃ P, ∀ (x : ℝ), tanh x = Polynomial.eval (tanh x) Pzero⊢ ∃ P, ∀ (x : ℝ), tanh x = Polynomial.eval (tanh x) P]zero⊢ ∃ P, ∀ (x : ℝ), tanh x = Polynomial.eval (tanh x) P
    use Polynomial.Xh⊢ ∀ (x : ℝ), tanh x = Polynomial.eval (tanh x) Polynomial.X
    simpAll goals completed! 🐙
  | succ n ih =>succn:ℕih:∃ P, ∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) P⊢ ∃ P, ∀ (x : ℝ), iteratedDeriv (n + 1) tanh x = Polynomial.eval (tanh x) P
    obtain ⟨P, h'⟩ := ihsuccn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) P⊢ ∃ P, ∀ (x : ℝ), iteratedDeriv (n + 1) tanh x = Polynomial.eval (tanh x) P
    rw [iteratedDeriv_succsuccn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) P⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) Psuccn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) P⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) P]succn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) P⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) P
    have h'': iteratedDeriv n tanh = (fun x => Polynomial.eval (tanh x) P) := byn:ℕ⊢ ∃ P, ∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Psuccn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) P⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) P
      funext xn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Px:ℝ⊢ iteratedDeriv n tanh x = Polynomial.eval (tanh x) Psuccn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) P⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) P
      apply h'succn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) P⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) Psuccn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) P⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) P
    have h_comp : (fun x => Polynomial.eval (tanh x) P) = (fun t => P.eval t) ∘ tanh := byn:ℕ⊢ ∃ P, ∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Psuccn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanh⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) P
      funext xn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Px:ℝ⊢ Polynomial.eval (tanh x) P = ((fun t => Polynomial.eval t P) ∘ tanh) xsuccn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanh⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) P
      simp [Function.comp_apply]succn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanh⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) Psuccn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanh⊢ ∃ P, ∀ (x : ℝ), deriv (iteratedDeriv n tanh) x = Polynomial.eval (tanh x) P
    rw [h'',succn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanh⊢ ∃ P_1, ∀ (x : ℝ), deriv (fun x => Polynomial.eval (tanh x) P) x = Polynomial.eval (tanh x) P_1succn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanh⊢ ∃ P_1, ∀ (x : ℝ), deriv ((fun t => Polynomial.eval t P) ∘ tanh) x = Polynomial.eval (tanh x) P_1 h_compsuccn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanh⊢ ∃ P_1, ∀ (x : ℝ), deriv ((fun t => Polynomial.eval t P) ∘ tanh) x = Polynomial.eval (tanh x) P_1succn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanh⊢ ∃ P_1, ∀ (x : ℝ), deriv ((fun t => Polynomial.eval t P) ∘ tanh) x = Polynomial.eval (tanh x) P_1]succn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanh⊢ ∃ P_1, ∀ (x : ℝ), deriv ((fun t => Polynomial.eval t P) ∘ tanh) x = Polynomial.eval (tanh x) P_1
    use Polynomial.derivative P * (1 - Polynomial.X^2)hn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanh⊢ ∀ (x : ℝ),
  deriv ((fun t => Polynomial.eval t P) ∘ tanh) x =
    Polynomial.eval (tanh x) (Polynomial.derivative P * (1 - Polynomial.X ^ 2))
    intro xhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ deriv ((fun t => Polynomial.eval t P) ∘ tanh) x =
  Polynomial.eval (tanh x) (Polynomial.derivative P * (1 - Polynomial.X ^ 2))
    rw [deriv_comp,hn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ deriv (fun t => Polynomial.eval t P) (tanh x) * deriv tanh x =
  Polynomial.eval (tanh x) (Polynomial.derivative P * (1 - Polynomial.X ^ 2))h.hh₂n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ (fun t => Polynomial.eval t P) (tanh x)h.hhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ tanh xhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ Polynomial.eval (tanh x) (Polynomial.derivative P) * (fun x => 1 - tanh x ^ 2) x =
  Polynomial.eval (tanh x) (Polynomial.derivative P * (1 - Polynomial.X ^ 2))h.hh₂n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ (fun t => Polynomial.eval t P) (tanh x)h.hhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ tanh x Polynomial.deriv,hn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ Polynomial.eval (tanh x) (Polynomial.derivative P) * deriv tanh x =
  Polynomial.eval (tanh x) (Polynomial.derivative P * (1 - Polynomial.X ^ 2))h.hh₂n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ (fun t => Polynomial.eval t P) (tanh x)h.hhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ tanh xhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ Polynomial.eval (tanh x) (Polynomial.derivative P) * (fun x => 1 - tanh x ^ 2) x =
  Polynomial.eval (tanh x) (Polynomial.derivative P * (1 - Polynomial.X ^ 2))h.hh₂n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ (fun t => Polynomial.eval t P) (tanh x)h.hhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ tanh x deriv_tanhhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ Polynomial.eval (tanh x) (Polynomial.derivative P) * (fun x => 1 - tanh x ^ 2) x =
  Polynomial.eval (tanh x) (Polynomial.derivative P * (1 - Polynomial.X ^ 2))h.hh₂n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ (fun t => Polynomial.eval t P) (tanh x)h.hhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ tanh xhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ Polynomial.eval (tanh x) (Polynomial.derivative P) * (fun x => 1 - tanh x ^ 2) x =
  Polynomial.eval (tanh x) (Polynomial.derivative P * (1 - Polynomial.X ^ 2))h.hh₂n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ (fun t => Polynomial.eval t P) (tanh x)h.hhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ tanh x]hn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ Polynomial.eval (tanh x) (Polynomial.derivative P) * (fun x => 1 - tanh x ^ 2) x =
  Polynomial.eval (tanh x) (Polynomial.derivative P * (1 - Polynomial.X ^ 2))h.hh₂n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ (fun t => Polynomial.eval t P) (tanh x)h.hhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ tanh x
    simp only [Polynomial.eval_mul, Polynomial.eval_sub, Polynomial.eval_one, Polynomial.eval_pow,
      Polynomial.eval_X]h.hh₂n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ (fun t => Polynomial.eval t P) (tanh x)h.hhn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ tanh x
    case h.hh =>n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ tanh x
      have h': Real.tanh = (sinh / cosh) := byn:ℕ⊢ ∃ P, ∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Pn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ tanh x
        funext xn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx✝:ℝx:ℝ⊢ tanh x = (sinh / cosh) xn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ tanh x
        rw [Pi.div_apply,n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx✝:ℝx:ℝ⊢ tanh x = sinh x / cosh xn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ tanh x tanh_eq_sinh_div_coshn:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx✝:ℝx:ℝ⊢ sinh x / cosh x = sinh x / cosh xn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ tanh x]n:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ tanh xn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ tanh x
      rw [h'n:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ (sinh / cosh) xn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ (sinh / cosh) x]n:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ (sinh / cosh) x
      apply DifferentiableAt.divhcn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ sinh xhdn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ cosh xhxn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ cosh x ≠ 0
      ·hcn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ sinh x apply Real.differentiable_sinhAll goals completed! 🐙
      ·hdn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ DifferentiableAt ℝ cosh x apply Real.differentiable_coshAll goals completed! 🐙
      ·hxn:ℕP:Polynomial ℝh'✝:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝh':tanh = sinh / cosh⊢ cosh x ≠ 0 exact ne_of_gt (Real.cosh_pos x)All goals completed! 🐙
    case h.hh₂ =>n:ℕP:Polynomial ℝh':∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) Ph'':iteratedDeriv n tanh = fun x => Polynomial.eval (tanh x) Ph_comp:(fun x => Polynomial.eval (tanh x) P) = (fun t => Polynomial.eval t P) ∘ tanhx:ℝ⊢ DifferentiableAt ℝ (fun t => Polynomial.eval t P) (tanh x)
      apply Polynomial.differentiableAtAll goals completed! 🐙

For a polynomial P, show it's bounded on any bounded interval

lemma polynomial_bounded_on_interval (P : Polynomial ℝ) (a b : ℝ) :
    ∃ M : ℝ, ∀ x : ℝ, x ∈ Set.Icc a b → |P.eval x| ≤ M := byP:Polynomial ℝa:ℝb:ℝ⊢ ∃ M, ∀ x ∈ Set.Icc a b, |Polynomial.eval x P| ≤ M
  -- Polynomials are continuous
  have hcont : Continuous (fun x => P.eval x) := P.continuousP:Polynomial ℝa:ℝb:ℝhcont:Continuous fun x => Polynomial.eval x P⊢ ∃ M, ∀ x ∈ Set.Icc a b, |Polynomial.eval x P| ≤ M
  -- Closed bounded intervals are compact
  have hcompact : IsCompact (Set.Icc a b) := isCompact_IccP:Polynomial ℝa:ℝb:ℝhcont:Continuous fun x => Polynomial.eval x Phcompact:IsCompact (Set.Icc a b)⊢ ∃ M, ∀ x ∈ Set.Icc a b, |Polynomial.eval x P| ≤ M
  -- Continuous functions on compact sets are bounded
  obtain ⟨M, hM⟩ := hcompact.exists_bound_of_continuousOn hcont.continuousOnP:Polynomial ℝa:ℝb:ℝhcont:Continuous fun x => Polynomial.eval x Phcompact:IsCompact (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, ‖Polynomial.eval x P‖ ≤ M⊢ ∃ M, ∀ x ∈ Set.Icc a b, |Polynomial.eval x P| ≤ M
  use MhP:Polynomial ℝa:ℝb:ℝhcont:Continuous fun x => Polynomial.eval x Phcompact:IsCompact (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, ‖Polynomial.eval x P‖ ≤ M⊢ ∀ x ∈ Set.Icc a b, |Polynomial.eval x P| ≤ M
  exact hMAll goals completed! 🐙

For a polynomial P, show that P (tanh x) is bounded on the real line


lemma polynomial_tanh_bounded (P : Polynomial ℝ) :
    ∃ C : ℝ, ∀ x : ℝ, |P.eval (Real.tanh x)| ≤ C := byP:Polynomial ℝ⊢ ∃ C, ∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ C
  -- Since tanh maps to (-1, 1), it maps to [-1+ε, 1-ε] for any ε > 0
  -- But more directly, tanh maps to (-1, 1) ⊆ [-1, 1]
  have h_range : ∀ x : ℝ, Real.tanh x ∈ Set.Icc (-1) 1 := by
    intro xP:Polynomial ℝx:ℝ⊢ tanh x ∈ Set.Icc (-1) 1P:Polynomial ℝh_range:∀ (x : ℝ), tanh x ∈ Set.Icc (-1) 1⊢ ∃ C, ∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ C
    constructorleftP:Polynomial ℝx:ℝ⊢ -1 ≤ tanh xrightP:Polynomial ℝx:ℝ⊢ tanh x ≤ 1P:Polynomial ℝh_range:∀ (x : ℝ), tanh x ∈ Set.Icc (-1) 1⊢ ∃ C, ∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ C
    ·leftP:Polynomial ℝx:ℝ⊢ -1 ≤ tanh xP:Polynomial ℝh_range:∀ (x : ℝ), tanh x ∈ Set.Icc (-1) 1⊢ ∃ C, ∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ C exact le_of_lt (neg_one_lt_tanh x)All goals completed! 🐙P:Polynomial ℝh_range:∀ (x : ℝ), tanh x ∈ Set.Icc (-1) 1⊢ ∃ C, ∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ C
    ·rightP:Polynomial ℝx:ℝ⊢ tanh x ≤ 1P:Polynomial ℝh_range:∀ (x : ℝ), tanh x ∈ Set.Icc (-1) 1⊢ ∃ C, ∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ C exact le_of_lt (tanh_lt_one x)P:Polynomial ℝh_range:∀ (x : ℝ), tanh x ∈ Set.Icc (-1) 1⊢ ∃ C, ∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ CP:Polynomial ℝh_range:∀ (x : ℝ), tanh x ∈ Set.Icc (-1) 1⊢ ∃ C, ∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ C
  -- Apply polynomial boundedness on [-1, 1]
  obtain ⟨M, hM⟩ := polynomial_bounded_on_interval P (-1) 1P:Polynomial ℝh_range:∀ (x : ℝ), tanh x ∈ Set.Icc (-1) 1M:ℝhM:∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ M⊢ ∃ C, ∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ C
  use MhP:Polynomial ℝh_range:∀ (x : ℝ), tanh x ∈ Set.Icc (-1) 1M:ℝhM:∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ M⊢ ∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ M
  intro xhP:Polynomial ℝh_range:∀ (x : ℝ), tanh x ∈ Set.Icc (-1) 1M:ℝhM:∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ Mx:ℝ⊢ |Polynomial.eval (tanh x) P| ≤ M
  exact hM (Real.tanh x) (h_range x)All goals completed! 🐙

The nth derivative of tanh is bounded on the real line


lemma iteratedDeriv_tanh_bounded (n : ℕ) :
    ∃ C : ℝ, ∀ x : ℝ, |iteratedDeriv n Real.tanh x| ≤ C := byn:ℕ⊢ ∃ C, ∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ C
  obtain ⟨P, hP⟩ := iteratedDeriv_tanh_is_polynomial_of_tanh nn:ℕP:Polynomial ℝhP:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) P⊢ ∃ C, ∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ C
  obtain ⟨C, hC⟩ := polynomial_tanh_bounded Pn:ℕP:Polynomial ℝhP:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) PC:ℝhC:∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ C⊢ ∃ C, ∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ C
  use Chn:ℕP:Polynomial ℝhP:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) PC:ℝhC:∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ C⊢ ∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ C
  intro xhn:ℕP:Polynomial ℝhP:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) PC:ℝhC:∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ Cx:ℝ⊢ |iteratedDeriv n tanh x| ≤ C
  rw [hPhn:ℕP:Polynomial ℝhP:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) PC:ℝhC:∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ Cx:ℝ⊢ |Polynomial.eval (tanh x) P| ≤ Chn:ℕP:Polynomial ℝhP:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) PC:ℝhC:∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ Cx:ℝ⊢ |Polynomial.eval (tanh x) P| ≤ C]hn:ℕP:Polynomial ℝhP:∀ (x : ℝ), iteratedDeriv n tanh x = Polynomial.eval (tanh x) PC:ℝhC:∀ (x : ℝ), |Polynomial.eval (tanh x) P| ≤ Cx:ℝ⊢ |Polynomial.eval (tanh x) P| ≤ C
  exact hC xAll goals completed! 🐙

tanh is infinitely differentiable


lemma contDiff_top_tanh : ContDiff ℝ ∞ Real.tanh := by⊢ ContDiff ℝ ∞ tanh
    rw [contDiff_infty⊢ ∀ (n : ℕ), ContDiff ℝ (↑n) tanh⊢ ∀ (n : ℕ), ContDiff ℝ (↑n) tanh]⊢ ∀ (n : ℕ), ContDiff ℝ (↑n) tanh
    apply contDiff_tanhAll goals completed! 🐙

tanh has temperate growth


lemma tanh_hasTemperateGrowth : Function.HasTemperateGrowth Real.tanh := by⊢ Function.HasTemperateGrowth tanh
  constructorleft⊢ ContDiff ℝ ∞ tanhright⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ k
  ·left⊢ ContDiff ℝ ∞ tanh apply contDiff_top_tanhAll goals completed! 🐙
  ·right⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ k intro nrightn:ℕ⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ k
    use 0hn:ℕ⊢ ∃ C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0
    obtain ⟨C, hC⟩ := iteratedDeriv_tanh_bounded nhn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ C⊢ ∃ C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0
    use Chn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ C⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0
    intro xhn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0
    have h_equiv : ‖iteratedFDeriv ℝ n Real.tanh x‖ = |iteratedDeriv n Real.tanh x| := by⊢ Function.HasTemperateGrowth tanhhn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0
      rw [← iteratedFDerivWithin_univn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedFDerivWithin ℝ n tanh Set.univ x‖ = |iteratedDeriv n tanh x|n:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedFDerivWithin ℝ n tanh Set.univ x‖ = |iteratedDeriv n tanh x|hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0]n:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedFDerivWithin ℝ n tanh Set.univ x‖ = |iteratedDeriv n tanh x|hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0
      rw [← iteratedDerivWithin_univn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedFDerivWithin ℝ n tanh Set.univ x‖ = |iteratedDerivWithin n tanh Set.univ x|n:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedFDerivWithin ℝ n tanh Set.univ x‖ = |iteratedDerivWithin n tanh Set.univ x|hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0]n:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedFDerivWithin ℝ n tanh Set.univ x‖ = |iteratedDerivWithin n tanh Set.univ x|hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0
      rw [← norm_eq_absn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedFDerivWithin ℝ n tanh Set.univ x‖ = ‖iteratedDerivWithin n tanh Set.univ x‖n:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedFDerivWithin ℝ n tanh Set.univ x‖ = ‖iteratedDerivWithin n tanh Set.univ x‖hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0]n:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedFDerivWithin ℝ n tanh Set.univ x‖ = ‖iteratedDerivWithin n tanh Set.univ x‖hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0
      rw [norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithinn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝ⊢ ‖iteratedDerivWithin n tanh Set.univ x‖ = ‖iteratedDerivWithin n tanh Set.univ x‖hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0]hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ ‖iteratedFDeriv ℝ n tanh x‖ ≤ C * (1 + ‖x‖) ^ 0
    rw [h_equivhn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ |iteratedDeriv n tanh x| ≤ C * (1 + ‖x‖) ^ 0hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ |iteratedDeriv n tanh x| ≤ C * (1 + ‖x‖) ^ 0]hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ |iteratedDeriv n tanh x| ≤ C * (1 + ‖x‖) ^ 0
    simp only [pow_zero, mul_one]hn:ℕC:ℝhC:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Cx:ℝh_equiv:‖iteratedFDeriv ℝ n tanh x‖ = |iteratedDeriv n tanh x|⊢ |iteratedDeriv n tanh x| ≤ C
    exact hC xAll goals completed! 🐙

Iterated derivative for scaled tanh is differentiable


lemma iteratedDeriv_tanh_differentiable (n : ℕ) : Differentiable ℝ (iteratedDeriv n tanh) := byn:ℕ⊢ Differentiable ℝ (iteratedDeriv n tanh)
  have h : ContDiff ℝ (n + 1) tanh := by
    apply contDiff_tanhn:ℕh:ContDiff ℝ (↑n + 1) tanh⊢ Differentiable ℝ (iteratedDeriv n tanh)n:ℕh:ContDiff ℝ (↑n + 1) tanh⊢ Differentiable ℝ (iteratedDeriv n tanh)
  apply h.differentiable_iteratedDerivn:ℕh:ContDiff ℝ (↑n + 1) tanh⊢ ↑n < ↑n + 1
  have h' : n < n + 1 := byn:ℕ⊢ Differentiable ℝ (iteratedDeriv n tanh)n:ℕh:ContDiff ℝ (↑n + 1) tanhh':n < n + 1⊢ ↑n < ↑n + 1
    apply Nat.lt_add_onen:ℕh:ContDiff ℝ (↑n + 1) tanhh':n < n + 1⊢ ↑n < ↑n + 1n:ℕh:ContDiff ℝ (↑n + 1) tanhh':n < n + 1⊢ ↑n < ↑n + 1
  norm_castAll goals completed! 🐙

Norm of Iterated derivative for scaled tanh is equal to the norm of its Fderiv


lemma tanh_const_mul_iteratedDeriv_norm_eq_iteratedFDeriv_norm (n : ℕ) (x : ℝ) :
    ‖iteratedFDeriv ℝ n (fun x => tanh (κ * x)) x‖
    = |iteratedDeriv n (fun x => tanh (κ * x)) x| := byκ:ℝn:ℕx:ℝ⊢ ‖iteratedFDeriv ℝ n (fun x => tanh (κ * x)) x‖ = |iteratedDeriv n (fun x => tanh (κ * x)) x|
  rw [← iteratedFDerivWithin_univ,κ:ℝn:ℕx:ℝ⊢ ‖iteratedFDerivWithin ℝ n (fun x => tanh (κ * x)) Set.univ x‖ = |iteratedDeriv n (fun x => tanh (κ * x)) x|All goals completed! 🐙 ← iteratedDerivWithin_univ,κ:ℝn:ℕx:ℝ⊢ ‖iteratedFDerivWithin ℝ n (fun x => tanh (κ * x)) Set.univ x‖ =
  |iteratedDerivWithin n (fun x => tanh (κ * x)) Set.univ x|All goals completed! 🐙 ← norm_eq_abs,κ:ℝn:ℕx:ℝ⊢ ‖iteratedFDerivWithin ℝ n (fun x => tanh (κ * x)) Set.univ x‖ =
  ‖iteratedDerivWithin n (fun x => tanh (κ * x)) Set.univ x‖All goals completed! 🐙
      norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithinκ:ℝn:ℕx:ℝ⊢ ‖iteratedDerivWithin n (fun x => tanh (κ * x)) Set.univ x‖ = ‖iteratedDerivWithin n (fun x => tanh (κ * x)) Set.univ x‖All goals completed! 🐙]All goals completed! 🐙

Iterated derivative for scaled tanh


lemma iteratedDeriv_tanh_const_mul (n : ℕ) (κ : ℝ) : ∀ x : ℝ,
    iteratedDeriv n (fun y => Real.tanh (κ * y)) x = κ^n * (iteratedDeriv n Real.tanh) (κ * x) := byn:ℕκ:ℝ⊢ ∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)
  induction n with
  | zero =>zeroκ:ℝ⊢ ∀ (x : ℝ), iteratedDeriv 0 (fun y => tanh (κ * y)) x = κ ^ 0 * iteratedDeriv 0 tanh (κ * x)
    rw [iteratedDeriv_zerozeroκ:ℝ⊢ ∀ (x : ℝ), tanh (κ * x) = κ ^ 0 * iteratedDeriv 0 tanh (κ * x)zeroκ:ℝ⊢ ∀ (x : ℝ), tanh (κ * x) = κ ^ 0 * iteratedDeriv 0 tanh (κ * x)]zeroκ:ℝ⊢ ∀ (x : ℝ), tanh (κ * x) = κ ^ 0 * iteratedDeriv 0 tanh (κ * x)
    field_simpzeroκ:ℝ⊢ ∀ (x : ℝ), tanh (κ * x) = iteratedDeriv 0 tanh (κ * x)
    simpAll goals completed! 🐙
  | succ n ih =>succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), iteratedDeriv (n + 1) (fun y => tanh (κ * y)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
    rw [iteratedDeriv_succsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (iteratedDeriv n fun y => tanh (κ * y)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (iteratedDeriv n fun y => tanh (κ * y)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)]succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (iteratedDeriv n fun y => tanh (κ * y)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
    have h' : iteratedDeriv n (fun y => tanh (κ * y)) =
        fun x => κ ^ n * iteratedDeriv n tanh (κ * x) := byn:ℕκ:ℝ⊢ ∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (iteratedDeriv n fun y => tanh (κ * y)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
      funext xκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)x:ℝ⊢ iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (iteratedDeriv n fun y => tanh (κ * y)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
      rw [ihκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)x:ℝ⊢ κ ^ n * iteratedDeriv n tanh (κ * x) = κ ^ n * iteratedDeriv n tanh (κ * x)succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (iteratedDeriv n fun y => tanh (κ * y)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)]succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (iteratedDeriv n fun y => tanh (κ * y)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (iteratedDeriv n fun y => tanh (κ * y)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
    rw [h'succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (fun x => κ ^ n * iteratedDeriv n tanh (κ * x)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (fun x => κ ^ n * iteratedDeriv n tanh (κ * x)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)]succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), deriv (fun x => κ ^ n * iteratedDeriv n tanh (κ * x)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
    simp only [deriv_const_mul_field']succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)⊢ ∀ (x : ℝ), κ ^ n * deriv (fun x => iteratedDeriv n tanh (κ * x)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
    have h'': (fun x => iteratedDeriv n tanh (κ * x)) =
        (iteratedDeriv n tanh) ∘ (fun x => κ * x) := byn:ℕκ:ℝ⊢ ∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * x⊢ ∀ (x : ℝ), κ ^ n * deriv (fun x => iteratedDeriv n tanh (κ * x)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
      funext xκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)x:ℝ⊢ iteratedDeriv n tanh (κ * x) = (iteratedDeriv n tanh ∘ fun x => κ * x) xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * x⊢ ∀ (x : ℝ), κ ^ n * deriv (fun x => iteratedDeriv n tanh (κ * x)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
      simpsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * x⊢ ∀ (x : ℝ), κ ^ n * deriv (fun x => iteratedDeriv n tanh (κ * x)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * x⊢ ∀ (x : ℝ), κ ^ n * deriv (fun x => iteratedDeriv n tanh (κ * x)) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
    rw [h''succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * x⊢ ∀ (x : ℝ), κ ^ n * deriv (iteratedDeriv n tanh ∘ fun x => κ * x) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * x⊢ ∀ (x : ℝ), κ ^ n * deriv (iteratedDeriv n tanh ∘ fun x => κ * x) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)]succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * x⊢ ∀ (x : ℝ), κ ^ n * deriv (iteratedDeriv n tanh ∘ fun x => κ * x) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
    intro xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ κ ^ n * deriv (iteratedDeriv n tanh ∘ fun x => κ * x) x = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)
    rw [deriv_comp,succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ κ ^ n * (deriv (iteratedDeriv n tanh) (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x ← iteratedDeriv_succsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x]succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
    have h''': deriv (fun x => κ * x) = fun x => κ := byn:ℕκ:ℝ⊢ ∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
      funext xκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ deriv (fun x => κ * x) x = κsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
      rw [deriv_const_mul,κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ κ * deriv (fun x => x) x = κhdκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ DifferentiableAt ℝ (fun x => x) xκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ κ * deriv id x = κhdκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ DifferentiableAt ℝ (fun x => x) xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x ← Function.id_defκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ κ * deriv id x = κhdκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ DifferentiableAt ℝ (fun x => x) xκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ κ * deriv id x = κhdκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ DifferentiableAt ℝ (fun x => x) xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x]κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ κ * deriv id x = κhdκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ DifferentiableAt ℝ (fun x => x) xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
      field_simpκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ κ * deriv id x = κhdκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ DifferentiableAt ℝ (fun x => x) xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
      simp only [deriv_id', mul_one]hdκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx✝:ℝx:ℝ⊢ DifferentiableAt ℝ (fun x => x) xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
      apply differentiable_idsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * deriv (fun x => κ * x) x) =
  κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
    rw [h'''succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * (fun x => κ) x) = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) xsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * (fun x => κ) x) = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x]succκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * (iteratedDeriv (n + 1) tanh (κ * x) * (fun x => κ) x) = κ ^ (n + 1) * iteratedDeriv (n + 1) tanh (κ * x)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
    field_simpsuccκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝh''':(deriv fun x => κ * x) = fun x => κ⊢ κ ^ n * κ * iteratedDeriv (n + 1) tanh (κ * x) = iteratedDeriv (n + 1) tanh (κ * x) * κ ^ (n + 1)succ.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
    ringsucc.hh₂κ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (iteratedDeriv n tanh) (κ * x)succ.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
    apply iteratedDeriv_tanh_differentiablesucc.hhκ:ℝn:ℕih:∀ (x : ℝ), iteratedDeriv n (fun y => tanh (κ * y)) x = κ ^ n * iteratedDeriv n tanh (κ * x)h':(iteratedDeriv n fun y => tanh (κ * y)) = fun x => κ ^ n * iteratedDeriv n tanh (κ * x)h'':(fun x => iteratedDeriv n tanh (κ * x)) = iteratedDeriv n tanh ∘ fun x => κ * xx:ℝ⊢ DifferentiableAt ℝ (fun x => κ * x) x
    fun_propAll goals completed! 🐙

tanh(κx) has temperate growth


@[fun_prop]
lemma tanh_const_mul_hasTemperateGrowth (κ : ℝ) :
    Function.HasTemperateGrowth (fun x => Real.tanh (κ * x)) := byκ:ℝ⊢ Function.HasTemperateGrowth fun x => tanh (κ * x)
  constructorleftκ:ℝ⊢ ContDiff ℝ ∞ fun x => tanh (κ * x)rightκ:ℝ⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => tanh (κ * x)) x‖ ≤ C * (1 + ‖x‖) ^ k
  ·leftκ:ℝ⊢ ContDiff ℝ ∞ fun x => tanh (κ * x) have h : (fun x => Real.tanh (κ * x)) = (Real.tanh ∘ (fun x => κ * x)) :=
      rflleftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * x⊢ ContDiff ℝ ∞ fun x => tanh (κ * x)
    have h' : ContDiff ℝ ∞ (fun x => κ * x) := byκ:ℝ⊢ Function.HasTemperateGrowth fun x => tanh (κ * x)leftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ fun x => tanh (κ * x)
      have h'': (fun x : ℝ => κ * x) = fun x => κ • x := rflκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh'':(fun x => κ * x) = fun x => κ • x⊢ ContDiff ℝ ∞ fun x => κ * xleftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ fun x => tanh (κ * x)
      rw [contDiff_infty,κ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh'':(fun x => κ * x) = fun x => κ • x⊢ ∀ (n : ℕ), ContDiff ℝ ↑n fun x => κ * xκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh'':(fun x => κ * x) = fun x => κ • x⊢ ∀ (n : ℕ), ContDiff ℝ ↑n fun x => κ • xleftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ fun x => tanh (κ * x) h''κ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh'':(fun x => κ * x) = fun x => κ • x⊢ ∀ (n : ℕ), ContDiff ℝ ↑n fun x => κ • xκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh'':(fun x => κ * x) = fun x => κ • x⊢ ∀ (n : ℕ), ContDiff ℝ ↑n fun x => κ • xleftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ fun x => tanh (κ * x)]κ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh'':(fun x => κ * x) = fun x => κ • x⊢ ∀ (n : ℕ), ContDiff ℝ ↑n fun x => κ • xleftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ fun x => tanh (κ * x)
      intro nκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh'':(fun x => κ * x) = fun x => κ • xn:ℕ⊢ ContDiff ℝ ↑n fun x => κ • xleftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ fun x => tanh (κ * x)
      apply contDiff_const_smulleftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ fun x => tanh (κ * x)leftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ fun x => tanh (κ * x)
    rw [hleftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ (tanh ∘ fun x => κ * x)leftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ (tanh ∘ fun x => κ * x)]leftκ:ℝh:(fun x => tanh (κ * x)) = tanh ∘ fun x => κ * xh':ContDiff ℝ ∞ fun x => κ * x⊢ ContDiff ℝ ∞ (tanh ∘ fun x => κ * x)
    apply ContDiff.comp contDiff_top_tanh h'All goals completed! 🐙
  ·rightκ:ℝ⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => tanh (κ * x)) x‖ ≤ C * (1 + ‖x‖) ^ k intro nrightκ:ℝn:ℕ⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => tanh (κ * x)) x‖ ≤ C * (1 + ‖x‖) ^ k
    obtain ⟨D, hD⟩ := iteratedDeriv_tanh_bounded nrightκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ D⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => tanh (κ * x)) x‖ ≤ C * (1 + ‖x‖) ^ k
    use 0hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ D⊢ ∃ C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => tanh (κ * x)) x‖ ≤ C * (1 + ‖x‖) ^ 0
    use D * (|κ| ^ n)hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ D⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => tanh (κ * x)) x‖ ≤ D * |κ| ^ n * (1 + ‖x‖) ^ 0
    intro xhκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ ‖iteratedFDeriv ℝ n (fun x => tanh (κ * x)) x‖ ≤ D * |κ| ^ n * (1 + ‖x‖) ^ 0
    rw [tanh_const_mul_iteratedDeriv_norm_eq_iteratedFDeriv_norm,hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |iteratedDeriv n (fun x => tanh (κ * x)) x| ≤ D * |κ| ^ n * (1 + ‖x‖) ^ 0hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ ^ n * iteratedDeriv n tanh (κ * x)| ≤ D * |κ| ^ n * (1 + ‖x‖) ^ 0 iteratedDeriv_tanh_const_mulhκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ ^ n * iteratedDeriv n tanh (κ * x)| ≤ D * |κ| ^ n * (1 + ‖x‖) ^ 0hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ ^ n * iteratedDeriv n tanh (κ * x)| ≤ D * |κ| ^ n * (1 + ‖x‖) ^ 0]hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ ^ n * iteratedDeriv n tanh (κ * x)| ≤ D * |κ| ^ n * (1 + ‖x‖) ^ 0
    field_simphκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ ^ n * iteratedDeriv n tanh (κ * x)| ≤ D * |κ| ^ n
    rw [abs_mul,hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ ^ n| * |iteratedDeriv n tanh (κ * x)| ≤ D * |κ| ^ nhκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ| ^ n * |iteratedDeriv n tanh (κ * x)| ≤ |κ| ^ n * D abs_pow,hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ| ^ n * |iteratedDeriv n tanh (κ * x)| ≤ D * |κ| ^ nhκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ| ^ n * |iteratedDeriv n tanh (κ * x)| ≤ |κ| ^ n * D mul_comm,hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |iteratedDeriv n tanh (κ * x)| * |κ| ^ n ≤ D * |κ| ^ nhκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ| ^ n * |iteratedDeriv n tanh (κ * x)| ≤ |κ| ^ n * D mul_comm,hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ| ^ n * |iteratedDeriv n tanh (κ * x)| ≤ D * |κ| ^ nhκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ| ^ n * |iteratedDeriv n tanh (κ * x)| ≤ |κ| ^ n * D mul_comm D (|κ| ^ n)hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ| ^ n * |iteratedDeriv n tanh (κ * x)| ≤ |κ| ^ n * Dhκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ| ^ n * |iteratedDeriv n tanh (κ * x)| ≤ |κ| ^ n * D]hκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |κ| ^ n * |iteratedDeriv n tanh (κ * x)| ≤ |κ| ^ n * D
    apply mul_le_mul_of_nonneg_lefth.hbcκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ |iteratedDeriv n tanh (κ * x)| ≤ Dhaκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ 0 ≤ |κ| ^ n
    apply hDhaκ:ℝn:ℕD:ℝhD:∀ (x : ℝ), |iteratedDeriv n tanh x| ≤ Dx:ℝ⊢ 0 ≤ |κ| ^ n
    simp only [abs_nonneg, pow_nonneg]All goals completed! 🐙