Energy conservation for semidiscrete wave finite elements

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Lem13_1

/-- A conforming triangulation of the closure of the polygonal domain `Ω ⊂ ℝ²`.
Each triangle is given by three affinely independent vertices. The triangles cover `closure Ω`.
Two distinct triangles meet only in the convex hull of their common vertices, that is in nothing,
a common vertex or a common edge. -/
structure Triangulation (Ω : Set (Euclidean 2)) where
  tri : Finset (Fin 3 → Euclidean 2)
  affineIndep : ∀ K ∈ tri, AffineIndependent ℝ K
  covers : (⋃ K ∈ tri, convexHull ℝ (Set.range K)) = closure Ω
  conforming : ∀ K ∈ tri, ∀ K' ∈ tri, Set.range K ≠ Set.range K' →
    convexHull ℝ (Set.range K) ∩ convexHull ℝ (Set.range K') =
      convexHull ℝ (Set.range K ∩ Set.range K')

/-- Membership in `S_h ⊂ H₀¹`, the piecewise linear finite element functions on `τ` vanishing on `Γ`.
The representative is extended by zero outside `Ω`. It is continuous, and it is affine on each
closed triangle. -/
def InSh {Ω : Set (Euclidean 2)} (τ : Triangulation Ω) (v : Euclidean 2 → ℝ) : Prop :=
  Continuous v ∧ (∀ x, x ∉ Ω → v x = 0) ∧
  ∀ K ∈ τ.tri, ∃ A : Euclidean 2 →ᵃ[ℝ] ℝ, ∀ x ∈ convexHull ℝ (Set.range K), v x = A x

/-- The L² scalar product `(v, w) = ∫_Ω v w` (real scalars). -/
def l2Ip (Ω : Set (Euclidean 2)) (v w : Euclidean 2 → ℝ) : ℝ :=
  ∫ x in Ω, v x * w x

/-- `‖v‖ = (v, v)^{1/2}`. -/
def l2Nrm (Ω : Set (Euclidean 2)) (v : Euclidean 2 → ℝ) : ℝ :=
  Real.sqrt (l2Ip Ω v v)

/-- `a(v, w) = (∇v, ∇w)`. For continuous piecewise linear functions the classical gradient exists
off the triangle edges, which form a null set, and it equals the weak gradient a.e. -/
def aForm (Ω : Set (Euclidean 2)) (v w : Euclidean 2 → ℝ) : ℝ :=
  ∫ x in Ω, ∑ i : Fin 2, partialDeriv v i x * partialDeriv w i x

/-- The H¹ seminorm `|v|₁ = ‖∇v‖`. -/
def h1Semi (Ω : Set (Euclidean 2)) (v : Euclidean 2 → ℝ) : ℝ :=
  Real.sqrt (aForm Ω v v)

/-- `u` (with time derivatives `ut`, `utt`) is a solution of the semidiscrete problem (13.2):
`(u_{h,tt}, χ) + a(u_h, χ) = (f, χ)` for all `χ ∈ S_h` and `t > 0`, with `u_h(0) = v_h` and
`u_{h,t}(0) = w_h`. Here `u_h(t) ∈ S_h` for `t ≥ 0`, and `u_h` is twice differentiable in `t`
on `[0, ∞)`. -/
def IsSolution_13_2 {Ω : Set (Euclidean 2)} (τ : Triangulation Ω)
    (f : ℝ → Euclidean 2 → ℝ) (v_h w_h : Euclidean 2 → ℝ)
    (u ut utt : ℝ → Euclidean 2 → ℝ) : Prop :=
  (∀ t : ℝ, 0 ≤ t → InSh τ (u t)) ∧
  (∀ t : ℝ, 0 ≤ t → ∀ x, HasDerivWithinAt (fun s => u s x) (ut t x) (Set.Ici 0) t) ∧
  (∀ t : ℝ, 0 ≤ t → ∀ x, HasDerivWithinAt (fun s => ut s x) (utt t x) (Set.Ici 0) t) ∧
  (∀ t : ℝ, 0 < t → ∀ χ, InSh τ χ →
    l2Ip Ω (utt t) χ + aForm Ω (u t) χ = l2Ip Ω (f t) χ) ∧
  u 0 = v_h ∧ ut 0 = w_h

/-- Lemma 13.1 (energy conservation for the semidiscrete wave equation, `f = 0`). -/
theorem lem_13_1 (Ω : Set (Euclidean 2)) (hΩopen : IsOpen Ω) (hΩconn : IsConnected Ω)
    (hΩbdd : Bornology.IsBounded Ω) (hΩconv : Convex ℝ Ω)
    (τ : Triangulation Ω) (v_h w_h : Euclidean 2 → ℝ)
    (hv : InSh τ v_h) (hw : InSh τ w_h)
    (u ut utt : ℝ → Euclidean 2 → ℝ)
    (hsol : IsSolution_13_2 τ (fun _ _ => 0) v_h w_h u ut utt) :
    ∀ t : ℝ, 0 ≤ t →
      l2Nrm Ω (ut t) ^ 2 + h1Semi Ω (u t) ^ 2 = l2Nrm Ω w_h ^ 2 + h1Semi Ω v_h ^ 2 := by
  sorry

end PDETextbook.LarssonThomee.Lem13_1