Eigenfunction solution of the Dirichlet wave equation

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm11_1

open PDETextbook

/-- The Dirichlet eigensystem of `-Δ` recalled in (8.11), in its weak form
`a(φ_j, ψ) = λ_j (φ_j, ψ)` for all `ψ ∈ H¹₀`, with `φ_j ∈ H¹₀`. The `φ_j` are
representatives of an orthonormal basis `b` of `L₂(Ω)`. The recalled properties of the
eigenvalues are `0 < λ₁ < λ₂ ≤ ⋯` and `λ_j → ∞`. Index `j` here is `j+1` in the book. -/
def IsDirichletEigenbasis {d : ℕ} (Ω : Set (Euclidean d))
    (φ : ℕ → Euclidean d → ℝ) (lam : ℕ → ℝ) (b : HilbertBasis ℕ ℝ (L2 ℝ Ω)) : Prop :=
  (∀ j, ((b j : L2 ℝ Ω) : Euclidean d → ℝ) =ᵐ[domainMeasure Ω] φ j) ∧
  (∀ j, InH10Closure Ω (φ j)) ∧
  (∀ j, ∃ Gφ : Fin d → Euclidean d → ℝ, HasH1Gradient Ω (φ j) Gφ ∧
     ∀ (ψ : Euclidean d → ℝ) (Gψ : Fin d → Euclidean d → ℝ),
       InH10Closure Ω ψ → HasH1Gradient Ω ψ Gψ →
       (∫ x in Ω, ∑ i, Gφ i x * Gψ i x) = lam j * ∫ x in Ω, φ j x * ψ x) ∧
  (0 < lam 0) ∧ (lam 0 < lam 1) ∧ Monotone lam ∧
  Filter.Tendsto lam Filter.atTop Filter.atTop

/-- Fourier coefficient `\hat f_j = (f, φ_j)`. -/
def coeff {d : ℕ} (Ω : Set (Euclidean d)) (φ : ℕ → Euclidean d → ℝ)
    (f : Euclidean d → ℝ) (j : ℕ) : ℝ :=
  ∫ x in Ω, f x * φ j x

/-- The `j`-th term of the series (11.6) at time `t`, as an element of `L₂(Ω)`:
`(v̂_j cos(√λ_j t) + ŵ_j λ_j^{-1/2} sin(√λ_j t)) φ_j`. -/
def seriesTerm {d : ℕ} (Ω : Set (Euclidean d)) (φ : ℕ → Euclidean d → ℝ)
    (lam : ℕ → ℝ) (b : HilbertBasis ℕ ℝ (L2 ℝ Ω)) (v w : Euclidean d → ℝ)
    (t : ℝ) (j : ℕ) : L2 ℝ Ω :=
  (coeff Ω φ v j * Real.cos (Real.sqrt (lam j) * t) +
    coeff Ω φ w j * (Real.sqrt (lam j))⁻¹ * Real.sin (Real.sqrt (lam j) * t)) • b j

/-- `f = Δu` in the weak sense: `u ∈ H¹` with gradient `G`, each `G i` has weak
partial `H i` in direction `i`, and `f = Σ_i H i` a.e. on `Ω`. -/
def HasWeakLaplacian {d : ℕ} (Ω : Set (Euclidean d)) (u f : Euclidean d → ℝ) : Prop :=
  ∃ G H : Fin d → Euclidean d → ℝ,
    HasH1Gradient Ω u G ∧ (∀ i, HasWeakPartial Ω (G i) i (H i)) ∧
    f =ᵐ[domainMeasure Ω] fun x => ∑ i, H i x

/-- Solution of (11.5) in the `L₂`-valued sense. `U` is twice differentiable in time
as an `L₂`-valued map on `[0,∞)`. For `t > 0`, `U(t) ∈ H¹₀` (the boundary condition
`u = 0` on `Γ`) and `u_tt = Δu` with a weak Laplacian, i.e. `u_tt - Δu = 0`.
The initial conditions are `U(0) = v` and `U_t(0) = w`. No `H²` regularity of `U(t)`
is required, because (11.5) does not demand it. -/
def IsSolution_11_5 {d : ℕ} (Ω : Set (Euclidean d)) (v w : Euclidean d → ℝ)
    (U : ℝ → L2 ℝ Ω) : Prop :=
  ∃ U' U'' : ℝ → L2 ℝ Ω,
    (∀ t, 0 ≤ t → HasDerivWithinAt U (U' t) (Set.Ici 0) t ∧
      HasDerivWithinAt U' (U'' t) (Set.Ici 0) t) ∧
    (∀ t, 0 < t →
      InH10Closure Ω ((U t : L2 ℝ Ω) : Euclidean d → ℝ) ∧
      HasWeakLaplacian Ω ((U t : L2 ℝ Ω) : Euclidean d → ℝ)
        ((U'' t : L2 ℝ Ω) : Euclidean d → ℝ)) ∧
    (((U 0 : L2 ℝ Ω) : Euclidean d → ℝ) =ᵐ[domainMeasure Ω] v) ∧
    (((U' 0 : L2 ℝ Ω) : Euclidean d → ℝ) =ᵐ[domainMeasure Ω] w)

/-- Theorem 11.1 (Larsson–Thomée). Let `Ω` be a bounded domain in `ℝ^d`.
Let `{φ_j, λ_j}` be the Dirichlet eigensystem of `-Δ`.
If `v ∈ H² ∩ H¹₀` and `w ∈ H¹₀`, then the series (11.6) converges in `L₂` for every
`t ≥ 0` and its sum is a solution of (11.5). -/
theorem thm_11_1 {d : ℕ} (Ω : Set (Euclidean d))
    (hΩopen : IsOpen Ω) (hΩconn : IsConnected Ω) (hΩbdd : Bornology.IsBounded Ω)
    (φ : ℕ → Euclidean d → ℝ) (lam : ℕ → ℝ) (b : HilbertBasis ℕ ℝ (L2 ℝ Ω))
    (hb : IsDirichletEigenbasis Ω φ lam b)
    (v w : Euclidean d → ℝ)
    (hv2 : InH2 Ω v) (hv0 : InH10Closure Ω v) (hw0 : InH10Closure Ω w) :
    (∀ t : ℝ, 0 ≤ t → Summable (seriesTerm Ω φ lam b v w t)) ∧
    IsSolution_11_5 Ω v w (fun t => ∑' j, seriesTerm Ω φ lam b v w t j) := by
  sorry

end PDETextbook.LarssonThomee.Thm11_1