Poincaré inequality for zero-boundary functions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.ThmA6

/-- A bounded domain in `ℝ^d`: a nonempty, open, connected and bounded subset. -/
def IsBoundedDomain {d : ℕ} (Ω : Set (Euclidean d)) : Prop :=
  IsOpen Ω ∧ IsConnected Ω ∧ Bornology.IsBounded Ω

/-- The L² norm `‖v‖ = (∫_Ω v²)^{1/2}` of a representative on `Ω`. -/
def l2Norm {d : ℕ} (Ω : Set (Euclidean d)) (v : Euclidean d → ℝ) : ℝ :=
  (eLpNorm v 2 (domainMeasure Ω)).toReal

/-- `‖∇v‖ = (∫_Ω |∇v|²)^{1/2} = (∑ᵢ ‖∂ᵢ v‖²)^{1/2}`, where `G` is the weak gradient of `v`. -/
def gradL2Norm {d : ℕ} (Ω : Set (Euclidean d)) (G : Fin d → Euclidean d → ℝ) : ℝ :=
  Real.sqrt (∑ i, (l2Norm Ω (G i)) ^ 2)

/-- Theorem A.6 (Poincaré's inequality). If `Ω` is a bounded domain in `ℝ^d`, there is a
constant `C = C(Ω)` such that `‖v‖ ≤ C ‖∇v‖` for all `v ∈ H₀¹(Ω)`.
`ℝ^d` is read with positive dimension `d ≥ 1`, the convention for Euclidean space in the book.
At `d = 0` the gradient is empty and the statement would be meaningless.
`H₀¹(Ω)` is realized by the closure formulation `InH10Closure`.
`∇v` is any weak gradient `G` of `v` with L² components; weak gradients are a.e. unique on open `Ω`.
The constant is chosen after `Ω` and before `v`. Functions are real-valued, as in Appendix A. -/
theorem poincare_inequality {d : ℕ} (hd : 0 < d) (Ω : Set (Euclidean d))
    (hΩ : IsBoundedDomain Ω) :
    ∃ C : ℝ, ∀ (v : Euclidean d → ℝ) (G : Fin d → Euclidean d → ℝ),
      InH10Closure Ω v → HasH1Gradient Ω v G →
        l2Norm Ω v ≤ C * gradL2Norm Ω G := by
  sorry

end PDETextbook.LarssonThomee.ThmA6