Finsler metrics

8 fully proved

Manifold

StructureFinsler metric#✓fully proved

Let \(M\) be a \(C^\infty\) manifold (possibly with boundary or corners) modelled on a finite-dimensional real normed space \(E\), so that each tangent space \(T_xM\) is \(E\). A \(C^\infty\) Finsler metric on \(M\) is a continuous function \(F : TM \to \mathbb{R}\) that is \(C^\infty\) off the zero section, satisfies \(F(x, v) > 0\) for every \(x \in M\) and every nonzero \(v \in T_xM\), is positively homogeneous of degree one on each fiber, that is \(F(x, cv) = c\,F(x, v)\) for all \(x \in M\), \(v \in T_xM\) and real \(c > 0\), and is strongly convex: for every \(x \in M\) and all nonzero \(v, w \in E\), the second derivative at \(v\) of the function \(u \mapsto F(x, u)^2\) on \(E\) satisfies \(D^2\big(F(x, \cdot)^2\big)(v)(w, w) > 0\).

structure FinslerMetric [FiniteDimensional ℝ E] where
  /-- The Finsler function `F : TM → ℝ`. -/
  toFun : TangentBundle I M → ℝ
  continuous_toFun : Continuous toFun
  contMDiffOn_toFun : ContMDiffOn I.tangent 𝓘(ℝ, ℝ) ∞ toFun {v | v.2 ≠ 0}
  pos : ∀ v : TangentBundle I M, v.2 ≠ 0 → 0 < toFun v
  homogeneous : ∀ (x : M) (v : TangentSpace I x) (c : ℝ), 0 < c →
    toFun ⟨x, c • v⟩ = c * toFun ⟨x, v⟩
  hessian_pos : ∀ (x : M) (v w : E), v ≠ 0 → w ≠ 0 →
    0 < fderiv ℝ (fderiv ℝ fun u : E ↦ toFun ⟨x, u⟩ ^ 2) v w w

Sources

• Bao–Chern–Shen, An Introduction to Riemann–Finsler Geometry, §1.1, where \(F\) takes values in \([0, \infty)\) and the Hessian is that of \(F^2/2\).

Used by 6

Used byForward Finsler distance · Euclidean Finsler metric · Closed Finsler geodesic · Finsler geodesic · Finsler geodesic of given speed on a set of times · Reversible Finsler metric

Finsler Metric

DefinitionReversible Finsler metric#✓fully proved

A Finsler metric \(F\) on a manifold \(M\) is reversible if \(F(x, -v) = F(x, v)\) for every point \(x \in M\) and every tangent vector \(v \in T_xM\).

def IsReversible (F : FinslerMetric I M) : Prop :=
  ∀ v : TangentBundle I M, F ⟨v.proj, -v.2⟩ = F v

Uses 1 · Used by 1

Statement usesFinsler metric

Used byThe Euclidean Finsler metric is reversible

DefinitionForward Finsler distance#✓fully proved

Let \(F\) be a Finsler metric on a manifold \(M\). The forward Finsler distance from \(x \in M\) to \(y \in M\) is the value in \([0, \infty]\)

\[ d_F(x, y) = \inf_\gamma \int_0^1 F(\gamma(t), \gamma'(t))\, dt, \]

the infimum over all \(C^1\) paths \(\gamma : [0, 1] \to M\) from \(x\) to \(y\); it is \(\infty\) when there is no such path.

It is not symmetric unless \(F\) is reversible.

def edist (F : FinslerMetric I M) (x y : M) : ℝ≥0∞ :=
  ⨅ (γ : Path x y) (_ : CMDiff 1 γ), ∫⁻ t, ENNReal.ofReal (F ⟨γ t, mfderiv% γ t 1⟩)

Sources

• Bao–Chern–Shen, An Introduction to Riemann–Finsler Geometry, §6.2. The formula is that of Mathlib's riemannianEDist with ‖v‖ₑ replaced by F v.

Uses 1 · Used by 1

Statement usesFinsler metric

Used byFinsler geodesic of given speed on a set of times

DefinitionFinsler geodesic of given speed on a set of times#✓fully proved

Let \(F\) be a Finsler metric on a manifold \(M\) with forward distance \(d_F\), let \(\gamma : \mathbb{R} \to M\) be a curve, let \(s \subseteq \mathbb{R}\) be a set of times and let \(c \ge 0\) be a real number. Then \(\gamma\) is a geodesic of speed \(c\) of \(F\) on \(s\) if for every \(t \in s\) there is \(\varepsilon > 0\) such that \(d_F(\gamma(t_1), \gamma(t_2)) = c\,(t_2 - t_1)\) for all \(t_1, t_2 \in s\) with \(t_1 \le t_2\), \(|t_1 - t| < \varepsilon\) and \(|t_2 - t| < \varepsilon\).

def IsGeodesicOnWithSpeed (F : FinslerMetric I M) (γ : ℝ → M) (s : Set ℝ) (c : ℝ≥0) : Prop :=
  ∀ t ∈ s, ∃ ε > (0 : ℝ), ∀ t₁ ∈ s, ∀ t₂ ∈ s, |t₁ - t| < ε → |t₂ - t| < ε → t₁ ≤ t₂ →
    F.edist (γ t₁) (γ t₂) = c * ENNReal.ofReal (t₂ - t₁)

Uses 2 · Used by 1

Statement usesFinsler metric · Forward Finsler distance

Used byFinsler geodesic

DefinitionFinsler geodesic#✓fully proved

Let \(F\) be a Finsler metric on a manifold \(M\). A curve \(\gamma : \mathbb{R} \to M\) is a geodesic of \(F\) if there is a real number \(c \ge 0\) such that \(\gamma\) is a geodesic of speed \(c\) of \(F\) on all of \(\mathbb{R}\).

def IsGeodesic (F : FinslerMetric I M) (γ : ℝ → M) : Prop :=
  ∃ c : ℝ≥0, F.IsGeodesicOnWithSpeed γ univ c

Uses 2 · Used by 1

Statement usesFinsler metric · Finsler geodesic of given speed on a set of times

Used byClosed Finsler geodesic

DefinitionClosed Finsler geodesic#✓fully proved

Let \(F\) be a Finsler metric on a manifold \(M\). A curve \(\gamma : \mathbb{R} \to M\) is a closed geodesic of \(F\) if it is a geodesic of \(F\), it is periodic with some period \(T > 0\), that is \(\gamma(t + T) = \gamma(t)\) for all real \(t\), and it is not constant: \(\gamma(t_1) \ne \gamma(t_2)\) for some real \(t_1, t_2\).

def IsClosedGeodesic (F : FinslerMetric I M) (γ : ℝ → M) : Prop :=
  F.IsGeodesic γ ∧ (∃ T > 0, Function.Periodic γ T) ∧ ∃ t₁ t₂, γ t₁ ≠ γ t₂

Uses 2

Statement usesFinsler metric · Finsler geodesic

DefinitionEuclidean Finsler metric#✓fully proved

Let \(V\) be a finite-dimensional real inner product space, viewed as a smooth manifold whose tangent spaces are \(V\) itself. The Euclidean Finsler metric on \(V\) is \(F(x, v) = \|v\|\) for \(x \in V\) and \(v \in T_xV = V\).

Manifold.FinslerMetric.euclidean · 19 lines

def euclidean : FinslerMetric 𝓘(ℝ, F) F where
  toFun v := ‖@id F v.2‖
  continuous_toFun := continuous_norm.comp
    ((contMDiff_snd_tangentBundle_modelSpace F 𝓘(ℝ, F) (n := 0)).continuous)
  contMDiffOn_toFun := by
    intro v hv
    have h1 := (contMDiff_snd_tangentBundle_modelSpace F 𝓘(ℝ, F) (n := ∞)).contMDiffAt (x := v)
    have h2 : ContMDiffAt 𝓘(ℝ, F) 𝓘(ℝ, ℝ) ∞ (fun w : F ↦ ‖w‖) (@id F v.2) :=
      (contDiffAt_norm ℝ (show @id F v.2 ≠ 0 from hv)).contMDiffAt
    exact (h2.comp v h1).contMDiffWithinAt
  pos v hv := norm_pos_iff.mpr (show @id F v.2 ≠ 0 from hv)
  homogeneous x v c hc := by
    change ‖c • @id F v‖ = c * ‖@id F v‖
    rw [norm_smul, Real.norm_of_nonneg hc.le]
  hessian_pos x v w hv hw := by
    simp only [id_eq]
    rw [fderiv_fderiv_norm_sq_apply]
    have := real_inner_self_pos.mpr hw
    positivity

Uses 2 · Used by 1

Statement usesFinsler metric · Second derivative of the squared norm

Used byThe Euclidean Finsler metric is reversible

TheoremThe Euclidean Finsler metric is reversible#✓fully proved

For every finite-dimensional real inner product space \(V\), the Euclidean Finsler metric \(F(x, v) = \|v\|\) on \(V\) is reversible: \(F(x, -v) = F(x, v)\) for all \(x, v \in V\).

theorem euclidean_isReversible : (euclidean : FinslerMetric 𝓘(ℝ, F) F).IsReversible

Uses 2

Statement usesReversible Finsler metric · Euclidean Finsler metric

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.