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

theorem tanh_lt_one (x : ℝ) : Real.tanh x < 1

tanh(x) is less than 1 for all x

theorem minus_one_lt_tanh (x : ℝ) : -1 < Real.tanh x

tanh(x) is greater than -1 for all x

theorem abs_tanh_lt_one (x : ℝ) : |Real.tanh x| < 1

The absolute value of tanh is bounded by 1

theorem deriv_tanh (x : ℝ) : deriv Real.tanh = fun (x : ℝ) => 1 - Real.tanh x ^ 2

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

theorem contDiff_tanh {n : ℕ} : ContDiff ℝ (↑n) Real.tanh

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

theorem iteratedDeriv_tanh_is_polynomial_of_tanh (n : ℕ) (x : ℝ) : ∃ (P : Polynomial ℝ), ∀ (x : ℝ), iteratedDeriv n Real.tanh x = Polynomial.eval (Real.tanh x) P

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