Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.KineticEnergy

Imports

/-
Copyright (c) 2026 Nathaneal Sajan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Nathaneal Sajan
-/
module

public import Physlib.ClassicalMechanics.HarmonicOscillator.Basic
public import Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.Basic
public import Mathlib.Geometry.Manifold.VectorBundle.Riemannian

Geometric kinetic energy of the harmonic oscillator

i. Overview

The configuration space of the geometric harmonic oscillator is ConfigurationSpace. At a configuration q, velocities are tangent vectors in TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q.

The oscillator mass determines a Riemannian metric on ConfigurationSpace. At each configuration q, the metric is the mass-scaled Euclidean inner product on tangent vectors, recorded by massMetricVal S q.

The kinetic energy associated with this mass metric is geometricKineticEnergy S q v = (1 / 2 : ℝ) * S.massRiemannianMetric.inner q v v. In coordinates this gives the standard expression (1 / 2 : ℝ) * S.m * ⟪tangentCoord q v, tangentCoord q v⟫_ℝ.

ii. Key results

massRiemannianMetric : the mass-scaled Euclidean inner product as a Riemannian metric on ConfigurationSpace.

geometricKineticEnergy : the geometric kinetic-energy function associated to the oscillator mass metric.

massRiemannianMetric_inner_apply : evaluation of the mass metric in global tangent coordinates.

massRiemannianMetric_pos : positive definiteness of the mass Riemannian metric.

geometricKineticEnergy_massMetric_eq : the metric-induced kinetic energy for the oscillator mass metric is the mass-scaled coordinate kinetic energy.

iii. Table of contents

A. Pointwise mass metric

B. Riemannian mass metric

C. Geometric kinetic energy

D. Coordinate formula

iv. References

Ivo Terek, Introductory Variational Calculus on Manifolds, pages 1-2.

@[expose] public section

-- Let Lean use the definitional tangent-coordinate identification in the metric proofs.
set_option backward.isDefEq.respectTransparency false

A. Pointwise mass metric

The pointwise mass metric is the mass-scaled Euclidean inner product in global tangent coordinates. Its positivity, boundedness, and smoothness properties are established here before assembling the Riemannian metric.

Applying the mass metric value to two tangent vectors gives the mass-scaled Euclidean inner product of their coordinate representatives.

lemma massMetricVal_apply
    (S : HarmonicOscillator) (q : ConfigurationSpace)
    (v w : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q) :
    massMetricVal S q v w = S.m * ⟪tangentCoord q v, tangentCoord q w⟫_ℝ := byS:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) qw:TangentSpace (𝓡 1) q⊢ ((S.massMetricVal q) v) w = S.m * ⟪(tangentCoord q) v, (tangentCoord q) w⟫_ℝ
  rflAll goals completed! 🐙

A nonzero tangent vector has nonzero coordinate representative under tangentCoord.

lemma tangentCoord_ne_zero {q : ConfigurationSpace}
    {v : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q}
    (hv : v ≠ 0) : tangentCoord q v ≠ 0 := byq:ConfigurationSpacev:TangentSpace (𝓡 1) qhv:v ≠ 0⊢ (tangentCoord q) v ≠ 0
  intro hq:ConfigurationSpacev:TangentSpace (𝓡 1) qhv:v ≠ 0h:(tangentCoord q) v = 0⊢ False
  apply hvq:ConfigurationSpacev:TangentSpace (𝓡 1) qhv:v ≠ 0h:(tangentCoord q) v = 0⊢ v = 0
  exact (tangentCoord q).injective (byq:ConfigurationSpacev:TangentSpace (𝓡 1) qhv:v ≠ 0h:(tangentCoord q) v = 0⊢ (tangentCoord q) v = (tangentCoord q) 0 simpa using hAll goals completed! 🐙)

The oscillator mass metric is positive on nonzero tangent vectors.


lemma massMetricVal_pos
    (S : HarmonicOscillator) (q : ConfigurationSpace)
    (v : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q) (hv : v ≠ 0) :
    0 < massMetricVal S q v v := byS:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) qhv:v ≠ 0⊢ 0 < ((S.massMetricVal q) v) v
  rw [massMetricVal_applyS:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) qhv:v ≠ 0⊢ 0 < S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝS:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) qhv:v ≠ 0⊢ 0 < S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝ]S:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) qhv:v ≠ 0⊢ 0 < S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝ
  exact mul_pos S.m_pos (real_inner_self_pos.mpr (tangentCoord_ne_zero hv))All goals completed! 🐙

The mass metric unit ball is bounded in the model norm.


lemma massMetricVal_isVonNBounded
    (S : HarmonicOscillator) (q : ConfigurationSpace) :
    IsVonNBounded ℝ
      {v : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q | massMetricVal S q v v < 1} := byS:HarmonicOscillatorq:ConfigurationSpace⊢ IsVonNBounded ℝ {v | ((S.massMetricVal q) v) v < 1}
  change IsVonNBounded ℝ
    {v : EuclideanSpace ℝ (Fin 1) | S.m * ⟪v, v⟫_ℝ < 1}S:HarmonicOscillatorq:ConfigurationSpace⊢ IsVonNBounded ℝ {v | S.m * ⟪v, v⟫_ℝ < 1}
  rw [NormedSpace.isVonNBounded_iff'S:HarmonicOscillatorq:ConfigurationSpace⊢ ∃ r, ∀ x ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}, ‖x‖ ≤ rS:HarmonicOscillatorq:ConfigurationSpace⊢ ∃ r, ∀ x ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}, ‖x‖ ≤ r]S:HarmonicOscillatorq:ConfigurationSpace⊢ ∃ r, ∀ x ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}, ‖x‖ ≤ r
  refine ⟨Real.sqrt (1 / S.m), ?_⟩S:HarmonicOscillatorq:ConfigurationSpace⊢ ∀ x ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}, ‖x‖ ≤ √(1 / S.m)
  intro v hvS:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}⊢ ‖v‖ ≤ √(1 / S.m)
  have hv' : S.m * ⟪v, v⟫_ℝ < 1 := byS:HarmonicOscillatorq:ConfigurationSpace⊢ IsVonNBounded ℝ {v | ((S.massMetricVal q) v) v < 1}S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ⟪v, v⟫_ℝ < 1⊢ ‖v‖ ≤ √(1 / S.m) simpa using hvS:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ⟪v, v⟫_ℝ < 1⊢ ‖v‖ ≤ √(1 / S.m)S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ⟪v, v⟫_ℝ < 1⊢ ‖v‖ ≤ √(1 / S.m)
  rw [real_inner_self_eq_norm_sqS:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1⊢ ‖v‖ ≤ √(1 / S.m)S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1⊢ ‖v‖ ≤ √(1 / S.m)] at hv'S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1⊢ ‖v‖ ≤ √(1 / S.m)
  have hmul : S.m * ‖v‖ ^ 2 < 1 := hv'S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1⊢ ‖v‖ ≤ √(1 / S.m)
  have hsq_le : ‖v‖ ^ 2 ≤ 1 / S.m := byS:HarmonicOscillatorq:ConfigurationSpace⊢ IsVonNBounded ℝ {v | ((S.massMetricVal q) v) v < 1}S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_le:‖v‖ ^ 2 ≤ 1 / S.m⊢ ‖v‖ ≤ √(1 / S.m)
    have hsq_lt : ‖v‖ ^ 2 < 1 / S.m := byS:HarmonicOscillatorq:ConfigurationSpace⊢ IsVonNBounded ℝ {v | ((S.massMetricVal q) v) v < 1}S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_lt:‖v‖ ^ 2 < 1 / S.m⊢ ‖v‖ ^ 2 ≤ 1 / S.mS:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_le:‖v‖ ^ 2 ≤ 1 / S.m⊢ ‖v‖ ≤ √(1 / S.m)
      rw [lt_div_iff₀ S.m_posS:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1⊢ ‖v‖ ^ 2 * S.m < 1S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1⊢ ‖v‖ ^ 2 * S.m < 1S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_lt:‖v‖ ^ 2 < 1 / S.m⊢ ‖v‖ ^ 2 ≤ 1 / S.mS:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_le:‖v‖ ^ 2 ≤ 1 / S.m⊢ ‖v‖ ≤ √(1 / S.m)]S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1⊢ ‖v‖ ^ 2 * S.m < 1S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_lt:‖v‖ ^ 2 < 1 / S.m⊢ ‖v‖ ^ 2 ≤ 1 / S.mS:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_le:‖v‖ ^ 2 ≤ 1 / S.m⊢ ‖v‖ ≤ √(1 / S.m)
      nlinarith [hmul]S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_lt:‖v‖ ^ 2 < 1 / S.m⊢ ‖v‖ ^ 2 ≤ 1 / S.mS:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_le:‖v‖ ^ 2 ≤ 1 / S.m⊢ ‖v‖ ≤ √(1 / S.m)S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_lt:‖v‖ ^ 2 < 1 / S.m⊢ ‖v‖ ^ 2 ≤ 1 / S.mS:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_le:‖v‖ ^ 2 ≤ 1 / S.m⊢ ‖v‖ ≤ √(1 / S.m)
    exact hsq_lt.leS:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_le:‖v‖ ^ 2 ≤ 1 / S.m⊢ ‖v‖ ≤ √(1 / S.m)S:HarmonicOscillatorq:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)hv:v ∈ {v | S.m * ⟪v, v⟫_ℝ < 1}hv':S.m * ‖v‖ ^ 2 < 1hmul:S.m * ‖v‖ ^ 2 < 1hsq_le:‖v‖ ^ 2 ≤ 1 / S.m⊢ ‖v‖ ≤ √(1 / S.m)
  exact Real.le_sqrt_of_sq_le hsq_leAll goals completed! 🐙

The oscillator mass metric is constant in the global tangent-bundle chart.


lemma massMetricVal_contMDiff (S : HarmonicOscillator) :
    ContMDiff 𝓘(ℝ, EuclideanSpace ℝ (Fin 1))
      (𝓘(ℝ, EuclideanSpace ℝ (Fin 1)).prod
        𝓘(ℝ, EuclideanSpace ℝ (Fin 1) →L[ℝ]
          EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ)) ω
      (fun q : ConfigurationSpace =>
        TotalSpace.mk'
          (EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ)
          (E := fun q : ConfigurationSpace =>
            TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q →L[ℝ]
              TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q →L[ℝ] ℝ)
          q (massMetricVal S q)) := byS:HarmonicOscillator⊢ ContMDiff (𝓡 1) ((𝓡 1).prod 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ)) ω fun q =>
  ⟨q, S.massMetricVal q⟩
  intro xS:HarmonicOscillatorx:ConfigurationSpace⊢ ContMDiffAt (𝓡 1) ((𝓡 1).prod 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ)) ω
  (fun q => ⟨q, S.massMetricVal q⟩) x
  rw [contMDiffAt_sectionS:HarmonicOscillatorx:ConfigurationSpace⊢ ContMDiffAt (𝓡 1) 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ) ω
  (fun x_1 =>
    (↑(trivializationAt (EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ)
            (fun x => TangentSpace (𝓡 1) x →L[ℝ] TangentSpace (𝓡 1) x →L[ℝ] ℝ) x)
        ⟨x_1, S.massMetricVal x_1⟩).2)
  xS:HarmonicOscillatorx:ConfigurationSpace⊢ ContMDiffAt (𝓡 1) 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ) ω
  (fun x_1 =>
    (↑(trivializationAt (EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ)
            (fun x => TangentSpace (𝓡 1) x →L[ℝ] TangentSpace (𝓡 1) x →L[ℝ] ℝ) x)
        ⟨x_1, S.massMetricVal x_1⟩).2)
  x]S:HarmonicOscillatorx:ConfigurationSpace⊢ ContMDiffAt (𝓡 1) 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ) ω
  (fun x_1 =>
    (↑(trivializationAt (EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ)
            (fun x => TangentSpace (𝓡 1) x →L[ℝ] TangentSpace (𝓡 1) x →L[ℝ] ℝ) x)
        ⟨x_1, S.massMetricVal x_1⟩).2)
  x
  convert! contMDiffAt_const (c := S.m • (innerSL ℝ :
    EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ))e'_22S:HarmonicOscillatorx:ConfigurationSpacex✝:ConfigurationSpace⊢ (↑(trivializationAt (EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ)
          (fun x => TangentSpace (𝓡 1) x →L[ℝ] TangentSpace (𝓡 1) x →L[ℝ] ℝ) x)
      ⟨x✝, S.massMetricVal x✝⟩).2 =
  S.m • innerSL ℝ
  ext v we'_22S:HarmonicOscillatorx:ConfigurationSpacex✝:ConfigurationSpacev:EuclideanSpace ℝ (Fin 1)w:EuclideanSpace ℝ (Fin 1)⊢ ((↑(trivializationAt (EuclideanSpace ℝ (Fin 1) →L[ℝ] EuclideanSpace ℝ (Fin 1) →L[ℝ] ℝ)
              (fun x => TangentSpace (𝓡 1) x →L[ℝ] TangentSpace (𝓡 1) x →L[ℝ] ℝ) x)
          ⟨x✝, S.massMetricVal x✝⟩).2
      v)
    w =
  ((S.m • innerSL ℝ) v) w
  simp [hom_trivializationAt_apply, ContinuousLinearMap.inCoordinates, massMetricVal, TangentSpace]All goals completed! 🐙

B. Riemannian mass metric

The pointwise bilinear forms assemble into a ContMDiffRiemannianMetric on the oscillator configuration space.

C. Geometric kinetic energy

The geometric kinetic energy is defined directly from the oscillator's mass Riemannian metric.

The geometric kinetic energy is one half the mass Riemannian metric applied to v twice.

lemma geometricKineticEnergy_eq
    (S : HarmonicOscillator) (q : ConfigurationSpace)
    (v : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q) :
    geometricKineticEnergy S q v =
      (1 / 2 : ℝ) * S.massRiemannianMetric.inner q v v := byS:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) q⊢ S.geometricKineticEnergy q v = 1 / 2 * ((S.massRiemannianMetric.inner q) v) v
  rflAll goals completed! 🐙

D. Coordinate formula

The coordinate identities below recover the usual mass-scaled formula for kinetic energy.

The oscillator mass Riemannian metric is positive definite.

lemma massRiemannianMetric_pos
    (S : HarmonicOscillator) (q : ConfigurationSpace)
    (v : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q)
    (hv : v ≠ 0) :
    0 < S.massRiemannianMetric.inner q v v :=
  massMetricVal_pos S q v hv

In the global coordinate, the oscillator mass metric is the mass-scaled Euclidean inner product of coordinate representatives.

lemma massRiemannianMetric_inner_apply
    (S : HarmonicOscillator) (q : ConfigurationSpace)
    (v w : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q) :
    S.massRiemannianMetric.inner q v w =
      S.m * ⟪tangentCoord q v, tangentCoord q w⟫_ℝ := byS:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) qw:TangentSpace (𝓡 1) q⊢ ((S.massRiemannianMetric.inner q) v) w = S.m * ⟪(tangentCoord q) v, (tangentCoord q) w⟫_ℝ
  exact massMetricVal_apply S q v wAll goals completed! 🐙

The metric-induced kinetic energy for the mass metric has the standard harmonic-oscillator coordinate form.


lemma geometricKineticEnergy_massMetric_eq
    (S : HarmonicOscillator) (q : ConfigurationSpace)
    (v : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q) :
    geometricKineticEnergy S q v =
      (1 / 2 : ℝ) * S.m * ⟪tangentCoord q v, tangentCoord q v⟫_ℝ := byS:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) q⊢ S.geometricKineticEnergy q v = 1 / 2 * S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝ
  rw [geometricKineticEnergy_eq,S:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) q⊢ 1 / 2 * ((S.massRiemannianMetric.inner q) v) v = 1 / 2 * S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝS:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) q⊢ 1 / 2 * (S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝ) = 1 / 2 * S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝ massRiemannianMetric_inner_applyS:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) q⊢ 1 / 2 * (S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝ) = 1 / 2 * S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝS:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) q⊢ 1 / 2 * (S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝ) = 1 / 2 * S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝ]S:HarmonicOscillatorq:ConfigurationSpacev:TangentSpace (𝓡 1) q⊢ 1 / 2 * (S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝ) = 1 / 2 * S.m * ⟪(tangentCoord q) v, (tangentCoord q) v⟫_ℝ
  ringAll goals completed! 🐙