Weak Dirichlet solvability on a bounded domain

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm36

/-- Divergence `∇·b` of a vector field, computed via classical partial derivatives
(used only for the smooth coefficient `b`). -/
def divergence {d : ℕ} (b : Euclidean d → Euclidean d) (x : Euclidean d) : ℝ :=
  ∑ i : Fin d, partialDeriv (fun y => b y i) i x

/-- Hypothesis (3.21): `a(x) ≥ a₀ > 0` and `c(x) - ½ ∇·b(x) ≥ 0` for `x ∈ Ω`. -/
def Coercivity321 {d : ℕ} (Ω : Set (Euclidean d)) (a : Euclidean d → ℝ)
    (b : Euclidean d → Euclidean d) (c : Euclidean d → ℝ) : Prop :=
  ∃ a₀ : ℝ, 0 < a₀ ∧ ∀ x ∈ Ω, a₀ ≤ a x ∧ 0 ≤ c x - (1 / 2 : ℝ) * divergence b x

/-- `Γ = ∂Ω` is smooth: near every boundary point `p`, `Ω` is the sublevel set `{ρ < 0}` of a
`C^∞` defining function `ρ` whose differential at `p` is nonzero (standard local-defining-function
characterization of a `C^∞` boundary). -/
def SmoothBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  ∀ p ∈ frontier Ω, ∃ U ∈ nhds p, ∃ ρ : Euclidean d → ℝ,
    ContDiff ℝ (⊤ : ℕ∞) ρ ∧ fderiv ℝ ρ p ≠ 0 ∧ Ω ∩ U = {x | ρ x < 0} ∩ U

/-- `Γ = ∂Ω` is a polygon (`d = 2`) / polyhedron (`d = 3`): it is a finite union of
nondegenerate `(d-1)`-simplices (segments if `d = 2`, triangles if `d = 3`), and `Ω` lies on
one side of its boundary in the sense that `Ω` is regular open (`Ω = int(Ω̄)`, excluding slits). -/
def PolyhedralBoundary {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  (∃ (n : ℕ) (P : Fin n → Fin d → Euclidean d),
      (∀ k, AffineIndependent ℝ (P k)) ∧
      frontier Ω = ⋃ k, convexHull ℝ (Set.range (P k))) ∧
    interior (closure Ω) = Ω

/-- Standing boundary assumption of the book: `Γ` is either smooth, or a polygon (if `d = 2`)
or polyhedron (if `d = 3`). -/
def BoundaryRegular {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  SmoothBoundary Ω ∨ ((d = 2 ∨ d = 3) ∧ PolyhedralBoundary Ω)

/-- Weak (variational) solution of (3.20): `u ∈ H₀¹` satisfying (3.23)
`∫_Ω (a ∇u·∇v + b·∇u v + c u v) dx = ∫_Ω f v dx` for all `v ∈ H₀¹`.
`H₀¹` is realized by the closure formulation `InH10Closure`; gradients are weak gradients.
On the book's domains (bounded, smooth or polygonal/polyhedral boundary, as assumed in
`thm_3_6`) the source's trace-kernel `H₀¹` has `C₀¹` as a dense subspace (source, before (3.23)),
which is the identification used here. -/
def IsWeakSolution {d : ℕ} (Ω : Set (Euclidean d)) (a : Euclidean d → ℝ)
    (b : Euclidean d → Euclidean d) (c : Euclidean d → ℝ)
    (f u : Euclidean d → ℝ) : Prop :=
  InH10Closure Ω u ∧
  ∃ G : Fin d → Euclidean d → ℝ, HasH1Gradient Ω u G ∧
    ∀ (v : Euclidean d → ℝ) (H : Fin d → Euclidean d → ℝ),
      InH10Closure Ω v → HasH1Gradient Ω v H →
      (∫ x in Ω, (a x * (∑ i : Fin d, G i x * H i x)
          + (∑ i : Fin d, b x i * G i x) * v x + c x * u x * v x))
        = ∫ x in Ω, f x * v x

/-- The seminorm `|v|₁ = (∫_Ω |∇v|² dx)^{1/2}` (A.22, k = 1), given a weak gradient `G` of `v`. -/
def h1Seminorm {d : ℕ} (Ω : Set (Euclidean d)) (G : Fin d → Euclidean d → ℝ) : ℝ :=
  Real.sqrt (∫ x in Ω, ∑ i : Fin d, (G i x) ^ 2)

/-- The `L₂(Ω)` norm `‖v‖ = (∫_Ω v² dx)^{1/2}`. -/
def l2Norm {d : ℕ} (Ω : Set (Euclidean d)) (v : Euclidean d → ℝ) : ℝ :=
  Real.sqrt (∫ x in Ω, (v x) ^ 2)

/-- Theorem 3.6 (Larsson–Thomée). Ω is a bounded domain (open, connected, bounded) in
`ℝ^d`, `d ∈ {1,2,3}`, whose boundary `Γ` is smooth or a polygon (`d = 2`) / polyhedron (`d = 3`)
(the book's standing assumption). The coefficients `a, b, c` are smooth on `Ω̄` and satisfy (3.21).
Then for every `f ∈ L₂` there is a weak solution `u ∈ H₀¹` of (3.20) (i.e. satisfying (3.23)),
unique as an element of `H₀¹` (a.e. on Ω), and there is a constant `C` independent of `f`
with `|u|₁ ≤ C ‖f‖`. -/
theorem thm_3_6 {d : ℕ} (hd : d = 1 ∨ d = 2 ∨ d = 3)
    (Ω : Set (Euclidean d)) (hΩo : IsOpen Ω) (hΩc : IsConnected Ω)
    (hΩb : Bornology.IsBounded Ω) (hΓ : BoundaryRegular Ω)
    (a : Euclidean d → ℝ) (b : Euclidean d → Euclidean d) (c : Euclidean d → ℝ)
    (ha : ContDiffOn ℝ (⊤ : ℕ∞) a (closure Ω))
    (hb : ContDiffOn ℝ (⊤ : ℕ∞) b (closure Ω))
    (hc : ContDiffOn ℝ (⊤ : ℕ∞) c (closure Ω))
    (h321 : Coercivity321 Ω a b c) :
    (∀ f : Euclidean d → ℝ, InL2 Ω f →
      ∃ u : Euclidean d → ℝ, IsWeakSolution Ω a b c f u ∧
        ∀ u' : Euclidean d → ℝ, IsWeakSolution Ω a b c f u' →
          u' =ᵐ[domainMeasure Ω] u) ∧
    (∃ C : ℝ, ∀ (f u : Euclidean d → ℝ) (G : Fin d → Euclidean d → ℝ),
      InL2 Ω f → IsWeakSolution Ω a b c f u → HasH1Gradient Ω u G →
        h1Seminorm Ω G ≤ C * l2Norm Ω f) := by
  sorry

end PDETextbook.LarssonThomee.Thm36