Compactness of the H1 embedding into L2

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Lem62

/-- `Ω` is a bounded domain (open, connected) in `ℝ^d` with smooth boundary `Γ = ∂Ω`.
Smooth boundary is realized by local smooth defining functions. Near each boundary point `p`
there is an open `U ∋ p` and a `C^∞` function `ψ` on `U` with nonvanishing derivative such that
`Ω ∩ U = {ψ < 0}`. By the implicit function theorem this is equivalent to `Ω` being locally the
region above the graph of a `C^∞` function. -/
def IsBoundedSmoothDomain {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  IsOpen Ω ∧ IsConnected Ω ∧ Bornology.IsBounded Ω ∧
  ∀ p ∈ frontier Ω, ∃ U : Set (Euclidean d), IsOpen U ∧ p ∈ U ∧
    ∃ ψ : Euclidean d → ℝ, ContDiffOn ℝ (⊤ : ℕ∞) ψ U ∧
      (∀ x ∈ U, fderiv ℝ ψ x ≠ 0) ∧
      Ω ∩ U = {x | x ∈ U ∧ ψ x < 0}

/-- `M` is a bounded subset of `H^1(Ω)` (real-valued). Every element lies in `H^1` with a weak
gradient `G`, and `‖u‖_1 = (‖u‖² + ‖∇u‖²)^{1/2} ≤ C` uniformly in `u ∈ M`. -/
def IsBoundedInH1 {d : ℕ} (Ω : Set (Euclidean d)) (M : Set (Euclidean d → ℝ)) : Prop :=
  ∃ C : ℝ, ∀ u ∈ M, ∃ G : Fin d → Euclidean d → ℝ, HasH1Gradient Ω u G ∧
    (∫ x in Ω, ((u x) ^ 2 + ∑ i, (G i x) ^ 2)) ≤ C ^ 2

/-- The image of a set of representatives in `L_2(Ω)`, the a.e. classes of its members. -/
def l2Image {d : ℕ} (Ω : Set (Euclidean d)) (M : Set (Euclidean d → ℝ)) : Set (L2 ℝ Ω) :=
  {f | ∃ u ∈ M, (f : Euclidean d → ℝ) =ᵐ[domainMeasure Ω] u}

/-- Lemma 6.2 (Rellich's lemma). Let `Ω ⊂ ℝ^d` be a bounded domain with smooth boundary
(Chapter 6 setting). A bounded subset `M` of `H^1(Ω)` is pre-compact in `L_2(Ω)`. Pre-compact
means that its closure in `L_2` is compact. -/
theorem rellich_lemma (d : ℕ) (Ω : Set (Euclidean d)) (hΩ : IsBoundedSmoothDomain Ω)
    (M : Set (Euclidean d → ℝ)) (hM : IsBoundedInH1 Ω M) :
    IsCompact (closure (l2Image Ω M)) := by
  sorry

end PDETextbook.LarssonThomee.Lem62