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 : 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 : ℕ) : ∃ (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)

theorem polynomial_bounded_on_interval (P : Polynomial ℝ) (a b : ℝ) : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |Polynomial.eval x P| ≤ M

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

theorem polynomial_tanh_bounded (P : Polynomial ℝ) : ∃ (C : ℝ), ∀ (x : ℝ), |Polynomial.eval (Real.tanh x) P| ≤ C

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

theorem iteratedDeriv_tanh_bounded (n : ℕ) : ∃ (C : ℝ), ∀ (x : ℝ), |iteratedDeriv n Real.tanh x| ≤ C

The nth derivative of tanh is bounded on the real line

theorem contDiff_top_tanh : ContDiff ℝ (↑⊤) Real.tanh

tanh is infinitely differentiable

theorem tanh_hasTemperateGrowth : Function.HasTemperateGrowth Real.tanh

tanh has temperate growth

theorem iteratedDeriv_tanh_differentiable (n : ℕ) : Differentiable ℝ (iteratedDeriv n Real.tanh)

Iterated derivative for scaled tanh is differentiable

theorem tanh_const_mul_iteratedDeriv_norm_eq_iteratedFDeriv_norm {κ : ℝ} (n : ℕ) (x : ℝ) : ‖iteratedFDeriv ℝ n (fun (x : ℝ) => Real.tanh (κ * x)) x‖ = |iteratedDeriv n (fun (x : ℝ) => Real.tanh (κ * x)) x|

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

theorem iteratedDeriv_tanh_const_mul (n : ℕ) (κ x : ℝ) : iteratedDeriv n (fun (y : ℝ) => Real.tanh (κ * y)) x = κ ^ n * iteratedDeriv n Real.tanh (κ * x)

Iterated derivative for scaled tanh

theorem tanh_const_mul_hasTemperateGrowth (κ : ℝ) : Function.HasTemperateGrowth fun (x : ℝ) => Real.tanh (κ * x)

tanh(κx) has temperate growth