Cᵏ coefficients indexed by the derivative order

Higher interior regularity (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2) runs by induction on m, and its hypothesis moves with the induction: reaching u ∈ H^{m+2}_loc asks for aᵢⱼ ∈ C^{m+1}. A hypothesis whose derivative order is fixed by the name of the structure cannot be the induction hypothesis of that argument, so IsC1Coeff and IsC2Coeff each state one instance of a family and neither states the family. This file gives the family.

IsCkCoeff A k bundles ContDiff ℝ k on every entry together with a uniform bound on each iterated derivative of order 1 ≤ m ≤ k. Orders start at one because order zero is already supplied by EllipticCoeff.Λ, so the mixin adds exactly the derivative data and nothing that the bundle beneath it already supplies.

The bounds are collected as a single function bound : ℕ → ℝ rather than as one field per order. A Fin (k+1)-indexed family would record the order in its type and force a cast at every use; the constraint 1 ≤ m ≤ k in iteratedFDeriv_bdd says which values of the function are meaningful, and mono then restricts to a lower order without touching it.

Derivatives are taken as iteratedFDeriv, where IsC2Coeff nests fderiv inside fderiv. The two agree at order two (norm_fderiv_fderiv_eq below, from Mathlib's norm_iteratedFDeriv_fderiv and norm_iteratedFDeriv_one), and only the iterated form has a statement at a general order.

Main declarations

• IsCkCoeff: the indexed mixin.
• IsCkCoeff.mono: an order-k bundle is an order-l bundle for every l ≤ k.
• IsCkCoeff.toIsC1Coeff, IsC1Coeff.toIsCkCoeff: the round trip at order one.
• IsCkCoeff.toIsC2Coeff, IsC2Coeff.toIsCkCoeff: the round trip at order two.

Both existing structures are left in place and unchanged, so every current consumer of IsC1Coeff and IsC2Coeff is untouched, and a consumer written against the family can be fed from either by the conversions above.

theorem EllipticPdes.Regularity.norm_fderiv_fderiv_eq {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) : ‖fderiv ℝ (fderiv ℝ f) x‖ = ‖iteratedFDeriv ℝ 2 f x‖

The second derivative read as a nested fderiv and as iteratedFDeriv have the same norm. This is the bridge between IsC2Coeff.hess_bdd and IsCkCoeff.iteratedFDeriv_bdd at order two.

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

A Cᵏ ellipticity bundle: every coefficient entry is k times continuously differentiable, with a uniform bound bound m on the iterated derivative of each order 1 ≤ m ≤ k. A mixin on top of EllipticCoeff, in the manner of IsC1Coeff, indexed by the order so that it can serve as the induction hypothesis of Evans §6.3.1, Theorem 2.

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

  Every coefficient entry is k times continuously differentiable.

• bound : ℕ → ℝ

  The uniform bound on the derivatives of each order. Only the values at 1 ≤ m ≤ k are constrained by iteratedFDeriv_bdd.

• bound_nonneg (m : ℕ) : 0 ≤ self.bound m

  Every bound is nonnegative.

• iteratedFDeriv_bdd (i j : Fin d) (m : ℕ) : 1 ≤ m → m ≤ k → ∀ (x : EuclideanSpace ℝ (Fin d)), ‖iteratedFDeriv ℝ m (fun (y : EuclideanSpace ℝ (Fin d)) => A.a y i j) x‖ ≤ self.bound m

  The iterated derivative of order m of every entry is bounded by bound m at every point, for every order m between one and k.

def EllipticPdes.Regularity.IsCkCoeff.mono {d : ℕ} {A : Sobolev.EllipticCoeff d} {k l : ℕ} (hA : IsCkCoeff A k) (hlk : l ≤ k) : IsCkCoeff A l

An order-k bundle is an order-l bundle for every l ≤ k: the differentiability weakens by ContDiff.of_le and the bounds are inherited unchanged.

Equations

• hA.mono hlk = { contDiff := ⋯, bound := hA.bound, bound_nonneg := ⋯, iteratedFDeriv_bdd := ⋯ }

def EllipticPdes.Regularity.IsCkCoeff.toIsC1Coeff {d : ℕ} {A : Sobolev.EllipticCoeff d} {k : ℕ} (hA : IsCkCoeff A k) (hk : 1 ≤ k) : IsC1Coeff A

An order-k bundle with 1 ≤ k is a C¹ bundle, at the order-one bound.

Equations

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

def EllipticPdes.Regularity.IsCkCoeff.toIsC2Coeff {d : ℕ} {A : Sobolev.EllipticCoeff d} {k : ℕ} (hA : IsCkCoeff A k) (hk : 2 ≤ k) : IsC2Coeff A

An order-k bundle with 2 ≤ k is a C² bundle, at the order-one and order-two bounds.

Equations

• hA.toIsC2Coeff hk = { contDiff := ⋯, A1 := hA.bound 1, A1_nonneg := ⋯, grad_bdd := ⋯, A2 := hA.bound 2, A2_nonneg := ⋯, hess_bdd := ⋯ }

def EllipticPdes.Regularity.IsC1Coeff.toIsCkCoeff {d : ℕ} {A : Sobolev.EllipticCoeff d} (hA : IsC1Coeff A) : IsCkCoeff A 1

A C¹ bundle is an order-one bundle, the single bound A1 serving every order.

Equations

• hA.toIsCkCoeff = { contDiff := ⋯, bound := fun (x : ℕ) => hA.A1, bound_nonneg := ⋯, iteratedFDeriv_bdd := ⋯ }

def EllipticPdes.Regularity.IsC2Coeff.toIsCkCoeff {d : ℕ} {A : Sobolev.EllipticCoeff d} (hA : IsC2Coeff A) : IsCkCoeff A 2

A C² bundle is an order-two bundle, A1 at order one and A2 above it.

Equations

• hA.toIsCkCoeff = { contDiff := ⋯, bound := fun (m : ℕ) => if m = 1 then hA.A1 else hA.A2, bound_nonneg := ⋯, iteratedFDeriv_bdd := ⋯ }