def Geodesics.IsGeodesic {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) : Prop

theorem Geodesics.deriv_mem_tangentSpace {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))} {ψ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (hsmooth : ContDiff ℝ ⊤ γ) (hM : ∀ (t : ℝ), γ t ∈ M) {t : ℝ} (hψ : Hypersurface.IsLocalDefiningFunction ψ M (γ t)) : deriv γ t ∈ Hypersurface.tangentSpace ψ (γ t)

theorem Geodesics.geodesic_constant_speed {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hHyp : Hypersurface.IsHypersurface M) (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (hγ : IsGeodesic M hHyp γ) : ∃ (c : ℝ), ∀ (t : ℝ), ‖deriv γ t‖ = c

noncomputable def Geodesics.energy {n : ℕ} (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) : ℝ

structure Geodesics.SmoothVariation {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) : Type

• Γ : ℝ → ℝ → EuclideanSpace ℝ (Fin (n + 1))
• smooth : ContDiff ℝ ⊤ fun (p : ℝ × ℝ) => self.Γ p.1 p.2
• base (t : ℝ) : self.Γ 0 t = γ t
• left_fixed (s : ℝ) : self.Γ s a = γ a
• right_fixed (s : ℝ) : self.Γ s b = γ b
• maps_to (s t : ℝ) : self.Γ s t ∈ M

noncomputable def Geodesics.firstVariationEnergy {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))} {a b : ℝ} (V : SmoothVariation M γ a b) : ℝ

noncomputable def Geodesics.variationField {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))} {a b : ℝ} (V : SmoothVariation M γ a b) (t : ℝ) : EuclideanSpace ℝ (Fin (n + 1))

theorem Geodesics.variationField_mem_tangentSpace {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))} {a b : ℝ} (V : SmoothVariation M γ a b) {ψ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {t : ℝ} (hψ : Hypersurface.IsLocalDefiningFunction ψ M (γ t)) : variationField V t ∈ Hypersurface.tangentSpace ψ (γ t)

theorem Geodesics.first_variation_formula {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))} {a b : ℝ} (V : SmoothVariation M γ a b) (hγ_smooth : ContDiff ℝ ⊤ γ) : firstVariationEnergy V = -2 * ∫ (t : ℝ) in a..b, inner ℝ (deriv (deriv γ) t) (variationField V t)

theorem Geodesics.critical_energy_implies_geodesic {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) (hab : a < b) (hγ_smooth : ContDiff ℝ ⊤ γ) (hγ_in : ∀ (t : ℝ), γ t ∈ M) (hcrit : ∀ (V : SmoothVariation M γ a b), firstVariationEnergy V = 0) : IsGeodesic M hM γ

theorem Geodesics.geodesic_iff_critical_energy {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) (hab : a < b) (hγ_smooth : ContDiff ℝ ⊤ γ) (hγ_in : ∀ (t : ℝ), γ t ∈ M) : IsGeodesic M hM γ ↔ ∀ (V : SmoothVariation M γ a b), firstVariationEnergy V = 0

def Geodesics.IsEnergyMinimizer {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) : Prop

theorem Geodesics.energy_differentiableAt_variation {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))} {a b : ℝ} (V : SmoothVariation M γ a b) : DifferentiableAt ℝ (fun (s : ℝ) => energy (V.Γ s) a b) 0

theorem Geodesics.geodesic_of_energy_minimizer {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) (hab : a < b) (hγ_smooth : ContDiff ℝ ⊤ γ) (hγ_in : ∀ (t : ℝ), γ t ∈ M) (hmin : IsEnergyMinimizer M γ a b) : IsGeodesic M hM γ

def Geodesics.IsGeodesicOn {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (I : Set ℝ) : Prop

theorem Geodesics.geodesic_local_agreement {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {hM : Hypersurface.IsHypersurface M} {γ γ' : ℝ → EuclideanSpace ℝ (Fin (n + 1))} (hγ : IsGeodesic M hM γ) (hγ' : IsGeodesic M hM γ') (t₀ : ℝ) (h_pos : γ t₀ = γ' t₀) (h_vel : deriv γ t₀ = deriv γ' t₀) : ∀ᶠ (t : ℝ) in nhds t₀, γ t = γ' t ∧ deriv γ t = deriv γ' t

theorem Geodesics.geodesic_uniqueness {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (γ γ' : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (hγ : IsGeodesic M hM γ) (hγ' : IsGeodesic M hM γ') (h_pos : γ 0 = γ' 0) (h_vel : deriv γ 0 = deriv γ' 0) (t : ℝ) : γ t = γ' t

theorem Geodesics.geodesic_existence {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (y : EuclideanSpace ℝ (Fin (n + 1))) (hy : y ∈ M) (ψ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ) (hψ : Hypersurface.IsLocalDefiningFunction ψ M y) (Y : EuclideanSpace ℝ (Fin (n + 1))) (hY : Y ∈ Hypersurface.tangentSpace ψ y) : ∃ (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))), IsGeodesic M hM γ ∧ γ 0 = y ∧ deriv γ 0 = Y

theorem Geodesics.path_length_eq_distance_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [StrictConvexSpace ℝ E] (γ : ℝ → E) (a b : ℝ) (hab : a < b) (hγ : ContDiff ℝ ⊤ γ) : ∫ (t : ℝ) in a..b, ‖deriv γ t‖ = ‖γ b - γ a‖ ↔ ∀ t ∈ Set.Icc a b, ∃ (c : ℝ), 0 ≤ c ∧ deriv γ t = c • (γ b - γ a)

def Geodesics.SatisfiesGeodesicEquation {n : ℕ} (patch : HypersurfacePatch n) (c : ℝ → Fin n → ℝ) : Prop

theorem Geodesics.patch_partialDeriv_mem_tangentSpace {n : ℕ} (patch : HypersurfacePatch n) (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hpatch_in_M : ∀ x ∈ patch.domain, (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x) ∈ M) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (ψ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ) (hψ : Hypersurface.IsLocalDefiningFunction ψ M ((WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x))) (s : Fin n) : (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.partialDeriv x s) ∈ Hypersurface.tangentSpace ψ ((WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x))

theorem Geodesics.metric_christoffel_identity {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (i j s : Fin n) : ∑ k : Fin n, firstFundamentalForm patch x s k * ChristoffelSymbols.christoffelSymbol patch x i j k = ChristoffelSymbols.secondPartialDeriv patch x i j ⬝ᵥ patch.partialDeriv x s

theorem Geodesics.second_deriv_inner_product_eq {n : ℕ} (patch : HypersurfacePatch n) (c : ℝ → Fin n → ℝ) (hc_smooth : ContDiff ℝ ⊤ c) (hc_domain : ∀ (t : ℝ), c t ∈ patch.domain) (t : ℝ) (s : Fin n) : inner ℝ (deriv (deriv fun (t : ℝ) => (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f (c t))) t) ((WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.partialDeriv (c t) s)) = ∑ i : Fin n, ∑ j : Fin n, ChristoffelSymbols.secondPartialDeriv patch (c t) i j ⬝ᵥ patch.partialDeriv (c t) s * deriv c t i * deriv c t j + ∑ k : Fin n, patch.partialDeriv (c t) k ⬝ᵥ patch.partialDeriv (c t) s * deriv (deriv c) t k

theorem Geodesics.geodesic_inner_product_formula {n : ℕ} (patch : HypersurfacePatch n) (c : ℝ → Fin n → ℝ) (hc_smooth : ContDiff ℝ ⊤ c) (hc_domain : ∀ (t : ℝ), c t ∈ patch.domain) (t : ℝ) (s : Fin n) : inner ℝ (deriv (deriv fun (t : ℝ) => (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f (c t))) t) ((WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.partialDeriv (c t) s)) = ∑ k : Fin n, firstFundamentalForm patch (c t) s k * (deriv (deriv c) t k + ∑ i : Fin n, ∑ j : Fin n, ChristoffelSymbols.christoffelSymbol patch (c t) i j k * deriv c t i * deriv c t j)

theorem Geodesics.firstFundamentalForm_mulVec_injective {n : ℕ} (patch : HypersurfacePatch n) (x : Fin n → ℝ) (hx : x ∈ patch.domain) : Function.Injective (firstFundamentalForm patch x).mulVec

theorem Geodesics.patch_comp_smooth {n : ℕ} (patch : HypersurfacePatch n) (c : ℝ → Fin n → ℝ) (hc_smooth : ContDiff ℝ ⊤ c) (hc_domain : ∀ (t : ℝ), c t ∈ patch.domain) : ContDiff ℝ ⊤ fun (t : ℝ) => (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f (c t))

theorem Geodesics.tangentSpace_mem_span_partialDerivs {n : ℕ} (patch : HypersurfacePatch n) (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (hpatch_in_M : ∀ x ∈ patch.domain, (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x) ∈ M) (x : Fin n → ℝ) (hx : x ∈ patch.domain) (ψ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ) (hψ : Hypersurface.IsLocalDefiningFunction ψ M ((WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x))) (v : EuclideanSpace ℝ (Fin (n + 1))) (hv : v ∈ Hypersurface.tangentSpace ψ ((WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x))) : ∃ (a : Fin n → ℝ), v = ∑ s : Fin n, a s • (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.partialDeriv x s)

theorem Geodesics.geodesic_ortho_from_ode {n : ℕ} (patch : HypersurfacePatch n) (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (c : ℝ → Fin n → ℝ) (hc_smooth : ContDiff ℝ ⊤ c) (hc_domain : ∀ (t : ℝ), c t ∈ patch.domain) (hpatch_in_M : ∀ x ∈ patch.domain, (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x) ∈ M) (hode : ∀ (t : ℝ) (k : Fin n), deriv (deriv c) t k + ∑ i : Fin n, ∑ j : Fin n, ChristoffelSymbols.christoffelSymbol patch (c t) i j k * deriv c t i * deriv c t j = 0) (t : ℝ) (ψ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ) (hψ : Hypersurface.IsLocalDefiningFunction ψ M ((WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f (c t)))) (v : EuclideanSpace ℝ (Fin (n + 1))) (hv : v ∈ Hypersurface.tangentSpace ψ ((WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f (c t)))) : inner ℝ (deriv (deriv fun (t : ℝ) => (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f (c t))) t) v = 0

theorem Geodesics.geodesic_equation_coordinates {n : ℕ} (patch : HypersurfacePatch n) (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (c : ℝ → Fin n → ℝ) (hc_smooth : ContDiff ℝ ⊤ c) (hc_domain : ∀ (t : ℝ), c t ∈ patch.domain) (hpatch_in_M : ∀ x ∈ patch.domain, (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x) ∈ M) : (IsGeodesic M hM fun (t : ℝ) => (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f (c t))) ↔ SatisfiesGeodesicEquation patch c

structure Geodesics.SmoothPathIn {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (p q : EuclideanSpace ℝ (Fin (n + 1))) : Type

• toFun : ℝ → EuclideanSpace ℝ (Fin (n + 1))
• smooth (m : ℕ∞) : ContDiff ℝ (↑m) self.toFun
• source : self.toFun 0 = p
• target : self.toFun 1 = q
• maps_to (t : ℝ) : self.toFun t ∈ M

noncomputable def Geodesics.pathLength {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) : ℝ

def Geodesics.reversePath {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) : SmoothPathIn M q p

theorem Geodesics.pathLength_reverse {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) : pathLength (reversePath γ) = pathLength γ

noncomputable def Geodesics.geodesicDist {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (p q : EuclideanSpace ℝ (Fin (n + 1))) : ℝ

def Geodesics.IsSmoothOnHypersurface {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : Set E) (f : ↑M → ℝ) : Prop

structure Geodesics.ConnectedHypersurface (n : ℕ) : Type

• carrier : Set (EuclideanSpace ℝ (Fin (n + 1)))
• isHypersurface : Hypersurface.IsHypersurface self.carrier
• connected (φ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ) : (∀ y ∈ self.carrier, ContDiffAt ℝ ⊤ φ y) → (∀ y ∈ self.carrier, ∀ (ψ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ), Hypersurface.IsLocalDefiningFunction ψ self.carrier y → ∀ v ∈ Hypersurface.tangentSpace ψ y, (fderiv ℝ φ y) v = 0) → ∀ y₁ ∈ self.carrier, ∀ y₂ ∈ self.carrier, φ y₁ = φ y₂

structure Geodesics.ConnectedHypersurfaceWithPaths (n : ℕ) extends Geodesics.ConnectedHypersurface n : Type

• carrier : Set (EuclideanSpace ℝ (Fin (n + 1)))
• isHypersurface : Hypersurface.IsHypersurface self.carrier
• connected (φ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ) : (∀ y ∈ self.carrier, ContDiffAt ℝ ⊤ φ y) → (∀ y ∈ self.carrier, ∀ (ψ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ), Hypersurface.IsLocalDefiningFunction ψ self.carrier y → ∀ v ∈ Hypersurface.tangentSpace ψ y, (fderiv ℝ φ y) v = 0) → ∀ y₁ ∈ self.carrier, ∀ y₂ ∈ self.carrier, φ y₁ = φ y₂
• pathConnected (p q : EuclideanSpace ℝ (Fin (n + 1))) : p ∈ self.carrier → q ∈ self.carrier → Nonempty (SmoothPathIn self.carrier p q)

theorem Geodesics.compact_connected_hypersurface_orientable {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (hconn : IsConnected M) (hcpt : IsCompact M) : Hypersurface.IsOrientable M

theorem Geodesics.smooth_concat_exists_path {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) {p q r : EuclideanSpace ℝ (Fin (n + 1))} (α : SmoothPathIn M p q) (β : SmoothPathIn M q r) : ∃ (δ : SmoothPathIn M p r), pathLength δ ≤ pathLength α + pathLength β

theorem Geodesics.geodesicDist_self {n : ℕ} (M : ConnectedHypersurfaceWithPaths n) (p : EuclideanSpace ℝ (Fin (n + 1))) (hp : p ∈ M.carrier) : geodesicDist M.carrier p p = 0

theorem Geodesics.geodesicDist_comm {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (p q : EuclideanSpace ℝ (Fin (n + 1))) : geodesicDist M p q = geodesicDist M q p

theorem Geodesics.geodesicDist_triangle {n : ℕ} (M : ConnectedHypersurfaceWithPaths n) (p q r : EuclideanSpace ℝ (Fin (n + 1))) (hp : p ∈ M.carrier) (hq : q ∈ M.carrier) (hr : r ∈ M.carrier) : geodesicDist M.carrier p r ≤ geodesicDist M.carrier p q + geodesicDist M.carrier q r

theorem Geodesics.geodesicDist_eq_zero_iff {n : ℕ} (M : ConnectedHypersurfaceWithPaths n) (p q : EuclideanSpace ℝ (Fin (n + 1))) (hp : p ∈ M.carrier) (hq : q ∈ M.carrier) (heq : geodesicDist M.carrier p q = 0) : p = q

theorem Geodesics.geodesicDist_metric {n : ℕ} (M : ConnectedHypersurfaceWithPaths n) (p q r : EuclideanSpace ℝ (Fin (n + 1))) (hp : p ∈ M.carrier) (hq : q ∈ M.carrier) (hr : r ∈ M.carrier) : geodesicDist M.carrier p p = 0 ∧ geodesicDist M.carrier p q = geodesicDist M.carrier q p ∧ geodesicDist M.carrier p r ≤ geodesicDist M.carrier p q + geodesicDist M.carrier q r ∧ (geodesicDist M.carrier p q = 0 → p = q)

theorem Geodesics.cauchy_schwarz_integral (f : ℝ → ℝ) (hf : Continuous f) (a b : ℝ) (hab : a < b) : ∫ (t : ℝ) in a..b, f t ≤ √(b - a) * √(∫ (t : ℝ) in a..b, f t ^ 2) ∧ (∫ (t : ℝ) in a..b, f t = √(b - a) * √(∫ (t : ℝ) in a..b, f t ^ 2) ↔ ∃ (c : ℝ), ∀ t ∈ Set.Icc a b, f t = c)

theorem Geodesics.cauchy_schwarz_integral_eq_iff (f : ℝ → ℝ) (hf : Continuous f) (hf_nn : ∀ (t : ℝ), 0 ≤ f t) (a b : ℝ) (hab : a < b) : ∫ (t : ℝ) in a..b, f t = √(b - a) * √(∫ (t : ℝ) in a..b, f t ^ 2) ↔ ∃ (c : ℝ), ∀ t ∈ Set.Icc a b, f t = c

noncomputable def Geodesics.lengthAB {n : ℕ} (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) : ℝ

theorem Geodesics.energy_ge_length_sq_div {n : ℕ} (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) (hab : a < b) (hγ : ContDiff ℝ ⊤ γ) : energy γ a b ≥ lengthAB γ a b ^ 2 / (b - a) ∧ (energy γ a b = lengthAB γ a b ^ 2 / (b - a) ↔ ∃ (c : ℝ), ∀ t ∈ Set.Icc a b, ‖deriv γ t‖ = c)

noncomputable def Geodesics.pathEnergy {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) : ℝ

def Geodesics.IsConstantSpeed {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) : Prop

def Geodesics.IsAbsoluteLengthMinimizer {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) : Prop

def Geodesics.IsAbsoluteEnergyMinimizer {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) : Prop

theorem Geodesics.energy_ge_length_sq {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) : pathLength γ ^ 2 ≤ pathEnergy γ

theorem Geodesics.energy_eq_length_sq_iff_constant_speed {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) : pathEnergy γ = pathLength γ ^ 2 ↔ IsConstantSpeed γ

theorem Geodesics.exists_constant_speed_reparametrization {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (σ : SmoothPathIn M p q) : ∃ (σ' : SmoothPathIn M p q), IsConstantSpeed σ' ∧ pathLength σ' = pathLength σ

theorem Geodesics.energy_minimizer_of_length_minimizer_constant_speed {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) (hlen : IsAbsoluteLengthMinimizer γ) (hcs : IsConstantSpeed γ) : IsAbsoluteEnergyMinimizer γ

theorem Geodesics.length_minimizer_constant_speed_of_energy_minimizer {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) (hmin : IsAbsoluteEnergyMinimizer γ) : IsAbsoluteLengthMinimizer γ ∧ IsConstantSpeed γ

theorem Geodesics.energy_minimizer_iff_length_minimizer_constant_speed {n : ℕ} {M : Set (EuclideanSpace ℝ (Fin (n + 1)))} {p q : EuclideanSpace ℝ (Fin (n + 1))} (γ : SmoothPathIn M p q) : IsAbsoluteEnergyMinimizer γ ↔ IsAbsoluteLengthMinimizer γ ∧ IsConstantSpeed γ

def Geodesics.IsMetricGeodesic {X : Type u_1} [MetricSpace X] (γ : ℝ → X) (a b : ℝ) : Prop

def Geodesics.IsGlobalMetricGeodesic {X : Type u_1} [MetricSpace X] (γ : ℝ → X) : Prop

structure Geodesics.CompactPositiveGaussCurvature (n : ℕ) : Type

• carrier : Set (EuclideanSpace ℝ (Fin (n + 1)))
• isHypersurface : Hypersurface.IsHypersurface self.carrier
• isCompact : IsCompact self.carrier
• isConnected : IsConnected self.carrier
• gaussCurvaturePos (patch : HypersurfacePatch n) (x : Fin n → ℝ) : x ∈ patch.domain → (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x) ∈ self.carrier → 0 < gaussCurvature patch x

theorem Geodesics.gauss_map_injective_of_positive_curvature {n : ℕ} (M : CompactPositiveGaussCurvature n) (hn : 2 ≤ n) (ν : EuclideanSpace ℝ (Fin (n + 1)) → EuclideanSpace ℝ (Fin (n + 1))) (hν_maps : ∀ y ∈ M.carrier, ν y ∈ GaussMap.unitSphere n) (hν_smooth : ContDiffOn ℝ ⊤ ν M.carrier) (hν_gauss_map : ∀ (patch : HypersurfacePatch n), ∀ x ∈ patch.domain, (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x) ∈ M.carrier → ν ((WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x)) = (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (gaussNormal patch x)) (y : EuclideanSpace ℝ (Fin (n + 1))) : y ∈ M.carrier → ∀ (ψ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ), Hypersurface.IsLocalDefiningFunction ψ M.carrier y → ∀ v ∈ Hypersurface.tangentSpace ψ y, (fderiv ℝ ν y) v = 0 → v = 0

theorem Geodesics.convex_of_bijective_gauss_map {n : ℕ} (M : CompactPositiveGaussCurvature n) (hn : 2 ≤ n) (ν : EuclideanSpace ℝ (Fin (n + 1)) → EuclideanSpace ℝ (Fin (n + 1))) (hν_maps : ∀ y ∈ M.carrier, ν y ∈ GaussMap.unitSphere n) (hν_bij : Function.Bijective fun (y : ↑M.carrier) => ⟨ν ↑y, ⋯⟩) : Hypersurface.IsConvexHypersurface M.carrier

theorem Geodesics.hadamard_convexity {n : ℕ} (M : CompactPositiveGaussCurvature n) (hn : 2 ≤ n) (ν : EuclideanSpace ℝ (Fin (n + 1)) → EuclideanSpace ℝ (Fin (n + 1))) (hν_maps : ∀ y ∈ M.carrier, ν y ∈ GaussMap.unitSphere n) (hν_smooth : ContDiffOn ℝ ⊤ ν M.carrier) (hν_gauss_map : ∀ (patch : HypersurfacePatch n), ∀ x ∈ patch.domain, (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x) ∈ M.carrier → ν ((WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (patch.f x)) = (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm (gaussNormal patch x)) : Hypersurface.IsConvexHypersurface M.carrier

def Geodesics.IsRiemannianGeodesicallyComplete {n : ℕ} (M : ConnectedHypersurface n) : Prop

def Geodesics.IsMetricallyComplete {n : ℕ} (M : ConnectedHypersurface n) : Prop

def Geodesics.IsMinimizingGeodesic {n : ℕ} (M : ConnectedHypersurface n) (p q : EuclideanSpace ℝ (Fin (n + 1))) (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) : Prop

theorem Geodesics.hopf_rinow_minimizing_geodesic {n : ℕ} (M : ConnectedHypersurface n) (hM : IsClosed M.carrier) (p q : EuclideanSpace ℝ (Fin (n + 1))) (hp : p ∈ M.carrier) (hq : q ∈ M.carrier) (a b : ℝ) (hab : a < b) : ∃ (γ : ℝ → EuclideanSpace ℝ (Fin (n + 1))), IsMinimizingGeodesic M p q γ a b

def Geodesics.IsGeodesicSpace (X : Type u_1) [MetricSpace X] : Prop

def Geodesics.IsCATZeroSpace (X : Type u_1) [MetricSpace X] : Prop

class Geodesics.IsBusemannSpace (X : Type u_1) [MetricSpace X] : Prop

• isGeodesicSpace : IsGeodesicSpace X
• busemann_inequality (l : ℝ) (hl : 0 < l) (γ₁ γ₂ : ℝ → X) (hγ₁ : IsMetricGeodesic γ₁ 0 l) (hγ₂ : IsMetricGeodesic γ₂ 0 l) (h_start : γ₁ 0 = γ₂ 0) (t : ℝ) (ht : t ∈ Set.Icc 0 l) : dist (γ₁ t) (γ₂ t) ≤ t / l * dist (γ₁ l) (γ₂ l)

theorem Geodesics.busemann_unique_geodesic {X : Type u_1} [MetricSpace X] [IsBusemannSpace X] (p q : X) : (∃ (γ : ℝ → X), IsMetricGeodesic γ 0 (dist p q) ∧ γ 0 = p ∧ γ (dist p q) = q) ∧ ∀ (γ₁ γ₂ : ℝ → X), IsMetricGeodesic γ₁ 0 (dist p q) → γ₁ 0 = p → γ₁ (dist p q) = q → IsMetricGeodesic γ₂ 0 (dist p q) → γ₂ 0 = p → γ₂ (dist p q) = q → ∀ t ∈ Set.Icc 0 (dist p q), γ₁ t = γ₂ t

theorem Geodesics.cauchy_schwarz_energy_length {n : ℕ} (σ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) (hab : a < b) (hσ : ContDiff ℝ ⊤ σ) : (∫ (t : ℝ) in a..b, ‖deriv σ t‖) ^ 2 ≤ (b - a) * ∫ (t : ℝ) in a..b, ‖deriv σ t‖ ^ 2

theorem Geodesics.geodesic_locally_minimizes_length {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (γ σ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) (hab : a < b) (hγ_geo : IsGeodesic M hM γ) (hγ_unit : ∀ (t : ℝ), ‖deriv γ t‖ = 1) (hσ : ContDiff ℝ ⊤ σ) (hσ_in : ∀ (t : ℝ), σ t ∈ M) (hendpoints : σ a = γ a ∧ σ b = γ b) : ∫ (t : ℝ) in a..b, ‖deriv σ t‖ ≥ b - a

theorem Geodesics.geodesic_arclength_minimizes_energy_locally {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM : Hypersurface.IsHypersurface M) (γ σ : ℝ → EuclideanSpace ℝ (Fin (n + 1))) (a b : ℝ) (hab : a < b) (hγ_geo : IsGeodesic M hM γ) (hγ_unit : ∀ (t : ℝ), ‖deriv γ t‖ = 1) (hσ : ContDiff ℝ ⊤ σ) (hσ_in : ∀ (t : ℝ), σ t ∈ M) (hendpoints : σ a = γ a ∧ σ b = γ b) : energy σ a b ≥ energy γ a b