Boundary trace from H1 to L2

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.ThmA4

/-- Smooth boundary, given by a local defining function. Near every boundary point `x` there is
an open neighbourhood `U` and a C^∞ function `ρ` with nonvanishing gradient on `U` such that
`Ω ∩ U = {ρ < 0} ∩ U`. -/
def HasSmoothBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  ∀ x ∈ frontier Ω, ∃ U : Set (Euclidean d), IsOpen U ∧ x ∈ U ∧
    ∃ ρ : Euclidean d → ℝ, (∀ n : ℕ, ContDiff ℝ n ρ) ∧
      (∀ y ∈ U, fderiv ℝ ρ y ≠ 0) ∧
      Ω ∩ U = {y | y ∈ U ∧ ρ y < 0}

/-- Polygonal (polyhedral) domain: `Ω` is the interior of a finite union of closed
nondegenerate `d`-simplices, so its boundary is piecewise flat. -/
def IsPolygonalDomain {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  ∃ (n : ℕ) (S : Fin n → Affine.Simplex ℝ (Euclidean d) d),
    Ω = interior (⋃ i, convexHull ℝ (Set.range (S i).points))

/-- Surface measure on `Γ = ∂Ω`: the `(d-1)`-dimensional Hausdorff measure restricted to `Γ`.
Mathlib's Hausdorff measure is unnormalized, so it is a fixed positive multiple of surface
measure. -/
abbrev boundaryMeasure {d : ℕ} (Ω : Set (Euclidean d)) : Measure (Euclidean d) :=
  (MeasureTheory.Measure.hausdorffMeasure ((d : ℝ) - 1)).restrict (frontier Ω)

/-- `L₂(Γ)`. -/
abbrev L2Boundary (𝕜 : Type*) [RCLike 𝕜] {d : ℕ} (Ω : Set (Euclidean d)) :=
  MeasureTheory.Lp 𝕜 2 (boundaryMeasure Ω)

/-- `𝒞¹(Ω̄)`. The function is `C¹` in `Ω`, it is continuous on `Ω̄`, and each first partial
derivative extends continuously to `Ω̄`. -/
def C1Bar {𝕜 : Type*} [RCLike 𝕜] {d : ℕ} (Ω : Set (Euclidean d))
    (v : Euclidean d → 𝕜) : Prop :=
  ContDiffOn ℝ 1 v Ω ∧ ContinuousOn v (closure Ω) ∧
    ∀ i : Fin d, ∃ g : Euclidean d → 𝕜, ContinuousOn g (closure Ω) ∧
      ∀ x ∈ Ω, partialDeriv v i x = g x

/-- The `H¹` norm `‖v‖₁ = (‖v‖² + ∑ᵢ ‖∂ᵢ v‖²)^{1/2}`, where `G` is the weak gradient of `v`. -/
def h1Norm {𝕜 : Type*} [RCLike 𝕜] {d : ℕ} (Ω : Set (Euclidean d))
    (v : Euclidean d → 𝕜) (G : Fin d → Euclidean d → 𝕜) : ℝ :=
  Real.sqrt ((eLpNorm v 2 (domainMeasure Ω)).toReal ^ 2 +
    ∑ i, (eLpNorm (G i) 2 (domainMeasure Ω)).toReal ^ 2)

/-- Theorem A.4 (Trace theorem). Let `Ω` be a bounded domain in `ℝ^d` with `d ≥ 2` and with
smooth or polygonal boundary `Γ`. The trace `γ v = v|_Γ` on `𝒞¹(Ω̄)` extends to a linear map
`γ : H¹(Ω) → L₂(Γ)`. There is also a constant `C = C(Ω)` such that
`‖γ v‖_{L₂(Γ)} ≤ C ‖v‖₁` for all `v ∈ H¹(Ω)`. -/
theorem trace_theorem {𝕜 : Type*} [RCLike 𝕜] {d : ℕ} (hd : 2 ≤ d)
    (Ω : Set (Euclidean d)) (hΩopen : IsOpen Ω) (hΩconn : IsConnected Ω)
    (hΩbdd : Bornology.IsBounded Ω)
    (hΓ : HasSmoothBoundary Ω ∨ IsPolygonalDomain Ω) :
    ∃ γ : (Euclidean d → 𝕜) → L2Boundary 𝕜 Ω, ∃ C : ℝ,
      -- γ is linear on H¹(Ω)
      (∀ v w : Euclidean d → 𝕜, InH1 Ω v → InH1 Ω w → ∀ a b : 𝕜,
        γ (a • v + b • w) = a • γ v + b • γ w) ∧
      -- γ extends the classical trace v ↦ v|_Γ on 𝒞¹(Ω̄)
      (∀ v : Euclidean d → 𝕜, C1Bar Ω v → ⇑(γ v) =ᵐ[boundaryMeasure Ω] v) ∧
      -- (A.26)
      (∀ (v : Euclidean d → 𝕜) (G : Fin d → Euclidean d → 𝕜), HasH1Gradient Ω v G →
        ‖γ v‖ ≤ C * h1Norm Ω v G) := by
  sorry

end PDETextbook.LarssonThomee.ThmA4