import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomeeLemA1

/-- The closed interval `Ω̄ = [0,1]` for `Ω = (0,1)`. -/
abbrev OmegaBar : Set ℝ := Set.Icc (0 : ℝ) 1

/-- The open interval `Ω = (0,1)`. -/
abbrev Omega : Set ℝ := Set.Ioo (0 : ℝ) 1

/-- The textbook's `H¹(Ω)` norm `‖v‖₁ = (‖v‖² + ‖v'‖²)^{1/2}`, with `L²(Ω)` norms
over `Ω = (0,1)` (book, Sect. A.2 and (2.18)). It is used here for `v ∈ C¹(Ω̄)`.
`v'` is the derivative of `v` within `Ω̄`, which agrees with the ordinary derivative
at interior points. -/
def h1Norm (v : ℝ → ℝ) : ℝ :=
  Real.sqrt ((∫ x in Omega, v x ^ 2) + ∫ x in Omega, (derivWithin v OmegaBar x) ^ 2)

/-- Lemma A.1 (Larsson–Thomée). Let `Ω = (0,1)`. Then there is a constant `C` such that
`|v(x)| ≤ C ‖v‖₁` for all `x ∈ Ω̄` and all `v ∈ C¹(Ω̄)`. -/
theorem lemma_A1 :
    ∃ C : ℝ, ∀ x ∈ OmegaBar, ∀ v : ℝ → ℝ, ContDiffOn ℝ 1 v OmegaBar →
      |v x| ≤ C * h1Norm v := by
  sorry

end PDETextbook.LarssonThomeeLemA1