Conformal classes of Riemannian metrics

11 fully proved

Bundle

DefinitionLowering the smoothness of a Riemannian metric#✓fully proved

Let \(E\) be a real vector bundle over a manifold \(B\), let \(m \le n\) be smoothness exponents in \(\mathbb{N} \cup \{\infty, \omega\}\), and let \(g\) be a \(C^n\) Riemannian metric on \(E\). Then \(g\), with the same inner product on every fiber, is a \(C^m\) Riemannian metric on \(E\).

def ContMDiffRiemannianMetric.ofLE (g : ContMDiffRiemannianMetric IB n F E)
    {m : ℕ∞ω} (h : m ≤ n) : ContMDiffRiemannianMetric IB m F E where
  inner := g.inner
  symm := g.symm
  pos := g.pos
  isVonNBounded := g.isVonNBounded
  contMDiff := g.contMDiff.of_le h

Used by 1

Used byLowering the smoothness keeps the inner product

TheoremLowering the smoothness keeps the inner product#✓fully proved

Let \(E\) be a real vector bundle over a manifold \(B\), let \(m \le n\) be smoothness exponents in \(\mathbb{N} \cup \{\infty, \omega\}\), and let \(g\) be a \(C^n\) Riemannian metric on \(E\). For every \(b \in B\), the inner product on the fiber \(E_b\) of \(g\) viewed as a \(C^m\) Riemannian metric equals the inner product of \(g\) on \(E_b\).

@[simp]
theorem ContMDiffRiemannianMetric.ofLE_inner
    (g : ContMDiffRiemannianMetric IB n F E) {m : ℕ∞ω} (h : m ≤ n) (b : B) :
    (g.ofLE h).inner b = g.inner b

Uses 1

Statement usesLowering the smoothness of a Riemannian metric

DefinitionConformal scaling of a Riemannian metric#✓fully proved

Let \(E\) be a real vector bundle over a manifold \(B\), let \(n \in \mathbb{N} \cup \{\infty, \omega\}\), let \(g\) be a \(C^n\) Riemannian metric on \(E\), and let \(u : B \to \mathbb{R}\) be a \(C^n\) function with \(u(b) > 0\) for every \(b \in B\). The conformal scaling of \(g\) by \(u\) is the \(C^n\) Riemannian metric \(u g\) on \(E\) whose inner product on each fiber \(E_b\) is \(u(b)\) times the inner product of \(g\) on \(E_b\).

Bundle.ContMDiffRiemannianMetric.conformalScale · 82 lines

def ContMDiffRiemannianMetric.conformalScale
    (g : ContMDiffRiemannianMetric IB n F E) (u : B → ℝ)
    (hu : ContMDiff IB 𝓘(ℝ) n u) (hpos : ∀ b, 0 < u b) :
    ContMDiffRiemannianMetric IB n F E where
  inner := fun b ↦ u b • g.inner b
  symm := by
    intro b v w
    have h1 : (u b • g.inner b) v w = u b * g.inner b v w := by
      simp [smul_eq_mul]
    have h2 : (u b • g.inner b) w v = u b * g.inner b w v := by
      simp [smul_eq_mul]
    rw [h1, h2, g.symm b v w]
  pos := by
    intro b v hv
    have h1 : (u b • g.inner b) v v = u b * g.inner b v v := by
      simp [smul_eq_mul]
    rw [h1]
    exact mul_pos (hpos b) (g.pos b v hv)
  isVonNBounded := by
    intro b
    have hub : 0 < u b := hpos b
    have hub_ne : u b ≠ 0 := ne_of_gt hub
    have hsqrt_pos : 0 < Real.sqrt (u b) := Real.sqrt_pos.mpr hub
    have hsqrt_ne : Real.sqrt (u b) ≠ 0 := ne_of_gt hsqrt_pos
    have hsqrt_sq : Real.sqrt (u b) ^ 2 = u b := Real.sq_sqrt (le_of_lt hub)
    set c : ℝ := (Real.sqrt (u b))⁻¹ with hc_def
    have hc_ne : c ≠ 0 := by
      rw [hc_def]
      exact inv_ne_zero hsqrt_ne
    have hcc : c * c = (u b)⁻¹ := by
      rw [hc_def, ← mul_inv_rev, ← pow_two, hsqrt_sq]
    have hcu : u b * (c * c) = 1 := by
      rw [hcc, mul_inv_cancel₀ hub_ne]
    have hcinv : c⁻¹ = Real.sqrt (u b) := by
      rw [hc_def, inv_inv]
    have hback : ∀ t : ℝ, c⁻¹ * (c⁻¹ * t) = u b * t := by
      intro t
      rw [hcinv, ← mul_assoc, ← pow_two, hsqrt_sq]
    have hfwd : ∀ t : ℝ, u b * (c * (c * t)) = t := by
      intro t
      have hring : u b * (c * (c * t)) = (u b * (c * c)) * t := by ring
      rw [hring, hcu, one_mul]
    have hscale : ∀ (a : ℝ) (v w : E b),
        g.inner b (a • v) (a • w) = a * (a * g.inner b v w) := by
      intro a v w
      simp [smul_eq_mul]
    have hsmul_inner : ∀ v w : E b,
        (u b • g.inner b) v w = u b * g.inner b v w := by
      intro v w
      simp [smul_eq_mul]
    let L : E b →L[ℝ] E b := c • ContinuousLinearMap.id ℝ (E b)
    have hL_apply : ∀ v : E b, L v = c • v := by
      intro v
      change (c • ContinuousLinearMap.id ℝ (E b)) v = c • v
      simp
    have hLinv : ∀ w : E b, L (c⁻¹ • w) = w := by
      intro w
      rw [hL_apply, smul_smul, mul_inv_cancel₀ hc_ne, one_smul]
    have hset : {v : E b | (u b • g.inner b) v v < 1} =
        L '' {v : E b | g.inner b v v < 1} := by
      ext w
      simp only [Set.mem_ofPred_eq, Set.mem_image]
      constructor
      · intro hw
        rw [hsmul_inner] at hw
        refine ⟨c⁻¹ • w, ?_, hLinv w⟩
        have hsc : g.inner b (c⁻¹ • w) (c⁻¹ • w) =
            c⁻¹ * (c⁻¹ * g.inner b w w) := hscale c⁻¹ w w
        rw [hsc, hback]
        exact hw
      · intro hw
        obtain ⟨v, hv, hvw⟩ := hw
        subst hvw
        rw [hsmul_inner]
        have hsc : g.inner b (L v) (L v) = c * (c * g.inner b v v) := by
          rw [hL_apply v]
          exact hscale c v v
        rw [hsc, hfwd]
        exact hv
    rw [hset]
    exact Bornology.IsVonNBounded.image (g.isVonNBounded b) L
  contMDiff := ContMDiff.smul_section hu g.contMDiff

Used by 4

Used byInner product of a conformally scaled metric · Conformal scalings lie in the conformal class · Conformal scaling of a metric in coordinates · Constant rescalings converge in every \(C^k\) topology

TheoremInner product of a conformally scaled metric#✓fully proved

Let \(E\) be a real vector bundle over a manifold \(B\), let \(n \in \mathbb{N} \cup \{\infty, \omega\}\), let \(g\) be a \(C^n\) Riemannian metric on \(E\), with inner product \(g_b\) on the fiber \(E_b\), and let \(u : B \to \mathbb{R}\) be a \(C^n\) function with \(u(b) > 0\) for every \(b \in B\). Then the conformal scaling \(u g\) of \(g\) by \(u\) satisfies \((u g)_b(v, w) = u(b)\, g_b(v, w)\) for every \(b \in B\) and all \(v, w \in E_b\).

@[simp]
theorem ContMDiffRiemannianMetric.conformalScale_inner_apply
    (g : ContMDiffRiemannianMetric IB n F E) (u : B → ℝ)
    (hu : ContMDiff IB 𝓘(ℝ) n u) (hpos : ∀ b, 0 < u b) (b : B)
    (v w : E b) :
    (g.conformalScale u hu hpos).inner b v w = u b * g.inner b v w

Uses 1 · Used by 2

Statement usesConformal scaling of a Riemannian metric

Used byConformal scalings lie in the conformal class · Conformal scaling of a metric in coordinates

TheoremA conformal factor at a point is positive#✓fully proved

Let \(E\) be a real vector bundle over a manifold \(B\), let \(n \in \mathbb{N} \cup \{\infty, \omega\}\), and let \(g\) and \(g'\) be \(C^n\) Riemannian metrics on \(E\), with inner products \(g_b\) and \(g'_b\) on the fiber \(E_b\). Let \(u : B \to \mathbb{R}\) and \(b \in B\). If \(g'_b(v, w) = u(b)\, g_b(v, w)\) for all \(v, w \in E_b\) and \(E_b\) contains a nonzero vector, then \(u(b) > 0\).

theorem ContMDiffRiemannianMetric.pos_of_inner_eq_mul
    (g g' : ContMDiffRiemannianMetric IB n F E) {u : B → ℝ} {b : B}
    (h : ∀ v w : E b, g'.inner b v w = u b * g.inner b v w)
    (hb : ∃ v : E b, v ≠ 0) : 0 < u b

Manifold

DefinitionConformal class of a Riemannian metric#✓fully proved

Let \(M\) be a \(C^\infty\) manifold modeled on a real normed space, and let \(g\) be a \(C^\infty\) Riemannian metric on \(M\), with inner product \(g_x\) on the tangent space \(T_x M\). The conformal class of \(g\) is the set of \(C^\infty\) Riemannian metrics \(g'\) on \(M\) for which there is a \(C^\infty\) function \(u : M \to \mathbb{R}\) with \(u(x) > 0\) for all \(x \in M\) and \(g'_x(v, w) = u(x)\, g_x(v, w)\) for all \(x \in M\) and all \(v, w \in T_x M\).

def conformalClass
    (g : ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x)) :
    Set (ContMDiffRiemannianMetric I ∞ E (fun x : M ↦ TangentSpace I x)) :=
  {g' |
    ∃ u : M → ℝ,
      ContMDiff I 𝓘(ℝ) ∞ u ∧
        (∀ x, 0 < u x) ∧
          ∀ x (v w : TangentSpace I x), g'.inner x v w = u x * g.inner x v w}

Used by 5

Used byConformal scalings lie in the conformal class · Conformal metrics via an exponential factor · Conformal equivalence is symmetric · Conformal equivalence is transitive · A metric lies in its own conformal class

TheoremConformal metrics via an exponential factor#✓fully proved

Let \(M\) be a \(C^\infty\) manifold modeled on a real normed space, and let \(g\) and \(g'\) be \(C^\infty\) Riemannian metrics on \(M\), with inner products \(g_x\) and \(g'_x\) on the tangent space \(T_x M\). Then \(g'\) lies in the conformal class of \(g\) if and only if there is a \(C^\infty\) function \(f : M \to \mathbb{R}\) with \(g'_x(v, w) = e^{f(x)}\, g_x(v, w)\) for all \(x \in M\) and all \(v, w \in T_x M\).

theorem mem_conformalClass_iff_exp :
    g' ∈ conformalClass g ↔
      ∃ f : M → ℝ,
        ContMDiff I 𝓘(ℝ) ∞ f ∧
          ∀ x (v w : TangentSpace I x),
            g'.inner x v w = Real.exp (f x) * g.inner x v w

Uses 1

Statement usesConformal class of a Riemannian metric

TheoremA metric lies in its own conformal class#✓fully proved

Every smooth Riemannian metric \(g\) on a smooth manifold \(M\) lies in the conformal class of \(g\).

theorem self_mem_conformalClass : g ∈ conformalClass g

Uses 1

Statement usesConformal class of a Riemannian metric

TheoremConformal scalings lie in the conformal class#✓fully proved

Let \(M\) be a \(C^\infty\) manifold modeled on a real normed space, let \(g\) be a \(C^\infty\) Riemannian metric on \(M\), and let \(u : M \to \mathbb{R}\) be a \(C^\infty\) function with \(u(x) > 0\) for all \(x \in M\). Then the conformal scaling \(u g\) of \(g\) by \(u\) lies in the conformal class of \(g\).

theorem conformalScale_mem_conformalClass (u : M → ℝ)
    (hu : ContMDiff I 𝓘(ℝ) ∞ u) (hpos : ∀ x, 0 < u x) :
    g.conformalScale u hu hpos ∈ conformalClass g

Uses 3

Statement usesConformal scaling of a Riemannian metric · Conformal class of a Riemannian metric

Proof usesInner product of a conformally scaled metric

TheoremConformal equivalence is symmetric#✓fully proved

Let \(M\) be a \(C^\infty\) manifold modeled on a real normed space, and let \(g\) and \(g'\) be \(C^\infty\) Riemannian metrics on \(M\). If \(g'\) lies in the conformal class of \(g\), then \(g\) lies in the conformal class of \(g'\).

theorem mem_conformalClass_symm :
    g' ∈ conformalClass g → g ∈ conformalClass g'

Uses 1

Statement usesConformal class of a Riemannian metric

TheoremConformal equivalence is transitive#✓fully proved

Let \(M\) be a \(C^\infty\) manifold modeled on a real normed space, and let \(g\), \(g'\) and \(g''\) be \(C^\infty\) Riemannian metrics on \(M\). If \(g'\) lies in the conformal class of \(g\) and \(g''\) lies in the conformal class of \(g'\), then \(g''\) lies in the conformal class of \(g\).

theorem mem_conformalClass_trans :
    g' ∈ conformalClass g → g'' ∈ conformalClass g' → g'' ∈ conformalClass g

Uses 1

Statement usesConformal class of a Riemannian metric

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.