W^{k,∞} regularity for the transport and zeroth-order coefficients

EllipticPdes.Sobolev.FullEllipticOp gives b and c sup bounds and measurability and no derivatives at all, which is everything the existence theory and the interior H² estimate need. Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65) asks for a_{ij} ∈ W^{k+2,∞} and b_i, c ∈ W^{k+1,∞}, one order less on the lower-order coefficients than on the principal part, because the lower-order terms are differentiated once less often on the way to the same conclusion. This file supplies the missing hypothesis.

Scalar predicate and bundle

IsWkInfty f k states the hypothesis for a single scalar function, and IsWkInftyLower bundles it over the d + 1 lower-order coefficients with a constant uniform across them. Splitting it this way lets IsWkInfty.deriv be stated once and used for b, for c, and for anything else the induction differentiates.

Main declarations

• IsWkInfty: weak derivatives to order k of a scalar function, essentially bounded.
• IsWkInfty.deriv: an order-k+1 bundle for f gives an order-k bundle for ∂_l f.
• IsWkInfty.ofContDiff: a Cᵏ function with bounded derivatives satisfies it.
• IsWkInfty.const: a constant satisfies it at every order.
• IsWkInftyCoeff.entry: one entry of the coefficient matrix, as a scalar bundle.
• IsWkInftyLower: Guo's hypothesis on b and c, with a uniform constant.

Scalar hypothesis

structure EllipticPdes.Regularity.IsWkInfty {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℝ) (k : ℕ) : Type

f ∈ W^{k,∞}, given as data: a family of weak derivatives indexed by lists of directions, each measurable and essentially bounded, with no continuity assumed. The order-zero member is f itself, so bound 0 is a sup bound on f.

• D : List (Fin d) → EuclideanSpace ℝ (Fin d) → ℝ

  The chosen representative of the iterated weak derivative along a list of directions.

• D_nil : self.D [] = f

  The empty list of directions is the function itself.

• D_meas (α : List (Fin d)) : α.length ≤ k → Measurable (self.D α)

  Every entry of the family is measurable.

• D_step (l : Fin d) (α : List (Fin d)) : α.length < k → HasWeakPartial l (self.D α) (self.D (l :: α))

  Each successive entry is a weak partial derivative of its parent, up to order k.

• bound : ℕ → ℝ

  The uniform bound on the derivatives of each order.

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

  Every bound is nonnegative.

• ess_bdd (α : List (Fin d)) : α.length ≤ k → ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |self.D α x| ≤ self.bound α.length

  Each derivative of order m ≤ k is bounded by bound m almost everywhere.

def EllipticPdes.Regularity.IsWkInfty.mono {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} {k l : ℕ} (hf : IsWkInfty f k) (hlk : l ≤ k) : IsWkInfty f l

An order-k bundle is an order-l bundle for every l ≤ k.

Equations

• hf.mono hlk = { D := hf.D, D_nil := ⋯, D_meas := ⋯, D_step := ⋯, bound := hf.bound, bound_nonneg := ⋯, ess_bdd := ⋯ }

def EllipticPdes.Regularity.IsWkInfty.deriv {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} {k : ℕ} (hf : IsWkInfty f (k + 1)) (m : Fin d) : IsWkInfty (hf.D [m]) k

Differentiating the hypothesis. From f ∈ W^{k+1,∞}, the first derivative D [m] is in W^{k,∞}, with family α ↦ D (α ++ [m]) and the bounds shifted by one order. Appending on the right makes the lengths line up, exactly as in HasIteratedWeakDerivOn.deriv; this step lets the induction of Guo's Theorem VIII.3.2 keep its coefficient hypothesis.

Equations

• hf.deriv m = { D := fun (α : List (Fin d)) => hf.D (α ++ [m]), D_nil := ⋯, D_meas := ⋯, D_step := ⋯, bound := fun (j : ℕ) => hf.bound (j + 1), bound_nonneg := ⋯, ess_bdd := ⋯ }

noncomputable def EllipticPdes.Regularity.IsWkInfty.ofContDiff {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} {k : ℕ} {B : ℕ → ℝ} (hf : ContDiff ℝ (↑↑k) f) (hB : ∀ (m : ℕ), 0 ≤ B m) (hbd : ∀ m ≤ k, ∀ (x : EuclideanSpace ℝ (Fin d)), ‖iteratedFDeriv ℝ m f x‖ ≤ B m) : IsWkInfty f k

Cᵏ function with bounded derivatives in W^{k,∞}. The classical iterated partials serve as the family, through hasWeakPartial_partialD, and the pointwise iteratedFDeriv bounds transfer through abs_iterPartial_le. Order zero is included here, unlike in IsCkCoeff, where EllipticCoeff.Λ already has it.

Equations

• EllipticPdes.Regularity.IsWkInfty.ofContDiff hf hB hbd = { D := EllipticPdes.Regularity.iterPartial f, D_nil := ⋯, D_meas := ⋯, D_step := ⋯, bound := B, bound_nonneg := hB, ess_bdd := ⋯ }

noncomputable def EllipticPdes.Regularity.IsWkInfty.const {d : ℕ} (c : ℝ) (k : ℕ) : IsWkInfty (fun (x : EuclideanSpace ℝ (Fin d)) => c) k

Constants in W^{k,∞} at every order. Its derivatives past the zeroth vanish, so one bound serves every order. The datum of the induction step has a term with no coefficient at all, namely the derivative of the datum itself, and this is what lets it be treated as a weighted term like the rest.

Equations

• EllipticPdes.Regularity.IsWkInfty.const c k = EllipticPdes.Regularity.IsWkInfty.ofContDiff ⋯ ⋯ ⋯

def EllipticPdes.Regularity.IsWkInftyCoeff.entry {d : ℕ} {A : Sobolev.EllipticCoeff d} {k : ℕ} (hA : IsWkInftyCoeff A k) (i j : Fin d) : IsWkInfty (fun (x : EuclideanSpace ℝ (Fin d)) => A.a x i j) k

Single entry of the coefficient matrix as a W^{k,∞} function. The matrix bundle already has a family for each entry, so the scalar bundle is that family read at a fixed pair of indices.

Equations

• hA.entry i j = { D := fun (α : List (Fin d)) => hA.D α i j, D_nil := ⋯, D_meas := ⋯, D_step := ⋯, bound := hA.bound, bound_nonneg := ⋯, ess_bdd := ⋯ }

Bundle over the lower-order coefficients

structure EllipticPdes.Regularity.IsWkInftyLower {d : ℕ} (Op : Sobolev.FullEllipticOp d) (k : ℕ) : Type

Guo's hypothesis on the lower-order coefficients. Every transport component and the zeroth-order coefficient lie in W^{k,∞}, with one constant serving all of them. The uniform constant is what the estimate of Theorem VIII.3.2 is stated against, so it is recorded here rather than reconstructed as a maximum at the point of use.

• bReg (i : Fin d) : IsWkInfty (fun (x : EuclideanSpace ℝ (Fin d)) => Op.b x i) k

  Each transport component is in W^{k,∞}.

• cReg : IsWkInfty Op.c k

  The zeroth-order coefficient is in W^{k,∞}.

• bound : ℕ → ℝ

  The constant uniform across the lower-order coefficients.

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

  Every bound is nonnegative.

• b_le (i : Fin d) (m : ℕ) : (self.bReg i).bound m ≤ self.bound m

  The transport bounds are dominated by the uniform constant.

• c_le (m : ℕ) : self.cReg.bound m ≤ self.bound m

  The zeroth-order bound is dominated by the uniform constant.

def EllipticPdes.Regularity.IsWkInftyLower.mono {d : ℕ} {Op : Sobolev.FullEllipticOp d} {k l : ℕ} (hOp : IsWkInftyLower Op k) (hlk : l ≤ k) : IsWkInftyLower Op l

An order-k bundle is an order-l bundle for every l ≤ k.

Equations

• hOp.mono hlk = { bReg := fun (i : Fin d) => (hOp.bReg i).mono hlk, cReg := hOp.cReg.mono hlk, bound := hOp.bound, bound_nonneg := ⋯, b_le := ⋯, c_le := ⋯ }

theorem EllipticPdes.Regularity.IsWkInftyLower.ae_abs_b_le {d : ℕ} {Op : Sobolev.FullEllipticOp d} {k : ℕ} (hOp : IsWkInftyLower Op k) (i : Fin d) (α : List (Fin d)) (hα : α.length ≤ k) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |(hOp.bReg i).D α x| ≤ hOp.bound α.length

Every transport component is essentially bounded by the uniform constant at every order up to k.

theorem EllipticPdes.Regularity.IsWkInftyLower.ae_abs_c_le {d : ℕ} {Op : Sobolev.FullEllipticOp d} {k : ℕ} (hOp : IsWkInftyLower Op k) (α : List (Fin d)) (hα : α.length ≤ k) : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), |hOp.cReg.D α x| ≤ hOp.bound α.length

The zeroth-order coefficient is essentially bounded by the uniform constant at every order up to k.