Iterated weak derivatives on a region #
The interior H² estimate EllipticPdes.Regularity.interior_H2_estimate produces one weak
derivative of one weak derivative, indexed by an explicit pair (k, i). Higher regularity
iterates that step, so the pair has to become a list and the statement has to quantify over
its length. This file supplies the indexed object.
HasIteratedWeakDerivOn V k u names a family D : List (Fin d) → L²(V) with D [] = u and
each D (l :: α) a weak l-derivative of D α, for every list shorter than k. It is the
L²-level reading of u ∈ H^k(V), given as data rather than as an existential, so that a proof
can name a particular derivative and hand it on.
Choice of a list of directions #
The same choice as in EllipticPdes.Regularity.IsWkInftyCoeff, and for the same reason: one
step of the recursion is cons. A multi-index in Fin d →₀ ℕ would need equality of mixed
partials before the recursion could even be stated, and that equality is a theorem about the
family rather than part of its definition. Nothing here presumes it.
Main declarations #
HasIteratedWeakDerivOn: weak derivatives up to orderkonV, given as a family.HasIteratedWeakDerivOn.mono: an order-kfamily is an order-lfamily forl ≤ k.HasIteratedWeakDerivOn.deriv: the order-kfamily of a first derivative, extracted from an order-k+1family by appending the direction on the right. This is the step the induction of Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65) runs on.IteratedL2Bound: a uniform bound on every member of the family up to orderk.
Iterated weak derivatives on a region. A family of L²(V) classes indexed by lists of
directions, with the empty list the function itself and each cons a weak derivative of its
parent. Giving the family as data rather than asserting existence at each order lets a consumer
name D [i, j] and pass it on, which the induction of Guo, Partial Differential Equations I
and II (Course Lecture Notes), Theorem VIII.3.2 (p. 65) requires.
- D : List (Fin d) → Sobolev.L2D V
The chosen representative of the iterated weak derivative along a list of directions.
The empty list of directions is the function itself.
- D_step (m : Fin d) (α : List (Fin d)) : α.length < k → HasWeakDerivOn V m (self.D α) (self.D (m :: α))
Each successive entry is a weak derivative of its parent, up to order
k.
Instances For
Every L² class has weak derivatives up to order zero, vacuously: the family is constant
and D_step is asked of no list.
Equations
Instances For
An order-k family is an order-l family for every l ≤ k: the family is inherited and
D_step is asked of fewer lists.
Instances For
Transport along an equality of the subject. The family is unchanged; only the proof
that its empty entry is the function moves. Stated because the induction reaches the derivative
of u through a cutoff, whose function coordinate agrees with the derivative on the region of
interest without being the same term.
Instances For
Induction step. From weak derivatives up to order k + 1 of u, the direction
l first derivative D [l] has weak derivatives up to order k, with family
α ↦ D (α ++ [l]). Appending on the right rather than consing on the left is what makes the
lengths line up: (α ++ [l]).length < k + 1 is exactly α.length < k, so every step the new
family needs is a step the old family already has.
This is the reduction that turns Guo's Theorem VIII.3.2 into an induction on k: an
H^{k+2} conclusion for u is an H^{k+1} conclusion for each ∂_l u, and ∂_l u solves a
differentiated equation of the same form.
Instances For
First derivative two orders down. The datum of the induction step multiplies
derivatives of the solution of order at most two, and asks each of them for k weak
derivatives of its own. Naming the two cases here rather than inlining them keeps the
definitional unfolding of deriv out of the assembly, where it is repeated a dozen times.
Instances For
A second derivative, at two orders down.
Instances For
The order-one family of a function with derivatives to order k + 1 records a weak
derivative in every direction.
The assembly a family is read off: the empty list is the function, and a nonempty list is
the family of its last direction's derivative, indexed by what remains. Reversing is what makes
the last direction visible, since D_step conses on the left.
Equations
Instances For
Inverse of deriv. Weak derivatives in every direction, each with its own order-k
family, assemble into an order-k + 1 family of the function itself. The index of the assembled
family reads β ++ [ℓ] as the β-entry of the family of ∂_ℓ u, which is the convention
deriv uses in the other direction.
This is the step that brings the conclusion of the induction of Guo, Partial Differential
Equations I and II (Course Lecture Notes), Theorem VIII.3.2 (p. 65) back to the solution:
the induction hypothesis is applied to each ∂_ℓ u and its conclusions are reassembled here.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Uniform L² bound on an iterated family. Every derivative up to order k is
bounded by C in L²(V). Kept apart from HasIteratedWeakDerivOn so that existence and
estimate can be proved and consumed separately, matching the shape of
interior_H2_estimate, which returns the derivative and its bound as separate conjuncts.
Equations
Instances For
A bound at order k bounds the function itself.
A bound is inherited by any larger constant.
Transport preserves the bound: the family is unchanged.
A bound at order k restricts to a bound on the order-l family for l ≤ k.
The bound is inherited by the family of a derivative.
The bound is inherited by the family of a first derivative.
The bound is inherited by the family of a second derivative.
The bound on an assembled family, read off the function and each first derivative's family.