Lagrangian

noncomputable def EulerLagrangian.momentumResidual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (u : ℝ × E → E) (p : ℝ × E → ℝ) (z : ℝ × E) : E

The unforced Euler momentum residual, with space-time derivative and the canonical real gradient.

Equations

• EulerLagrangian.momentumResidual u p z = (fderiv ℝ u z) (1, u z) + gradient (fun (x : E) => p (z.1, x)) z.2

theorem EulerLagrangian.material_derivative {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (w : ℝ × E → E) (X : ℝ → E) (t : ℝ) (U : E) (D : ℝ × E →L[ℝ] E) (hX : HasDerivAt X U t) (hw : HasFDerivAt w D (t, X t)) : HasDerivAt (fun (s : ℝ) => w (s, X s)) (D (1, U)) t

theorem EulerLagrangian.gradient_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f g : E → ℝ) (x : E) (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : gradient (fun (y : E) => f y + g y) x = gradient f x + gradient g x

theorem EulerLagrangian.momentum_perturbation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (u w : ℝ × E → E) (p q : ℝ × E → ℝ) (z : ℝ × E) (Du Dw : ℝ × E →L[ℝ] E) (hu : HasFDerivAt u Du z) (hw : HasFDerivAt w Dw z) (hp : DifferentiableAt ℝ (fun (x : E) => p (z.1, x)) z.2) (hq : DifferentiableAt ℝ (fun (x : E) => q (z.1, x)) z.2) : momentumResidual (fun (y : ℝ × E) => u y + w y) (fun (y : ℝ × E) => p y + q y) z = momentumResidual u p z + Dw (1, u z) + Du (0, w z) + Dw (0, w z) + gradient (fun (x : E) => q (z.1, x)) z.2

theorem EulerLagrangian.euler_perturbation_along_flow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (u w : ℝ × E → E) (p q : ℝ × E → ℝ) (X : ℝ → E) (t : ℝ) (Du Dw : ℝ × E →L[ℝ] E) (V : E) (hX : HasDerivAt X (u (t, X t)) t) (hu : HasFDerivAt u Du (t, X t)) (hw : HasFDerivAt w Dw (t, X t)) (hW : HasDerivAt (fun (s : ℝ) => w (s, X s)) V t) (hp : DifferentiableAt ℝ (fun (x : E) => p (t, x)) (X t)) (hq : DifferentiableAt ℝ (fun (x : E) => q (t, x)) (X t)) (hparent : momentumResidual u p (t, X t) = 0) : momentumResidual (fun (y : ℝ × E) => u y + w y) (fun (y : ℝ × E) => p y + q y) (t, X t) = V + Du (0, w (t, X t)) + Dw (0, w (t, X t)) + gradient (fun (x : E) => q (t, x)) (X t)

theorem EulerLagrangian.deformation_acceleration {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (F M H : ℝ → E →L[ℝ] E) (t : ℝ) (hF : HasDerivAt F (M t ∘SL F t) t) (hM : HasDerivAt M (-M t ∘SL M t - H t) t) : HasDerivAt (fun (s : ℝ) => M s ∘SL F s) (-H t ∘SL F t) t

theorem EulerLagrangian.derivative_pullback_inverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f X : E → E) (F : E ≃L[ℝ] E) (x : E) (hX : HasFDerivAt X (↑F) x) (hf : DifferentiableAt ℝ f (X x)) : fderiv ℝ f (X x) = fderiv ℝ (f ∘ X) x ∘SL ↑F.symm

theorem EulerLagrangian.gradient_pullback {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (X : E → E) (F : E →L[ℝ] E) (x : E) (hX : HasFDerivAt X F x) (hf : DifferentiableAt ℝ f (X x)) : gradient (f ∘ X) x = (ContinuousLinearMap.adjoint F) (gradient f (X x))

theorem EulerLagrangian.gradient_pullback_inverse {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (X : E → E) (F : E ≃L[ℝ] E) (x : E) (hX : HasFDerivAt X (↑F) x) (hf : DifferentiableAt ℝ f (X x)) : gradient f (X x) = (ContinuousLinearMap.adjoint ↑F.symm) (gradient (f ∘ X) x)