H^k norm of an iterated family

Evans, Partial Differential Equations (2nd ed.), §5.2.2 (p. 259) defines

‖u‖_{W^{k,p}(U)} = (Σ_{|α| ≤ k} ∫_U |D^α u|^p dx)^{1/p}

for multi-indices α. A family HasIteratedWeakDerivOn V k u indexes derivatives by lists of directions, one list per ordered sequence of differentiations, so a multi-index of order j corresponds to as many lists as it has orderings. iteratedNorm is the same sum taken over lists:

iteratedNorm H = (Σ_{j ≤ k} Σ_{α ∈ (Fin d)^j} ‖D_α u‖²_{L²(V)})^{1/2}.

Weak derivatives commute, so each multi-index contributes its L² norm squared with the multiplicity of its orderings, between 1 and j!; the two norms are equivalent with constants depending on d and k alone. Weak derivatives on an open set are unique, so the value does not depend on the family chosen.

Main declarations

• iteratedNorm: the norm.
• norm_D_le_iteratedNorm: every entry of the family is bounded by it.
• iteratedNorm_le: a uniform bound on the entries bounds it, with a constant in d and k.

noncomputable def EllipticPdes.Regularity.iteratedNorm {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {u : Sobolev.L2D V} (H : HasIteratedWeakDerivOn V k u) : ℝ

H^k(V) norm of an iterated family, summed over lists of directions of length at most k.

Equations

• EllipticPdes.Regularity.iteratedNorm H = √(∑ m ∈ Finset.range (k + 1), ∑ α : Fin m → Fin d, ‖H.D (List.ofFn α)‖ ^ 2)

theorem EllipticPdes.Regularity.iteratedNorm_nonneg {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {u : Sobolev.L2D V} (H : HasIteratedWeakDerivOn V k u) : 0 ≤ iteratedNorm H

theorem EllipticPdes.Regularity.norm_D_le_iteratedNorm {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {u : Sobolev.L2D V} (H : HasIteratedWeakDerivOn V k u) {α : List (Fin d)} (hα : α.length ≤ k) : ‖H.D α‖ ≤ iteratedNorm H

Every entry of the family up to order k is bounded by the norm.

theorem EllipticPdes.Regularity.iteratedL2Bound_iteratedNorm {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {u : Sobolev.L2D V} (H : HasIteratedWeakDerivOn V k u) : IteratedL2Bound H (iteratedNorm H)

The norm is a uniform bound on the family.

def EllipticPdes.Regularity.listCount (d k : ℕ) : ℝ

The number of lists of directions of length at most k, as a real number.

Equations

• EllipticPdes.Regularity.listCount d k = ∑ m ∈ Finset.range (k + 1), ↑d ^ m

theorem EllipticPdes.Regularity.listCount_nonneg (d k : ℕ) : 0 ≤ listCount d k

theorem EllipticPdes.Regularity.iteratedNorm_le {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {k : ℕ} {u : Sobolev.L2D V} {H : HasIteratedWeakDerivOn V k u} {C : ℝ} (hC : IteratedL2Bound H C) : iteratedNorm H ≤ √(listCount d k) * C

Norm bound from a uniform bound on the family, with the factor √N for N the number of lists of length at most k.