Conformal rescaling of Riemannian metrics

Multiplying a C^n Riemannian metric g on a vector bundle by a positive C^n function f on the base gives another C^n Riemannian metric f • g, conformal to g. Many model metrics are written this way: the upper half-space model of hyperbolic space is the Euclidean metric divided by the square of the height, and the Poincaré ball model is the Euclidean metric multiplied by 4 / (1 - ‖x‖²)².

Main definitions

• Bundle.ContMDiffRiemannianMetric.rescale: the rescaled metric f • g.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (conformal metrics) and Chapter 3 (the models of hyperbolic space).

noncomputable def Bundle.ContMDiffRiemannianMetric.rescale {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_5} [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [∀ (b : B), ContinuousConstSMul ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (g : ContMDiffRiemannianMetric IB n F E) (f : B → ℝ) (hf : ContMDiff IB (modelWithCornersSelf ℝ ℝ) n f) (hf_pos : ∀ (b : B), 0 < f b) : ContMDiffRiemannianMetric IB n F E

The Riemannian metric f • g obtained by multiplying a C^n Riemannian metric g by a positive C^n function f on the base.

Equations

• g.rescale f hf hf_pos = { inner := fun (b : B) => f b • g.inner b, symm := ⋯, pos := ⋯, isVonNBounded := ⋯, contMDiff := ⋯ }

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.rescale_inner {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_5} [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [∀ (b : B), ContinuousConstSMul ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (g : ContMDiffRiemannianMetric IB n F E) (f : B → ℝ) (hf : ContMDiff IB (modelWithCornersSelf ℝ ℝ) n f) (hf_pos : ∀ (b : B), 0 < f b) (b : B) (v w : E b) : (((g.rescale f hf hf_pos).inner b) v) w = f b * ((g.inner b) v) w

The rescaled metric f • g is f b times g on the fibre over b.