C¹ coefficients and the coefficient difference-quotient bound

The interior H² estimate (Evans, Partial Differential Equations (2nd ed.), §6.3.1; Gilbarg–Trudinger, Elliptic Partial Differential Equations of Second Order, Thm 8.8) needs the manuscript hypothesis aᵢⱼ ∈ C¹ only through one quantitative consequence: the difference quotient of each coefficient entry is uniformly bounded by the sup of its gradient. This file bundles that hypothesis as an added structure IsC1Coeff (a mixin on top of EllipticCoeff, leaving every existing consumer of EllipticCoeff untouched) and proves the coefficient difference-quotient bound abs_diffQuot_coeff_le by the segment mean-value inequality.

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

A C¹ ellipticity bundle: the coefficient matrix is continuously differentiable with a global bound A₁ on the first derivatives of every entry. Faithful to aᵢⱼ ∈ C¹ for the interior estimate, where only a ∈ C¹(closure W) with W ⋐ Ω bounded matters, so A₁ < ∞.

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

  Every coefficient entry is 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.

theorem EllipticPdes.Regularity.IsC1Coeff.abs_diffQuot_coeff_le {d : ℕ} {A : Sobolev.EllipticCoeff d} (hA : IsC1Coeff A) (i j k : Fin d) {h : ℝ} (hh : h ≠ 0) (x : EuclideanSpace ℝ (Fin d)) : |(A.a (x + hshift k h) i j - A.a x i j) / h| ≤ hA.A1

The coefficient difference quotient is uniformly bounded: for the (i, j) coefficient entry, |Dₖʰ aᵢⱼ(x)| ≤ A₁ for every x and every h ≠ 0. This is the pointwise commutator bound used in the master interior estimate to control the coefficient- difference-quotient term ∑ ∫ (Dₖʰ aᵢⱼ) ∂ᵢu · ∂ⱼ(ζ² Dₖʰ u) (Evans, Partial Differential Equations (2nd ed.), §6.3.1).