Documentation

TauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.Curvature.Weyl.Integrability

The integrability obstruction of the conformal flattening equation #

In dimension at least 3, a metric e^(2φ) g has vanishing Schouten tensor exactly when φ solves the conformal flattening equation

Hess φ = P + dφ ⊗ dφ - (|dφ|² / 2) g,

where P is the Schouten tensor of g (Bundle.ContMDiffRiemannianMetric.schoutenTensor_leviCivitaConnection_rescale_eq_zero_iff). This is a first-order system for the gradient ξ = grad φ: its right side Φ_ξ(u, v) = P(u, v) + ⟪ξ, u⟫ ⟪ξ, v⟫ - (‖ξ‖² / 2) ⟪u, v⟫ depends only on the point and the value of ξ there (CovariantDerivative.conformalFlatteningForm). Differentiating Φ_ξ along a solution, and substituting the equation for the derivative of ξ, gives the trilinear form

D_ξ(u, v, w) = (∇_w P)(u, v) + Φ_ξ(w, u) ⟪ξ, v⟫ + ⟪ξ, u⟫ Φ_ξ(w, v) - Φ_ξ(w, ξ) ⟪u, v⟫

(CovariantDerivative.conformalFlatteningDeriv), again a function of the point and of ξ alone. For a solution φ, D_(grad φ) is the covariant derivative of Hess φ (TauCeti.Manifold.mvfderiv_hessian_sub_eq_conformalFlatteningDeriv).

The Ricci identity says that (∇_w Hess φ)(u, v) - (∇_v Hess φ)(u, w) = ⟪R(w, v) grad φ, u⟫, so the system can only be solved with prescribed value ξ at a point where D_ξ(u, v, w) - D_ξ(u, w, v) = ⟪R(w, v) ξ, u⟫. The main computation of this file identifies the defect in this identity for every vector ξ, solution or not:

D_ξ(u, v, w) - D_ξ(u, w, v) - ⟪R(w, v) ξ, u⟫ = C(u, v, w) + W(w, v, u, ξ),

with C the Cotton tensor and W the Weyl tensor (CovariantDerivative.IsMetricCompatible.conformalFlatteningDeriv_sub_swap). All terms quadratic and cubic in ξ cancel, and the terms linear in ξ assemble into P ⊙ g, which turns the curvature term into the Weyl tensor. Consequently the obstruction vanishes for every ξ at a point where W = 0 and C = 0; conversely, if the system has a solution through every value ξ at x, then C = 0 and W = 0 at x. The first statement is the involutivity condition in the proof that vanishing Weyl tensor (dimension at least 4) or vanishing Cotton tensor (dimension 3) implies local conformal flatness.

The same computation applies to an arbitrary smooth φ that solves the equation only at the single point x: writing ψ = Hess φ - Φ_(grad φ) for the defect of the equation, the derivatives of ψ at x satisfy Z (ψ(X, Y)) - Y (ψ(X, Z)) = -(C(X, Y, Z) + W(Z, Y, X, grad φ)) (TauCeti.Manifold.mvfderiv_hessian_sub_conformalFlatteningForm_sub_swap). This is the form in which the Frobenius integrability condition of the equation is verified.

Main declarations #

References #

source
noncomputable def CovariantDerivative.conformalFlatteningForm {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 →ₗ[ℝ] ℝ

The right side of the conformal flattening equation Hess φ = Φ_(grad φ), Φ_ξ(u, v) = P(u, v) + ⟪ξ, u⟫ ⟪ξ, v⟫ - (‖ξ‖² / 2) ⟪u, v⟫, where P is the Schouten tensor.

Instances For
    source
    @[simp]
    theorem CovariantDerivative.conformalFlatteningForm_apply {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) (ξ u v : TangentSpace I x) :
    ((cov.conformalFlatteningForm x ξ) u) v = ((cov.schoutenTensor x) u) v + inner ℝ ξ u * inner ℝ ξ v - ‖ξ‖ ^ 2 / 2 * inner ℝ u v

    Evaluation of the right side of the conformal flattening equation.

    source
    noncomputable def CovariantDerivative.conformalFlatteningDeriv {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 →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] ℝ

    The derivative of the right side Φ_ξ of the conformal flattening equation along a solution, D_ξ(u, v, w) = (∇_w P)(u, v) + Φ_ξ(w, u) ⟪ξ, v⟫ + ⟪ξ, u⟫ Φ_ξ(w, v) - Φ_ξ(w, ξ) ⟪u, v⟫, with the derivative direction w last as in CovariantDerivative.derivSchoutenTensor.

    Instances For
      source
      @[simp]
      theorem CovariantDerivative.conformalFlatteningDeriv_apply {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) (ξ u v w : TangentSpace I x) :
      (((cov.conformalFlatteningDeriv x ξ) u) v) w = (((cov.derivSchoutenTensor x) u) v) w + ((cov.conformalFlatteningForm x ξ) w) u * inner ℝ ξ v + inner ℝ ξ u * ((cov.conformalFlatteningForm x ξ) w) v - ((cov.conformalFlatteningForm x ξ) w) ξ * inner ℝ u v

      Evaluation of the derivative of the right side of the conformal flattening equation.

      source
      theorem CovariantDerivative.IsMetricCompatible.conformalFlatteningForm_isSymm {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 ↑⊤] [IsContMDiffRiemannianBundle I 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) (ξ : TangentSpace I x) :
      (cov.conformalFlatteningForm x ξ).IsSymm

      For a metric-compatible torsion-free connection, the right side of the conformal flattening equation is symmetric.

      source
      theorem CovariantDerivative.IsMetricCompatible.conformalFlatteningDeriv_sub_swap {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 ↑⊤] [IsContMDiffRiemannianBundle I 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) (ξ u v w : TangentSpace I x) :
      (((cov.conformalFlatteningDeriv x ξ) u) v) w - (((cov.conformalFlatteningDeriv x ξ) u) w) v = inner ℝ ((((cov.curvatureTensor x) w) v) ξ) u + ((((cov.cottonTensor x) u) v) w + ((((cov.weylTensor x) w) v) u) ξ)

      The integrability obstruction of the conformal flattening equation. For a metric-compatible torsion-free connection and every tangent vector ξ, D_ξ(u, v, w) - D_ξ(u, w, v) = ⟪R(w, v) ξ, u⟫ + (C(u, v, w) + W(w, v, u, ξ)), where D_ξ is CovariantDerivative.conformalFlatteningDeriv, C the Cotton tensor and W the Weyl tensor.

      Along a solution of the equation the Ricci identity gives D_ξ(u, v, w) - D_ξ(u, w, v) = ⟪R(w, v) ξ, u⟫, so C(u, v, w) + W(w, v, u, ξ) must vanish at x for the equation to have a solution near x with gradient ξ at x.

      source
      theorem CovariantDerivative.IsMetricCompatible.conformalFlatteningDeriv_sub_swap_eq_inner_curvatureTensor {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 ↑⊤] [IsContMDiffRiemannianBundle I 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) {x : M} (hW : cov.weylTensor x = 0) (hC : cov.cottonTensor x = 0) (ξ u v w : TangentSpace I x) :
      (((cov.conformalFlatteningDeriv x ξ) u) v) w - (((cov.conformalFlatteningDeriv x ξ) u) w) v = inner ℝ ((((cov.curvatureTensor x) w) v) ξ) u

      At a point where the Weyl and Cotton tensors vanish, the integrability obstruction of the conformal flattening equation vanishes for every value ξ: D_ξ(u, v, w) - D_ξ(u, w, v) = ⟪R(w, v) ξ, u⟫.

      source
      theorem Bundle.ContMDiffRiemannianMetric.schoutenTensor_leviCivitaConnection_rescale_eq_zero_iff {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 : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {φ : M → ℝ} (hfφ : ∀ (x : M), f x = Real.exp (2 * φ x)) (hn : 3 ≤ Module.finrank ℝ E) (x : M) :
      (CovariantDerivative.leviCivitaConnection I M).schoutenTensor x = 0 ↔ ∀ (u v : TangentSpace I x), TauCeti.Manifold.hessian I φ x u v = (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm x (TauCeti.Manifold.mgradient I φ x)) u) v

      The conformal flattening equation. In dimension at least 3, the metric f g with f = e^(2φ) has vanishing Schouten tensor at x exactly when Hess φ = P + dφ ⊗ dφ - (|dφ|² / 2) g at x, where the Hessian, the gradient and the Schouten tensor P are those of g.

      source
      theorem TauCeti.Manifold.mvfderiv_conformalFlatteningForm_sub_eq_conformalFlatteningDeriv {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 : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {φ : M → ℝ} {x : M} (hφ : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) 2 φ x) (hHx : ∀ (u v : TangentSpace I x), hessian I φ x u v = (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm x (mgradient I φ x)) u) v) {X Y : (x : M) → TangentSpace I x} (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (w : TangentSpace I x) :
      ((d% fun (y : M) => (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm y (mgradient I φ y)) (X y)) (Y y)) x) w - (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm x (mgradient I φ x)) ((↑(CovariantDerivative.leviCivitaConnection I M) X x) w)) (Y x) - (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm x (mgradient I φ x)) (X x)) ((↑(CovariantDerivative.leviCivitaConnection I M) Y x) w) = ((((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningDeriv x (mgradient I φ x)) (X x)) (Y x)) w

      If the Hessian of φ at x is the right side Φ_(grad φ x) of the conformal flattening equation, then the covariant derivative at x of the field of bilinear forms y ↦ Φ_(grad φ y) is D_(grad φ x): (∇_w Φ_(grad φ))(X, Y) = D_(grad φ x)(X, Y, w), where (∇_w Φ_(grad φ))(X, Y) = w (Φ_(grad φ)(X, Y)) - Φ_(grad φ)(∇_w X, Y) - Φ_(grad φ)(X, ∇_w Y) and D is CovariantDerivative.conformalFlatteningDeriv for the Levi-Civita connection. Only the equation at the single point x is used: it replaces the Hessian of φ, which appears in the derivative of grad φ, by Φ_(grad φ x).

      source
      theorem TauCeti.Manifold.mvfderiv_hessian_sub_eq_conformalFlatteningDeriv {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 : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {φ : M → ℝ} {x : M} (hφ : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) 2 φ x) (hsol : ∀ᶠ (y : M) in nhds x, ∀ (u v : TangentSpace I y), hessian I φ y u v = (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm y (mgradient I φ y)) u) v) {X Y : (x : M) → TangentSpace I x} (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (w : TangentSpace I x) :
      ((d% fun (y : M) => hessian I φ y (X y) (Y y)) x) w - hessian I φ x ((↑(CovariantDerivative.leviCivitaConnection I M) X x) w) (Y x) - hessian I φ x (X x) ((↑(CovariantDerivative.leviCivitaConnection I M) Y x) w) = ((((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningDeriv x (mgradient I φ x)) (X x)) (Y x)) w

      Along a solution φ of the conformal flattening equation Hess φ = Φ_(grad φ) near x, the covariant derivative of the Hessian is D_(grad φ): (∇_w Hess φ)(X, Y) = D_(grad φ)(X, Y, w), where (∇_w Hess φ)(X, Y) = w (Hess φ(X, Y)) - Hess φ(∇_w X, Y) - Hess φ(X, ∇_w Y) and D is CovariantDerivative.conformalFlatteningDeriv for the Levi-Civita connection.

      source
      theorem TauCeti.Manifold.mvfderiv_hessian_sub_conformalFlatteningForm_sub_swap {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 : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {φ : M → ℝ} (hφ : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) φ) {x : M} (hHx : ∀ (u v : TangentSpace I x), hessian I φ x u v = (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm x (mgradient I φ x)) u) v) {X Y Z : (x : M) → TangentSpace I x} (hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩) (hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩) (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) :
      ((d% fun (y : M) => hessian I φ y (X y) (Y y) - (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm y (mgradient I φ y)) (X y)) (Y y)) x) (Z x) - ((d% fun (y : M) => hessian I φ y (X y) (Z y) - (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm y (mgradient I φ y)) (X y)) (Z y)) x) (Y x) = -(((((CovariantDerivative.leviCivitaConnection I M).cottonTensor x) (X x)) (Y x)) (Z x) + (((((CovariantDerivative.leviCivitaConnection I M).weylTensor x) (Z x)) (Y x)) (X x)) (mgradient I φ x))

      The integrability defect of the conformal flattening equation along a function. Let φ be smooth, with Hess φ = Φ_(grad φ) at the single point x, and write ψ(X, Y) = Hess φ(X, Y) - Φ_(grad φ)(X, Y) for the defect of the equation. For smooth vector fields X, Y, Z, the derivatives of ψ at x satisfy Z (ψ(X, Y)) - Y (ψ(X, Z)) = -(C(X, Y, Z) + W(Z, Y, X, grad φ)), with C the Cotton tensor and W the Weyl tensor of the Levi-Civita connection. Thus where C and W vanish, the first derivatives at x of the defect are symmetric in this sense: this is the Frobenius integrability condition of the equation, written invariantly.

      source
      theorem TauCeti.Manifold.cottonTensor_add_weylTensor_eq_zero_of_eventually_hessian_eq {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 : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {φ : M → ℝ} (hφ : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) φ) {x : M} (hsol : ∀ᶠ (y : M) in nhds x, ∀ (u v : TangentSpace I y), hessian I φ y u v = (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm y (mgradient I φ y)) u) v) (u v w : TangentSpace I x) :
      ((((CovariantDerivative.leviCivitaConnection I M).cottonTensor x) u) v) w + (((((CovariantDerivative.leviCivitaConnection I M).weylTensor x) w) v) u) (mgradient I φ x) = 0

      The integrability condition of the conformal flattening equation. If a smooth φ solves Hess φ = P + dφ ⊗ dφ - (|dφ|² / 2) g near x, then the Cotton and Weyl tensors of the Levi-Civita connection satisfy C(u, v, w) + W(w, v, u, grad φ) = 0 at x.

      source
      theorem TauCeti.Manifold.cottonTensor_eq_zero_of_eventually_hessian_eq {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 : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {φ : M → ℝ} (hφ : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) φ) {x : M} (hx : mgradient I φ x = 0) (hsol : ∀ᶠ (y : M) in nhds x, ∀ (u v : TangentSpace I y), hessian I φ y u v = (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm y (mgradient I φ y)) u) v) :
      (CovariantDerivative.leviCivitaConnection I M).cottonTensor x = 0

      If the conformal flattening equation has a smooth solution near x whose gradient vanishes at x, then the Cotton tensor of the Levi-Civita connection vanishes at x.

      source
      theorem TauCeti.Manifold.weylTensor_eq_zero_of_forall_exists_eventually_hessian_eq {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 : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {x : M} (hsol : ∀ (ξ : TangentSpace I x), ∃ (φ : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) φ ∧ mgradient I φ x = ξ ∧ ∀ᶠ (y : M) in nhds x, ∀ (u v : TangentSpace I y), hessian I φ y u v = (((CovariantDerivative.leviCivitaConnection I M).conformalFlatteningForm y (mgradient I φ y)) u) v) :
      (CovariantDerivative.leviCivitaConnection I M).weylTensor x = 0

      If the conformal flattening equation has a smooth solution near x through every value grad φ x = ξ of the gradient at x, then the Weyl tensor of the Levi-Civita connection vanishes at x.