Recovering a function from one of its exponentials

Real.exp is a smooth bijection onto (0, ∞) whose inverse Real.log is smooth there, so a real-valued function g is exactly as regular as any single exponential t ↦ e^{c g(t)} built from it with c ≠ 0. Mathlib supplies the easy direction (ContDiffOn.exp, Continuous.exp); this file records the converse, which recovers g as c⁻¹ log (e^{c g}).

Main declarations

• TauCeti.contDiffOn_of_contDiffOn_exp_const_mul: smoothness of g on a set follows from smoothness of t ↦ e^{c g(t)} there, for a single c ≠ 0.
• TauCeti.continuousOn_of_continuousOn_exp_const_mul: the same for continuity.

theorem TauCeti.contDiffOn_of_contDiffOn_exp_const_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {c : ℝ} (hc : c ≠ 0) {g : E → ℝ} {s : Set E} (h : ContDiffOn ℝ n (fun (t : E) => Real.exp (c * g t)) s) : ContDiffOn ℝ n g s

A real-valued function is smooth on a set as soon as one of its exponentials t ↦ e^{c g(t)}, c ≠ 0, is: the exponential is positive, so composing with Real.log stays inside the domain of smoothness of the logarithm, and Real.log_exp recovers g on the nose.

theorem TauCeti.continuousOn_of_continuousOn_exp_const_mul {α : Type u_1} [TopologicalSpace α] {c : ℝ} (hc : c ≠ 0) {g : α → ℝ} {s : Set α} (h : ContinuousOn (fun (t : α) => Real.exp (c * g t)) s) : ContinuousOn g s

A real-valued function is continuous on a set as soon as one of its exponentials t ↦ e^{c g(t)}, c ≠ 0, is.