discreteEnergy

formal source

  87-/
  88
  89/-- Discrete kinetic energy: \(E(u)=\frac12 \|u\|^2\). -/
  90noncomputable def discreteEnergy {N : ℕ} (u : GalerkinState N) : ℝ :=
  91  (1 / 2 : ℝ) * ‖u‖ ^ 2
  92
  93/-- Algebraic hypothesis capturing the skew-symmetry of the Galerkin nonlinearity in L²:
  94\( \langle B(u,u), u \rangle = 0 \). -/
  95structure EnergySkewHypothesis {N : ℕ} (B : ConvectionOp N) : Prop where
  96  skew : ∀ u : GalerkinState N, ⟪B u u, u⟫_ℝ = 0
  97
  98/-- Energy conservation for the inviscid Galerkin system (ν = 0), stated at a point.
  99
 100If `u` solves `u' = -B(u,u)` and the nonlinearity is energy-skew, then the derivative of the
 101discrete energy is zero.
 102-/
 103theorem inviscid_energy_deriv_zero {N : ℕ} (B : ConvectionOp N) (HB : EnergySkewHypothesis B)
 104    (u : ℝ → GalerkinState N) {t : ℝ}
 105    (hu : HasDerivAt u (-(B (u t) (u t))) t) :
 106    HasDerivAt (fun s => discreteEnergy (u s)) 0 t := by
 107  -- Use the chain rule for `‖u‖^2` in an inner product space.
 108  -- d/dt (1/2 * ‖u‖^2) = ⟪u', u⟫.
 109  have h_normsq :
 110      HasDerivAt (fun s => ‖u s‖ ^ 2) (2 * ⟪u t, -(B (u t) (u t))⟫_ℝ) t := by
 111    -- `HasDerivAt.norm_sq` gives: derivative of `‖u‖^2` is `2 * ⟪u, u'⟫`.
 112    simpa using (HasDerivAt.norm_sq hu)
 113  have h_energy : HasDerivAt (fun s => discreteEnergy (u s))
 114      ((1 / 2 : ℝ) * (2 * ⟪u t, -(B (u t) (u t))⟫_ℝ)) t := by
 115    -- Multiply the norm-square derivative by 1/2
 116    simpa [discreteEnergy, mul_assoc] using h_normsq.const_mul (1 / 2 : ℝ)
 117  -- Now simplify using skew-symmetry: ⟪-B(u,u), u⟫ = -⟪B(u,u),u⟫ = 0
 118  have h_inner_zero : ⟪u t, -(B (u t) (u t))⟫_ℝ = 0 := by
 119    calc
 120      ⟪u t, -(B (u t) (u t))⟫_ℝ = -⟪u t, B (u t) (u t)⟫_ℝ := by simp