Logarithms of real functions on manifolds #
The logarithm x ↦ Real.log (u x) of a C^n real function u on a manifold is C^n wherever
u does not vanish, since Real.log is smooth away from 0. This is the manifold version of
ContDiffAt.log; it is used, for instance, to see that the exponent φ of a smooth conformal
factor e^(2φ) is smooth.
Main results #
ContMDiffAt.log,ContMDiff.log:x ↦ Real.log (u x)isC^nwhereudoes not vanish.
theorem
ContMDiffAt.log
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{u : M → ℝ}
{x : M}
(hu : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) n u x)
(h : u x ≠ 0)
:
ContMDiffAt I (modelWithCornersSelf ℝ ℝ) n (fun (y : M) => Real.log (u y)) x
The logarithm of a real function that is C^n at a point where it does not vanish is C^n
there.
theorem
ContMDiff.log
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{u : M → ℝ}
(hu : ContMDiff I (modelWithCornersSelf ℝ ℝ) n u)
(h : ∀ (x : M), u x ≠ 0)
:
ContMDiff I (modelWithCornersSelf ℝ ℝ) n fun (y : M) => Real.log (u y)
The logarithm of a nowhere-vanishing C^n real function is C^n.