hessianMetric

formal source

 137
 138    This is the natural Riemannian metric on the cost manifold induced
 139    by the second derivative of `Jcost`. -/
 140noncomputable def hessianMetric (x : ℝ) : ℝ := x ^ (-3 : ℤ)
 141
 142@[simp] lemma hessianMetric_eq {x : ℝ} (_hx : 0 < x) :
 143    hessianMetric x = 1 / x ^ 3 := by
 144  unfold hessianMetric
 145  rw [zpow_neg, zpow_ofNat, one_div]
 146
 147/-- The Christoffel symbol of the Hessian metric `g(x) = 1/x³`.
 148
 149    For a 1D metric, `Γ = (1/2g) (dg/dx) = (1/2) · x³ · (-3 x⁻⁴) = -3/(2x)`. -/
 150noncomputable def christoffel (x : ℝ) : ℝ := -3 / (2 * x)
 151
 152/-- The geodesic equation for the Hessian metric.
 153
 154    A path `γ` satisfies `γ̈ + Γ(γ) γ̇² = 0`, where `Γ` is the
 155    Christoffel symbol of `g(x) = 1/x³`. -/
 156def geodesicEquationHolds (γ : ℝ → ℝ) : Prop :=
 157  ∀ t : ℝ, deriv (deriv γ) t + christoffel (γ t) * (deriv γ t) ^ 2 = 0
 158
 159/-- The geodesic equation is the Euler–Lagrange equation of the
 160    Hessian-energy action `E[γ] = ∫ ½ g(γ) γ̇² dt`.
 161
 162    This is a standard fact of Riemannian geometry: for a metric
 163    `g(x)` in 1D, the EL equation of the energy functional
 164    `E[γ] = ∫ ½ g(γ) γ̇² dt` is exactly the geodesic equation
 165    `γ̈ + Γ(γ) γ̇² = 0` with `Γ = (1/2g) g'`.
 166
 167    We record this as a definitional equivalence (the names of the two
 168    equations refer to the same mathematical object). The full proof of
 169    one direction (the geodesic family `γ(t) = (at+b)^(-2)` satisfies
 170    the equation) is in