W^{1,∞} principal coefficients

Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 1 asks aᵢⱼ ∈ C¹ for the interior H² estimate, where Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65) asks aᵢⱼ ∈ W^{1,∞}. On ℝᵈ a W^{1,∞} function is one with a Lipschitz representative, so in its pointwise form the hypothesis is the Lipschitz estimate of IsLipCoeff below.

The estimate consumes the hypothesis through abs_diffQuot_coeff_le alone, which IsC1Coeff supplies by the mean value inequality and a Lipschitz coefficient supplies outright. IsC1Coeff.toIsLipCoeff is therefore what makes the C¹ statement the instance: the interior estimate, higher interior regularity and interior smoothness all run over IsLipCoeff and no step of them asks a principal coefficient to be differentiable.

Main declarations

• IsLipCoeff: the Lipschitz estimate on the principal coefficients.
• IsLipCoeff.abs_diffQuot_coeff_le: the coefficient difference-quotient bound.
• IsC1Coeff.toIsLipCoeff: the bridge, by the segment mean value inequality.

Statements this file does not supply

The passage from an IsWkInftyCoeff A 1 bundle, whose derivative bound is essential rather than pointwise, to IsLipCoeff. That passage is the statement that a W^{1,∞} function has a Lipschitz representative, and Mathlib has Rademacher's theorem in the opposite direction alone (LipschitzWith.ae_differentiableAt). Until it is proved the two hypotheses are distinct, and interior_smooth asks IsLipCoeff beside its W^{k,∞} bundles rather than reading the first from the second.

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

A W^{1,∞} ellipticity bundle in pointwise form: every entry of the coefficient matrix satisfies the Lipschitz estimate with one constant A₁, and no entry is asked to be differentiable.

• A1 : ℝ

  The uniform Lipschitz constant of the entries.

• A1_nonneg : 0 ≤ self.A1

  A1 is nonnegative.

• lip (i j : Fin d) (x y : EuclideanSpace ℝ (Fin d)) : |A.a x i j - A.a y i j| ≤ self.A1 * ‖x - y‖

  Every entry is Lipschitz with constant A1.

theorem EllipticPdes.Regularity.IsLipCoeff.abs_diffQuot_coeff_le {d : ℕ} {A : Sobolev.EllipticCoeff d} (hA : IsLipCoeff 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), and it is the whole of what that estimate asks of the principal coefficients beyond their bounds.

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

A C¹ bundle is a W^{1,∞} bundle. The segment mean value inequality turns the pointwise bound on the first derivatives into the Lipschitz estimate with the same constant, so a result proved under IsLipCoeff applies to a C¹ coefficient and Guo's hypothesis is no stronger than Evans's as far as the principal coefficients go.

Equations

• hA.toIsLipCoeff = { A1 := hA.A1, A1_nonneg := ⋯, lip := ⋯ }