import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm25

/-- The interval `Ω = (0,1)`, realized as a subset of the one-dimensional Euclidean space. -/
def Ω01 : Set (Euclidean 1) := {x | x 0 ∈ Set.Ioo (0 : ℝ) 1}

/-- The bilinear form `a(v,w) = ∫_0^1 (a v' w' + b v' w + c v w) dx` of the variational
formulation (2.16) of problem (2.11). Here `v'` and `w'` are the weak derivatives. -/
def bilin (a b c : ℝ → ℝ) (v v' w w' : Euclidean 1 → ℝ) : ℝ :=
  ∫ x in Ω01, (a (x 0) * v' x * w' x + b (x 0) * v' x * w x + c (x 0) * v x * w x)

/-- The linear functional `L(w) = (f,w) = ∫_0^1 f w dx` of (2.16). -/
def loadL (f w : Euclidean 1 → ℝ) : ℝ :=
  ∫ x in Ω01, f x * w x

/-- The energy functional
`F(φ) = ½ ∫_0^1 (a (φ')² + c φ²) dx - ∫_0^1 f φ dx`.
Here `φ'` is the weak derivative of `φ`. -/
def energyF (a c : ℝ → ℝ) (f φ φ' : Euclidean 1 → ℝ) : ℝ :=
  (1 / 2 : ℝ) * (∫ x in Ω01, (a (x 0) * (φ' x) ^ 2 + c (x 0) * (φ x) ^ 2))
    - ∫ x in Ω01, f x * φ x

/-- Theorem 2.5 (Larsson–Thomée).

Assumptions:
* (2.2) holds and `b = 0`.
* The coefficients are smooth, which is the standing assumption of Sect. 2.3.
* `f ∈ L₂`.
* `u ∈ H₀¹` solves (2.16), that is, `a(u,φ) = L(φ)` for all `φ ∈ H₀¹`.

Conclusion: `F(u) ≤ F(φ)` for every `φ ∈ H₀¹`, and equality holds only for `φ = u`.
Equality is understood in `H₀¹`, that is, almost everywhere on `Ω`. -/
theorem energy_minimization
    (a b c : ℝ → ℝ) (a₀ : ℝ)
    (ha_smooth : ContDiffOn ℝ (⊤ : ℕ∞) a (Set.Icc 0 1))
    (hb_smooth : ContDiffOn ℝ (⊤ : ℕ∞) b (Set.Icc 0 1))
    (hc_smooth : ContDiffOn ℝ (⊤ : ℕ∞) c (Set.Icc 0 1))
    (ha₀ : 0 < a₀)
    (ha : ∀ x ∈ Set.Icc (0 : ℝ) 1, a₀ ≤ a x)
    (hc : ∀ x ∈ Set.Icc (0 : ℝ) 1, 0 ≤ c x)
    (hb : ∀ x ∈ Set.Icc (0 : ℝ) 1, b x = 0)
    (f : Euclidean 1 → ℝ) (hf : InL2 Ω01 f)
    (u : Euclidean 1 → ℝ) (Gu : Fin 1 → Euclidean 1 → ℝ)
    (hu : InH10Closure Ω01 u) (hGu : HasH1Gradient Ω01 u Gu)
    (hsol : ∀ (φ : Euclidean 1 → ℝ) (Gφ : Fin 1 → Euclidean 1 → ℝ),
      InH10Closure Ω01 φ → HasH1Gradient Ω01 φ Gφ →
        bilin a b c u (Gu 0) φ (Gφ 0) = loadL f φ) :
    (∀ (φ : Euclidean 1 → ℝ) (Gφ : Fin 1 → Euclidean 1 → ℝ),
      InH10Closure Ω01 φ → HasH1Gradient Ω01 φ Gφ →
        energyF a c f u (Gu 0) ≤ energyF a c f φ (Gφ 0)) ∧
    (∀ (φ : Euclidean 1 → ℝ) (Gφ : Fin 1 → Euclidean 1 → ℝ),
      InH10Closure Ω01 φ → HasH1Gradient Ω01 φ Gφ →
        energyF a c f φ (Gφ 0) = energyF a c f u (Gu 0) →
          φ =ᵐ[domainMeasure Ω01] u) := by
  sorry

end PDETextbook.LarssonThomee.Thm25