C² coefficients

The differentiated-equation identity (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2) needs one order of differentiability beyond the interior H² estimate: the coefficient gradient ∂_ℓ aᵢⱼ must itself be treated as a C¹ weight. This file bundles that hypothesis as IsC2Coeff, a mixin on top of EllipticCoeff one derivative order above IsC1Coeff (a mechanical copy of CoeffC1.lean), leaving every existing consumer of EllipticCoeff and IsC1Coeff untouched.

structure EllipticPdes.Regularity.IsC2Coeff {d : ℕ} (A : Sobolev.EllipticCoeff d) : Type

A C² ellipticity bundle: every coefficient entry is twice continuously differentiable with uniform bounds A1 on the first and A2 on the second derivatives. Layered on EllipticCoeff, leaving every existing consumer untouched (as IsC1Coeff is).

• contDiff (i j : Fin d) : ContDiff ℝ 2 fun (x : EuclideanSpace ℝ (Fin d)) => A.a x i j

  Every coefficient entry is twice continuously differentiable.

• A1 : ℝ

  The uniform bound on the first derivatives of every entry.

• A1_nonneg : 0 ≤ self.A1

  A1 is nonnegative.

• grad_bdd (i j : Fin d) (x : EuclideanSpace ℝ (Fin d)) : ‖fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin d)) => A.a y i j) x‖ ≤ self.A1

  The Fréchet derivative of every coefficient entry is bounded by A1 at every point.

• A2 : ℝ

  The uniform bound on the second derivatives of every entry.

• A2_nonneg : 0 ≤ self.A2

  A2 is nonnegative.

• hess_bdd (i j : Fin d) (x : EuclideanSpace ℝ (Fin d)) : ‖fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin d)) => fderiv ℝ (fun (z : EuclideanSpace ℝ (Fin d)) => A.a z i j) y) x‖ ≤ self.A2

  The nested Fréchet derivative (the second derivative, taken as fderiv of fderiv) of every coefficient entry is bounded by A2 at every point.

def EllipticPdes.Regularity.IsC2Coeff.toIsC1Coeff {d : ℕ} {A : Sobolev.EllipticCoeff d} (hA : IsC2Coeff A) : IsC1Coeff A

A C² bundle is in particular a C¹ bundle (drops the second-order data).

Equations

• hA.toIsC1Coeff = { contDiff := ⋯, A1 := hA.A1, A1_nonneg := ⋯, grad_bdd := ⋯ }

theorem EllipticPdes.Regularity.IsC2Coeff.contDiff_partialD_coeff {d : ℕ} {A : Sobolev.EllipticCoeff d} (hA : IsC2Coeff A) (i j ℓ : Fin d) : ContDiff ℝ 1 (Sobolev.partialD ℓ fun (y : EuclideanSpace ℝ (Fin d)) => A.a y i j)

The gradient entry ∂_ℓ a_{ij} is C¹ (needed to treat it as a differentiable weight in the strong-datum move, Task 7).