A fundamental-solution convolution construction

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Thm34

/-- The operator `𝒜` of (3.1) with `b = 0`, applied to a smooth function `φ` on `ℝ^d`:
`𝒜φ = -∇·(a∇φ) + cφ`. -/
def opA {d : ℕ} (a c : Euclidean d → ℝ) (φ : Euclidean d → ℝ) (x : Euclidean d) : ℝ :=
  -(∑ i : Fin d, partialDeriv (fun y => a y * partialDeriv φ i y) i x) + c x * φ x

/-- `φ ∈ 𝒞₀^∞(ℝ^d)`: smooth with compact support. -/
def IsTestFunction {d : ℕ} (φ : Euclidean d → ℝ) : Prop :=
  ContDiff ℝ (⊤ : ℕ∞) φ ∧ HasCompactSupport φ

/-- Fundamental solution of (3.12), as defined around (3.14)-(3.15): `U` is smooth for `x ≠ 0`,
`U ∈ L₁(B)` with `B` the open unit ball, `|D^α U(x)| ≤ C_α |x|^{2-d-|α|}` for `|α| ≠ 0`,
and `(U, 𝒜φ) = φ(0)` for all `φ ∈ 𝒞₀^∞(ℝ^d)`. The derivative `D^α` of order `k = |α|`
is written as the `k`-th iterated derivative along coordinate directions `ι : Fin k → Fin d`. -/
def IsFundamentalSolution {d : ℕ} (a c : Euclidean d → ℝ) (U : Euclidean d → ℝ) : Prop :=
  ContDiffOn ℝ (⊤ : ℕ∞) U {x | x ≠ 0} ∧
  IntegrableOn U (Metric.ball (0 : Euclidean d) 1) ∧
  (∀ k : ℕ, 1 ≤ k → ∀ ι : Fin k → Fin d, ∃ C : ℝ, ∀ x : Euclidean d, x ≠ 0 →
      |iteratedFDeriv ℝ k U x (fun j => EuclideanSpace.single (ι j) (1 : ℝ))|
        ≤ C * ‖x‖ ^ ((2 : ℤ) - (d : ℤ) - (k : ℤ))) ∧
  (∀ φ : Euclidean d → ℝ, IsTestFunction φ →
      ∫ x, U x * opA a c φ x = φ 0)

/-- `u` is a solution of (3.12) `𝒜u = f` in `ℝ^d` in the sense of (3.13):
`(u, 𝒜φ) = (f, φ)` for all `φ ∈ 𝒞₀^∞(ℝ^d)` (the integral `(u, 𝒜φ)` being defined). -/
def IsSolution {d : ℕ} (a c : Euclidean d → ℝ) (u f : Euclidean d → ℝ) : Prop :=
  ∀ φ : Euclidean d → ℝ, IsTestFunction φ →
    Integrable (fun x => u x * opA a c φ x) ∧
    ∫ x, u x * opA a c φ x = ∫ x, f x * φ x

/-- Theorem 3.4: if `U` is a fundamental solution of (3.12) and `f ∈ 𝒞₀¹(ℝ^d)`, then
`u = U * f`, `u(x) = ∫ U(x-y) f(y) dy`, is a solution of (3.12). The coefficients `a, c`
are smooth with `a ≥ a₀ > 0`, `c ≥ 0` as in (3.1)-(3.2), and `b = 0`. -/
theorem thm_3_4 {d : ℕ} (a c : Euclidean d → ℝ)
    (ha : ContDiff ℝ (⊤ : ℕ∞) a) (hc : ContDiff ℝ (⊤ : ℕ∞) c)
    (ha0 : ∃ a₀ : ℝ, 0 < a₀ ∧ ∀ x, a₀ ≤ a x) (hc0 : ∀ x, 0 ≤ c x)
    (U f : Euclidean d → ℝ)
    (hU : IsFundamentalSolution a c U)
    (hf : CompactC1 (Set.univ : Set (Euclidean d)) f) :
    IsSolution a c (fun x => ∫ y, U (x - y) * f y) f := by
  sorry

end PDETextbook.LarssonThomee.Thm34