The Yamabe problem and conformal scalar curvature

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremScalar curvature of a conformal metric#

In dimension n ≠ 2, let u be a positive function such that ĝ = u ^ (4 / (n - 2)) g is a smooth metric. Then the scalar curvature of ĝ is Scal_ĝ = u ^ (-(n + 2) / (n - 2)) L_g u, where L_g is the conformal Laplacian of g. Such a u is automatically smooth.

TauCeti.Yamabe.scalarCurvature_rescale_eq_rpow_mul_conformalLaplacian.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M]
  (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun x => TangentSpace I x)
  (hn : Module.finrank ℝ E ≠ 2) {u : M → ℝ} (hu_pos : ∀ (x : M), 0 < u x)
  {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun x => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))}
  {hf_pos : ∀ (x : M), 0 < u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} (x : M) :
  (g.rescale (fun x => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))) hf hf_pos).scalarCurvature x =
    u x ^ (-(↑(Module.finrank ℝ E) + 2) / (↑(Module.finrank ℝ E) - 2)) *
      TauCeti.Yamabe.conformalLaplacian I u x

Lean

Formalized in Tau Ceti as TauCeti.Yamabe.scalarCurvature_rescale_eq_rpow_mul_conformalLaplacian.

Sources

• Tau Ceti documentation: TauCeti.Yamabe.scalarCurvature_rescale_eq_rpow_mul_conformalLaplacian
• Source of TauCeti.Yamabe.scalarCurvature_rescale_eq_rpow_mul_conformalLaplacian in TauCeti/Analysis/PDE/Yamabe/ConformalLaplacian.lean
• Tau Ceti roadmap status: The Yamabe problem and conformal scalar curvature

LeanTauCeti.Yamabe.scalarCurvature_rescale_eq_rpow_mul_conformalLaplacian

Uses 3 · Used by 2

Statement usesTauCeti.Yamabe.conformalLaplacian

Proof usesCurvature under conformal change · The Koszul formula

Used byThe Yamabe equation · Volume-normalized total scalar curvature of a conformal metric

TheoremThe Yamabe equation#

In dimension n ≠ 2, let u be a positive function such that ĝ = u ^ (4 / (n - 2)) g is a smooth metric. Then ĝ has scalar curvature c at a point exactly when u solves the Yamabe equation L_g u = c u ^ (pₙ - 1) there, where pₙ = 2 n / (n - 2).

TauCeti.Yamabe.scalarCurvature_rescale_eq_iff_conformalLaplacian_eq.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M]
  (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun x => TangentSpace I x)
  (hn : Module.finrank ℝ E ≠ 2) {u : M → ℝ} (hu_pos : ∀ (x : M), 0 < u x)
  {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun x => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))}
  {hf_pos : ∀ (x : M), 0 < u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} (c : ℝ) (x : M) :
  (g.rescale (fun x => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))) hf hf_pos).scalarCurvature x = c ↔
    TauCeti.Yamabe.conformalLaplacian I u x =
      c * u x ^ (TauCeti.Yamabe.criticalExponent (Module.finrank ℝ E) - 1)

Lean

Formalized in Tau Ceti as TauCeti.Yamabe.scalarCurvature_rescale_eq_iff_conformalLaplacian_eq.

Sources

• Tau Ceti documentation: TauCeti.Yamabe.scalarCurvature_rescale_eq_iff_conformalLaplacian_eq
• Source of TauCeti.Yamabe.scalarCurvature_rescale_eq_iff_conformalLaplacian_eq in TauCeti/Analysis/PDE/Yamabe/ConformalLaplacian.lean
• Tau Ceti roadmap status: The Yamabe problem and conformal scalar curvature

LeanTauCeti.Yamabe.scalarCurvature_rescale_eq_iff_conformalLaplacian_eq

Uses 3

Statement usesTauCeti.Yamabe.conformalLaplacian

Proof usesThe Koszul formula · Scalar curvature of a conformal metric

TheoremVolume-normalized total scalar curvature of a conformal metric#

On a compact manifold of dimension n ≠ 2, let u be a positive function such that ĝ = u ^ (4 / (n - 2)) g is a smooth metric, and let pₙ = 2 n / (n - 2). Then (∫ Scal_ĝ dV_ĝ) / Vol(ĝ) ^ (2 / pₙ) = (∫ u L_g u dV_g) / (∫ u ^ pₙ dV_g) ^ (2 / pₙ), where L_g is the conformal Laplacian of g.

TauCeti.Yamabe.integral_scalarCurvature_rescale_div_riemannianTotalVolume_rpow.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] [LindelofSpace M] [CompactSpace M]
  (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun x => TangentSpace I x)
  (hn : Module.finrank ℝ E ≠ 2) {u : M → ℝ} (hu_pos : ∀ (x : M), 0 < u x)
  {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ fun x => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))}
  {hf_pos : ∀ (x : M), 0 < u x ^ (4 / (↑(Module.finrank ℝ E) - 2))} :
  (∫ (x :
        TauCeti.WithMetric
          (g.rescale (fun x => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))) hf hf_pos)),
        (g.rescale (fun x => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))) hf hf_pos).scalarCurvature
          x.ofWithMetric ∂TauCeti.riemannianVolume I
          (TauCeti.WithMetric
            (g.rescale (fun x => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))) hf hf_pos))) /
      TauCeti.riemannianTotalVolume I
          (TauCeti.WithMetric
            (g.rescale (fun x => u x ^ (4 / (↑(Module.finrank ℝ E) - 2))) hf hf_pos)) ^
        (2 / TauCeti.Yamabe.criticalExponent (Module.finrank ℝ E)) =
    (∫ (x : TauCeti.WithMetric g),
        u x.ofWithMetric *
          TauCeti.Yamabe.conformalLaplacian I u
            x.ofWithMetric ∂TauCeti.riemannianVolume I (TauCeti.WithMetric g)) /
      (∫ (x : TauCeti.WithMetric g),
          u x.ofWithMetric ^
            TauCeti.Yamabe.criticalExponent
              (Module.finrank ℝ E) ∂TauCeti.riemannianVolume I (TauCeti.WithMetric g)) ^
        (2 / TauCeti.Yamabe.criticalExponent (Module.finrank ℝ E))

Lean

Formalized in Tau Ceti as TauCeti.Yamabe.integral_scalarCurvature_rescale_div_riemannianTotalVolume_rpow.

Sources

• Tau Ceti documentation: TauCeti.Yamabe.integral_scalarCurvature_rescale_div_riemannianTotalVolume_rpow
• Source of TauCeti.Yamabe.integral_scalarCurvature_rescale_div_riemannianTotalVolume_rpow in TauCeti/Analysis/PDE/Yamabe/TotalScalarCurvature.lean
• Tau Ceti roadmap status: The Yamabe problem and conformal scalar curvature

LeanTauCeti.Yamabe.integral_scalarCurvature_rescale_div_riemannianTotalVolume_rpow

Uses 5

Statement usesTauCeti.Yamabe.conformalLaplacian

Proof usesHomeomorph.pullbackChartedSpace · Homeomorph.pullbackDiffeomorph · The Koszul formula · Scalar curvature of a conformal metric

TheoremWeyl tensor under conformal change#

Away from dimension 2, the fully covariant Weyl tensor of a conformally rescaled smooth metric f g is f times that of g: W^(f g)(u, v, w, z) = f W^g(u, v, w, z). Equivalently, the Weyl tensor of type (1, 3) is conformally invariant.

Bundle.ContMDiffRiemannianMetric.weylTensor_leviCivitaConnection_rescale.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M]
  (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun x => TangentSpace I x) {f : M → ℝ}
  (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x)
  (hn : Module.finrank ℝ E ≠ 2) (x : M) (u v w z : TangentSpace I x) :
  (((((CovariantDerivative.leviCivitaConnection I M).weylTensor x) u) v) w) z =
    f x * (((((CovariantDerivative.leviCivitaConnection I M).weylTensor x) u) v) w) z

Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.weylTensor_leviCivitaConnection_rescale.

Sources

• Tau Ceti documentation: Bundle.ContMDiffRiemannianMetric.weylTensor_leviCivitaConnection_rescale
• Source of Bundle.ContMDiffRiemannianMetric.weylTensor_leviCivitaConnection_rescale in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/Curvature/Conformal/Basic.lean
• Tau Ceti roadmap status: The Yamabe problem and conformal scalar curvature

LeanBundle.ContMDiffRiemannianMetric.weylTensor_leviCivitaConnection_rescale

Uses 2 · Used by 2

Proof usesCurvature under conformal change · The Koszul formula

Used byLocal conformal flatness forces the Weyl tensor to vanish · Weyl–Schouten in dimension three, on a model space

TheoremLocal conformal flatness forces the Weyl tensor to vanish#

Away from dimension 2, the Weyl tensor of a locally conformally flat metric vanishes at every point. This is the easy half of the Weyl–Schouten theorem.

Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.weylTensor_eq_zero.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M]
  {g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun x => TangentSpace I x}
  (hg : g.IsLocallyConformallyFlat) (hn : Module.finrank ℝ E ≠ 2) (x : M) :
  (CovariantDerivative.leviCivitaConnection I M).weylTensor x = 0

Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.weylTensor_eq_zero.

Sources

• Tau Ceti documentation: Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.weylTensor_eq_zero
• Source of Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.weylTensor_eq_zero in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/Curvature/ConformallyFlat/Basic.lean
• Tau Ceti roadmap status: The Yamabe problem and conformal scalar curvature

LeanBundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.weylTensor_eq_zero

Uses 3 · Used by 1

Statement usesBundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat

Proof usesThe Koszul formula · Weyl tensor under conformal change

Used byWeyl–Schouten in dimension three, on a model space

TheoremThe bubbles attain the Yamabe constant of the sphere#

in dimension n > 2, for Lebesgue measure, aₙ ∫ ‖dU_{t,b}‖² = Y(Sⁿ) (∫ U_{t,b} ^ pₙ) ^ (2 / pₙ). This is the equality case of the sharp Euclidean Sobolev inequality.

TauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq_eq_sphereYamabeConstant.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (hn : 2 < Module.finrank ℝ E) {t : ℝ} (ht : 0 < t) (b : E) :
  TauCeti.Yamabe.conformalCoefficient (Module.finrank ℝ E) *
      ∫ (x : E), ‖fderiv ℝ (TauCeti.Yamabe.bubble t b) x‖ ^ 2 =
    TauCeti.Yamabe.sphereYamabeConstant (Module.finrank ℝ E) *
      (∫ (x : E),
          TauCeti.Yamabe.bubble t b x ^ TauCeti.Yamabe.criticalExponent (Module.finrank ℝ E)) ^
        (2 / TauCeti.Yamabe.criticalExponent (Module.finrank ℝ E))

Lean

Formalized in Tau Ceti as TauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq_eq_sphereYamabeConstant.

Sources

• Tau Ceti documentation: TauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq_eq_sphereYamabeConstant
• Source of TauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq_eq_sphereYamabeConstant in TauCeti/Analysis/PDE/Yamabe/Bubble/SobolevQuotient.lean
• Tau Ceti roadmap status: The Yamabe problem and conformal scalar curvature

LeanTauCeti.Yamabe.conformalCoefficient_mul_integral_norm_fderiv_bubble_sq_eq_sphereYamabeConstant

Uses 1

Proof usesThe area of the unit round sphere

TheoremThe area of the unit round sphere#

|Sⁿ| = 2 π ^ ((n + 1) / 2) / Γ((n + 1) / 2).

TauCeti.roundSphereVolume_eq_two_mul_pi_rpow_div_Gamma (n : ℕ) :
  TauCeti.roundSphereVolume n = 2 * Real.pi ^ ((↑n + 1) / 2) / Real.Gamma ((↑n + 1) / 2)

Lean

Formalized in Tau Ceti as TauCeti.roundSphereVolume_eq_two_mul_pi_rpow_div_Gamma.

Sources

• Tau Ceti documentation: TauCeti.roundSphereVolume_eq_two_mul_pi_rpow_div_Gamma
• Source of TauCeti.roundSphereVolume_eq_two_mul_pi_rpow_div_Gamma in TauCeti/Geometry/Euclidean/Volume/Sphere.lean
• Tau Ceti roadmap status: The Yamabe problem and conformal scalar curvature

LeanTauCeti.roundSphereVolume_eq_two_mul_pi_rpow_div_Gamma

Used by 1

Used byThe bubbles attain the Yamabe constant of the sphere

DefinitionTauCeti.Yamabe.conformalLaplacian#

The conformal Laplacian L_g u = aₙ Δ⁺_g u + Scal_g u of a function u on a smooth Riemannian manifold of dimension n, where aₙ = 4 (n - 1) / (n - 2), Δ⁺_g = -Δ_g is the nonnegative Laplacian and Scal_g is the scalar curvature.

TauCeti.Yamabe.conformalLaplacian.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M]
  [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun x => TangentSpace I x]
  [IsContMDiffRiemannianBundle I (↑⊤) E fun x => TangentSpace I x] (u : M → ℝ) (x : M) : ℝ

Lean

Formalized in Tau Ceti as TauCeti.Yamabe.conformalLaplacian.

Sources

• Tau Ceti documentation: TauCeti.Yamabe.conformalLaplacian
• Source of TauCeti.Yamabe.conformalLaplacian in TauCeti/Analysis/PDE/Yamabe/ConformalLaplacian.lean
• Tau Ceti roadmap status: The Yamabe problem and conformal scalar curvature

LeanTauCeti.Yamabe.conformalLaplacian

Uses 1 · Used by 3

Proof usesThe Koszul formula

Used byScalar curvature of a conformal metric · The Yamabe equation · Volume-normalized total scalar curvature of a conformal metric

DefinitionBundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat#

A smooth Riemannian metric g is locally conformally flat if every point x has a neighbourhood on which a conformal rescaling f g, by a smooth positive function f, is flat: the curvature tensor of the Levi-Civita connection of f g vanishes at every point near x.

Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M]
  (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun x => TangentSpace I x) : Prop

Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat.

Sources

• Tau Ceti documentation: Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat
• Source of Bundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/Curvature/ConformallyFlat/Basic.lean
• Tau Ceti roadmap status: The Yamabe problem and conformal scalar curvature

LeanBundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat

Uses 1 · Used by 2

Proof usesThe Koszul formula

Used byLocal conformal flatness forces the Weyl tensor to vanish · Weyl–Schouten in dimension three, on a model space

DefinitionCovariantDerivative.cottonTensor#

The Cotton tensor C(u, v, w) = (∇_w P)(u, v) - (∇_v P)(u, w) of a smooth connection, where P is the Schouten tensor and ∇P is CovariantDerivative.derivSchoutenTensor. The usual formula on vector fields holds for a smooth metric (see CovariantDerivative.cottonTensor_apply_of_mdifferentiableAt); otherwise ∇P, and hence the Cotton tensor, may be 0.

CovariantDerivative.cottonTensor.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M]
  [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle (TangentSpace I)]
  (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) :
  TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] ℝ

Lean

Formalized in Tau Ceti as CovariantDerivative.cottonTensor.

Sources

• Tau Ceti documentation: CovariantDerivative.cottonTensor
• Source of CovariantDerivative.cottonTensor in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/Curvature/Cotton.lean
• Tau Ceti roadmap status: The Yamabe problem and conformal scalar curvature

LeanCovariantDerivative.cottonTensor

Used by 1

Used byWeyl–Schouten in dimension three, on a model space

TheoremWeyl–Schouten in dimension three, on a model space#

An arbitrary smooth Riemannian metric is locally conformally flat if and only if its Cotton tensor vanishes.

Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_iff_cottonTensor_eq_zero_model_space.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  (g :
    Bundle.ContMDiffRiemannianMetric (modelWithCornersSelf ℝ E) (↑⊤) E fun x =>
      TangentSpace (modelWithCornersSelf ℝ E) x)
  (hn : Module.finrank ℝ E = 3) :
  g.IsLocallyConformallyFlat ↔
    ∀ (x : E),
      (CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ E) E).cottonTensor x = 0

Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_iff_cottonTensor_eq_zero_model_space.

Other forms

Weyl–Schouten in dimension at least four, on a model space. Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_iff_weylTensor_eq_zero_model_space.

Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_iff_weylTensor_eq_zero_model_space.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
  (g :
    Bundle.ContMDiffRiemannianMetric (modelWithCornersSelf ℝ E) (↑⊤) E fun x =>
      TangentSpace (modelWithCornersSelf ℝ E) x)
  (hn : 4 ≤ Module.finrank ℝ E) :
  g.IsLocallyConformallyFlat ↔
    ∀ (x : E),
      (CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ E) E).weylTensor x = 0

Sources

• Tau Ceti documentation: Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_iff_cottonTensor_eq_zero_model_space
• Source of Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_iff_cottonTensor_eq_zero_model_space in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/Curvature/ConformallyFlat/ModelSpace.lean

LeanBundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_iff_cottonTensor_eq_zero_model_space · Bundle.ContMDiffRiemannianMetric.isLocallyConformallyFlat_iff_weylTensor_eq_zero_model_space

Uses 9

Statement usesBundle.ContMDiffRiemannianMetric.IsLocallyConformallyFlat · CovariantDerivative.cottonTensor

Proof usesThe Christoffel formula of the first kind · Curvature under conformal change · The Koszul formula · Local conformal flatness forces the Weyl tensor to vanish · The Ricci identity · The second Bianchi identity · Weyl tensor under conformal change

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.