import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm23

/-- The operator of (2.1): `𝒜u := -(a u')' + b u' + c u`, evaluated classically at `x`. -/
def opA (a b c u : ℝ → ℝ) (x : ℝ) : ℝ :=
  -(deriv (fun y => a y * deriv u y) x) + b x * deriv u x + c x * u x

/-- Classical solution of the two-point boundary value problem (2.1) on `Ω = (0,1)`:
`u ∈ C²(Ω) ∩ C(Ω̄)`, `𝒜u = f` in `Ω`, `u(0) = u₀`, `u(1) = u₁`. -/
def IsSolution21 (a b c f : ℝ → ℝ) (u₀ u₁ : ℝ) (u : ℝ → ℝ) : Prop :=
  ContinuousOn u (Set.Icc 0 1) ∧ ContDiffOn ℝ 2 u (Set.Ioo 0 1) ∧
  (∀ x ∈ Set.Ioo (0 : ℝ) 1, opA a b c u x = f x) ∧ u 0 = u₀ ∧ u 1 = u₁

/-- Green's function of Theorem 2.3:
`G(x,y) = U₀(x)U₁(y)/κ` for `y ≤ x`, `G(x,y) = U₁(x)U₀(y)/κ` for `x ≤ y`. -/
def greenFn (κ : ℝ) (U₀ U₁ : ℝ → ℝ) (x y : ℝ) : ℝ :=
  if y ≤ x then (1 / κ) * U₀ x * U₁ y else (1 / κ) * U₁ x * U₀ y

/-- Theorem 2.3 (Larsson–Thomée). Standing hypotheses: `a, b, c` smooth on `[0,1]` with
(2.2) `a ≥ a₀ > 0`, `c ≥ 0`; here `b = 0`. `U₀, U₁` solve `𝒜U = 0` with
`U₀(0)=1, U₀(1)=0` and `U₁(0)=0, U₁(1)=1`. Then
`κ = a(U₀U₁' - U₀'U₁)` is a positive constant on `Ω` and
`u(x) = ∫₀¹ G(x,y) f(y) dy` solves (2.1) with `u₀ = u₁ = 0`. -/
theorem thm_2_3 (a b c f U₀ U₁ : ℝ → ℝ) (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 : b = fun _ => 0)
    (hf : ContinuousOn f (Set.Icc 0 1))
    (hU₀ : IsSolution21 a b c (fun _ => 0) 1 0 U₀)
    (hU₁ : IsSolution21 a b c (fun _ => 0) 0 1 U₁) :
    ∃ κ : ℝ, 0 < κ ∧
      (∀ x ∈ Set.Ioo (0 : ℝ) 1,
        a x * (U₀ x * deriv U₁ x - deriv U₀ x * U₁ x) = κ) ∧
      IsSolution21 a b c f 0 0
        (fun x => ∫ y in (0 : ℝ)..1, greenFn κ U₀ U₁ x y * f y) := by
  sorry

end PDETextbook.LarssonThomee.Thm23