Physlib.ClassicalMechanics.EulerLagrange

Imports

/-
Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
module

public import Physlib.Mathematics.VariationalCalculus.HasVarGradient
public import Physlib.SpaceAndTime.Time.Derivatives

A. Euler–Lagrange equations

The Euler–Lagrange equations characterize stationary trajectories of an action functional. For a Lagrangian L t q v, they compare the gradient with respect to position to the time derivative of the gradient with respect to velocity.

A.1. Mathematical setting

Trajectories take values in a complete real inner-product space X. The Lagrangian has type Time → X → X → ℝ, and the corresponding action is the time integral of L t (q t) (∂ₜ q t).

A.2. Main definitions and results

eulerLagrangeOp defines the Euler–Lagrange operator ∂L/∂q - ∂ₜ (∂L/∂v) along a trajectory.

eulerLagrangeOp_eq exposes its pointwise formula.

eulerLagrangeOp_zero evaluates the operator for the zero Lagrangian.

euler_lagrange_varGradient proves that the variational gradient of the action equals the Euler–Lagrange operator for smooth trajectories and Lagrangians.

A.3. Current scope

The result is formulated for smooth data and Hilbert-space-valued trajectories. Applications to specific mechanical systems are developed in their corresponding modules, where vanishing of the operator becomes the system's equation of motion.

              @[expose] public sectionlemma eulerLagrangeOp_eq (L : Time → X → X → ℝ) (q : Time → X) :
    eulerLagrangeOp L q = fun t => gradient (L t · (∂ₜ q t)) (q t)
    - ∂ₜ (fun t' => gradient (L t' (q t') ·) (∂ₜ q t')) t := byX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → X⊢ eulerLagrangeOp L q = fun t =>
  gradient (fun x => L t x (∂ₜ q t)) (q t) - ∂ₜ (fun t' => gradient (fun x => L t' (q t') x) (∂ₜ q t')) t rflAll goals completed! 🐙lemma eulerLagrangeOp_zero (q : Time → X) :
    eulerLagrangeOp (fun _ _ _ => 0) q = fun _ => 0 := byX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace Xq:Time → X⊢ eulerLagrangeOp (fun x x_1 x_2 => 0) q = fun x => 0
  simp [eulerLagrangeOp_eq, Time.deriv_eq]All goals completed! 🐙

/- The variational derivative of `L t (q' t) (deriv q' t))` for a lagrangian `L`
  is equal to the `eulerLagrangeOp`. -/
theorem euler_lagrange_varGradient
    (L : Time → X → X → ℝ) (q : Time → X)
    (hq : ContDiff ℝ ∞ q) (hL : ContDiff ℝ ∞ ↿L) :
    (δ (q':=q), ∫ t, L t (q' t) (fderiv ℝ q' t 1)) = eulerLagrangeOp L q := byX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ varGradient (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) q = eulerLagrangeOp L q
  simp only [eulerLagrangeOp_eq, Time.deriv_eq]X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ varGradient (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) q = fun t =>
  gradient (fun x => L t x ((fderiv ℝ q t) 1)) (q t) -
    (fderiv ℝ (fun t' => gradient (fun x => L t' (q t') x) ((fderiv ℝ q t') 1)) t) 1
  apply HasVarGradientAt.varGradientX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1))
  (fun t =>
    gradient (fun x => L t x ((fderiv ℝ q t) 1)) (q t) -
      (fderiv ℝ (fun t' => gradient (fun x => L t' (q t') x) ((fderiv ℝ q t') 1)) t) 1)
  q
  apply HasVarGradientAt.intro _hF'X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarAdjDerivAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) ?m.83 qhgradX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ (fun t =>
    gradient (fun x => L t x ((fderiv ℝ q t) 1)) (q t) -
      (fderiv ℝ (fun t' => gradient (fun x => L t' (q t') x) ((fderiv ℝ q t') 1)) t) 1) =
  ?m.83 fun x => 1X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ (Time → ℝ) → Time → X
  ·hF'X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarAdjDerivAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) ?m.83 q apply HasVarAdjDerivAt.comp
      (F := fun (φ : Time → X × X) t => L t (φ t).fst (φ t).snd)
      (G := fun (φ : Time → X) t => (φ t, fderiv ℝ φ t 1))hF'.hFX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarAdjDerivAt (fun φ t => L t (φ t).1 (φ t).2) ?m.131 fun t => (q t, (fderiv ℝ q t) 1)hF'.hGX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarAdjDerivAt (fun φ t => (φ t, (fderiv ℝ φ t) 1)) ?m.132 qX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ (Time → ℝ) → Time → X × XX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ (Time → X × X) → Time → X
    ·hF'.hFX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarAdjDerivAt (fun φ t => L t (φ t).1 (φ t).2) ?m.131 fun t => (q t, (fderiv ℝ q t) 1) apply HasVarAdjDerivAt.fmap (f := fun t => ↿(L t))hF'.hF.huX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ ContDiff ℝ ∞ fun t => (q t, (fderiv ℝ q t) 1)hF'.hF.hf'X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ ContDiff ℝ ∞ ↿fun t => ↿(L t)hF'.hF.hfX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ ∀ (x : Time) (u : X × X), HasAdjFDerivAt ℝ (↿(L x)) (?m.154 x u) uX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ Time → X × X → ℝ → X × X
      ·hF'.hF.huX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ ContDiff ℝ ∞ fun t => (q t, (fderiv ℝ q t) 1) fun_propAll goals completed! 🐙
      ·hF'.hF.hf'X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ ContDiff ℝ ∞ ↿fun t => ↿(L t) fun_propAll goals completed! 🐙
      intro x uhF'.hF.hfX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lx:Timeu:X × X⊢ HasAdjFDerivAt ℝ (↿(L x)) (?m.154 x u) uX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ Time → X × X → ℝ → X × X
      apply DifferentiableAt.hasAdjFDerivAthF'.hF.hfX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lx:Timeu:X × X⊢ DifferentiableAt ℝ (↿(L x)) u
      apply ContDiff.differentiable (n := ∞) (byX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lx:Timeu:X × X⊢ ContDiff ℝ ∞ ↿(L x) fun_propAll goals completed! 🐙) (byX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lx:Timeu:X × X⊢ ∞ ≠ 0 simpAll goals completed! 🐙)
    ·hF'.hGX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarAdjDerivAt (fun φ t => (φ t, (fderiv ℝ φ t) 1)) ?m.132 q apply HasVarAdjDerivAt.prod (F:=fun φ => φ)hF'.hG.hFX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarAdjDerivAt (fun φ => φ) ?m.340 qhF'.hG.hGX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarAdjDerivAt (fun φ x => (fderiv ℝ φ x) 1) ?m.341 qX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ (Time → X) → Time → XX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ (Time → X) → Time → X
      ·hF'.hG.hFX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarAdjDerivAt (fun φ => φ) ?m.340 q apply HasVarAdjDerivAt.id _ hqAll goals completed! 🐙
      ·hF'.hG.hGX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ HasVarAdjDerivAt (fun φ x => (fderiv ℝ φ x) 1) ?m.341 q apply HasVarAdjDerivAt.fderiv (hu := hq)All goals completed! 🐙
  case hgrad =>X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿L⊢ (fun t =>
    gradient (fun x => L t x ((fderiv ℝ q t) 1)) (q t) -
      (fderiv ℝ (fun t' => gradient (fun x => L t' (q t') x) ((fderiv ℝ q t') 1)) t) 1) =
  fun x =>
  (fun x' => ((fun x => adjFDeriv ℝ ↿(L x) (q x, (fderiv ℝ q x) 1) ((fun x => 1) x)) x').1) x +
    -(fderiv ℝ (fun x' => ((fun x => adjFDeriv ℝ ↿(L x) (q x, (fderiv ℝ q x) 1) ((fun x => 1) x)) x').2) x) 1
    funext tX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ gradient (fun x => L t x ((fderiv ℝ q t) 1)) (q t) -
    (fderiv ℝ (fun t' => gradient (fun x => L t' (q t') x) ((fderiv ℝ q t') 1)) t) 1 =
  (fun x' => ((fun x => adjFDeriv ℝ ↿(L x) (q x, (fderiv ℝ q x) 1) ((fun x => 1) x)) x').1) t +
    -(fderiv ℝ (fun x' => ((fun x => adjFDeriv ℝ ↿(L x) (q x, (fderiv ℝ q x) 1) ((fun x => 1) x)) x').2) t) 1
    simp (disch := fun_prop) [sub_eq_add_neg]X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ gradient (fun x => L t x ((fderiv ℝ q t) 1)) (q t) +
    -(fderiv ℝ (fun t' => gradient (fun x => L t' (q t') x) ((fderiv ℝ q t') 1)) t) 1 =
  (adjFDeriv ℝ ↿(L t) (q t, (fderiv ℝ q t) 1) 1).1 +
    -(fderiv ℝ (fun x' => (adjFDeriv ℝ ↿(L x') (q x', (fderiv ℝ q x') 1) 1).2) t) 1
    congre_aX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ gradient (fun x => L t x ((fderiv ℝ q t) 1)) (q t) = (adjFDeriv ℝ ↿(L t) (q t, (fderiv ℝ q t) 1) 1).1e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ (fun t' => gradient (fun x => L t' (q t') x) ((fderiv ℝ q t') 1)) = fun x' =>
  (adjFDeriv ℝ ↿(L x') (q x', (fderiv ℝ q x') 1) 1).2
    all_goals
      try funext te_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ gradient (fun x => L t (q t) x) ((fderiv ℝ q t) 1) = (adjFDeriv ℝ ↿(L t) (q t, (fderiv ℝ q t) 1) 1).2
      rw [gradient_eq_adjFDeriv,e_aX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ adjFDeriv ℝ (fun x => L t x ((fderiv ℝ q t) 1)) (q t) 1 = (adjFDeriv ℝ ↿(L t) (q t, (fderiv ℝ q t) 1) 1).1e_aX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ DifferentiableAt ℝ (fun x => L t x ((fderiv ℝ q t) 1)) (q t)e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ DifferentiableAt ℝ ↿(L t) (q t, (fderiv ℝ q t) 1)e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ DifferentiableAt ℝ (fun x => L t (q t) x) ((fderiv ℝ q t) 1) adjFDeriv_uncurrye_aX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ adjFDeriv ℝ (fun x => L t x ((fderiv ℝ q t) 1)) (q t) 1 =
  ((fun dz =>
        (adjFDeriv ℝ (fun x => L t x (q t, (fderiv ℝ q t) 1).2) (q t, (fderiv ℝ q t) 1).1 dz,
          adjFDeriv ℝ (fun x => L t (q t, (fderiv ℝ q t) 1).1 x) (q t, (fderiv ℝ q t) 1).2 dz))
      1).1e_aX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ DifferentiableAt ℝ ↿(L t) (q t, (fderiv ℝ q t) 1)e_aX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ DifferentiableAt ℝ (fun x => L t x ((fderiv ℝ q t) 1)) (q t)e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ DifferentiableAt ℝ ↿(L t) (q t, (fderiv ℝ q t) 1)e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ DifferentiableAt ℝ (fun x => L t (q t) x) ((fderiv ℝ q t) 1)]e_aX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ DifferentiableAt ℝ ↿(L t) (q t, (fderiv ℝ q t) 1)e_aX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt:Time⊢ DifferentiableAt ℝ (fun x => L t x ((fderiv ℝ q t) 1)) (q t)e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ DifferentiableAt ℝ ↿(L t) (q t, (fderiv ℝ q t) 1)e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ DifferentiableAt ℝ (fun x => L t (q t) x) ((fderiv ℝ q t) 1)e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ DifferentiableAt ℝ ↿(L t) (q t, (fderiv ℝ q t) 1)e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ DifferentiableAt ℝ (fun x => L t (q t) x) ((fderiv ℝ q t) 1) <;>e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ DifferentiableAt ℝ ↿(L t) (q t, (fderiv ℝ q t) 1)e_a.e_fX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ DifferentiableAt ℝ (fun x => L t (q t) x) ((fderiv ℝ q t) 1)
        apply ContDiff.differentiable (n := ∞) (byX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ ContDiff ℝ ∞ fun x => L t (q t) x fun_propAll goals completed! 🐙) (byX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qhL:ContDiff ℝ ∞ ↿Lt✝:Timet:Time⊢ ∞ ≠ 0 simpAll goals completed! 🐙)