Energy identity for finite-dimensional integral paths

Once the separated weak tests have identified the Fourier coefficient path as an integral path, its finite-dimensional energy balance follows from the Hilbert-space chain rule.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.integral_path_energy_identity {E : Type u_1} [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace ℝ E] {a b : ℝ} {hab : a ≤ b} {u q : ℝ → E} {u₀ : E} (hu : ODE.IsLinearIntegralSolution (fun (x : ℝ) => 0) (fun (t : ℝ) => -q t) u₀ a b u) (hq : IntervalIntegrable q MeasureTheory.volume a b) : ∫ (t : ℝ) in a..b, 2 * inner ℝ (u t) (q t) = ‖u a‖ ^ 2 - ‖u b‖ ^ 2

Energy balance for an integral path forced by an integrable vector field.