The Levi-Civita connection in the upper half-space

Compute the Levi-Civita connection of the metric (‖dx‖² + dt²) / t² on constant coordinate fields and identify its Christoffel map. These formulas give the connection coefficients used to compute the curvature of the upper-half-space model. They hold over any finite-dimensional real inner product space of horizontal coordinates, including dimension zero.

The Euclidean inner product in the formulas is the model-space inner product; the tangent metric is divided by the square of the height. The order of the Christoffel-map arguments follows the local-frame API: field value first, differentiation direction second.

The calculation uses Mathlib's CovariantDerivative.leviCivitaConnection through the Koszul formula, and the existing inherited tangent-bundle trivializations of open submanifolds.

References

• J. M. Lee, Introduction to Riemannian Manifolds, second edition, Chapter 3 (upper half-space metric) and Theorem 5.10 (Koszul formula).

noncomputable def TauCeti.UpperHalfSpace.constantField {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : WithLp 2 (E × ℝ)) (x : UpperHalfSpace E) : TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x

The vector field with constant value v in the inherited upper-half-space coordinates.

@[simp]

theorem TauCeti.UpperHalfSpace.constantField_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : WithLp 2 (E × ℝ)) (x : UpperHalfSpace E) : constantField v x = (tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x).symm v

The value of a constant coordinate vector field.

theorem TauCeti.UpperHalfSpace.contMDiff_constantField {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (v : WithLp 2 (E × ℝ)) : ContMDiff (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) ((modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))).prod (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ)))) ↑⊤ fun (y : UpperHalfSpace E) => ⟨y, constantField v y⟩

Constant coordinate fields are smooth as sections of the tangent bundle.

@[simp]

theorem TauCeti.UpperHalfSpace.mlieBracket_constantField {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (u v : WithLp 2 (E × ℝ)) (x : UpperHalfSpace E) : VectorField.mlieBracket (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) (constantField u) (constantField v) x = 0

Constant coordinate fields commute.

@[simp]

theorem TauCeti.UpperHalfSpace.leviCivitaConnection_const_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (x : UpperHalfSpace E) (u v : WithLp 2 (E × ℝ)) : (tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) ((↑(CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) (UpperHalfSpace E)) (constantField v) x) ((tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x).symm u)) = x.height⁻¹ • (inner ℝ u v • WithLp.toLp 2 (0, 1) - u.snd • v - v.snd • u)

In the upper-half-space coordinates, the Levi-Civita derivative of the constant field v in direction u is (⟪u,v⟫ eₜ - uₜ v - vₜ u) / t, where eₜ is the vertical unit vector. The tangent-space identifications read the result in the Euclidean model.

@[simp]

theorem TauCeti.UpperHalfSpace.christoffelMap_leviCivitaConnection_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℝ (WithLp 2 (E × ℝ))) (x : UpperHalfSpace E) (u v : WithLp 2 (E × ℝ)) : ((Manifold.christoffelMap b ⋯ x) v) u = x.height⁻¹ • (inner ℝ u v • WithLp.toLp 2 (0, 1) - u.snd • v - v.snd • u)

The Christoffel map of the upper-half-space metric in its inherited coordinates, independently of the finite basis used to construct the map. The first input v is the field value and the second input u is the direction of differentiation.