Gluing the local extensions #
Guo's third step covers the boundary, fixes a partition of unity subordinate to that cover with
each support compactly inside its neighbourhood, and sets ū = ∑ᵢ Pᵢ ūᵢ. This file carries out
that sum.
Each piece is a local extension cut down by its piece of the partition, so the cutoff comes
after the extension. That order is what makes the sum agree with the class: where a piece of the
partition is nonzero the point lies in that chart's ball, where the local extension agrees with
the class, so the piece equals Pᵢ u there and off the ball both sides vanish. The pieces then
add to u because the partition adds to one.
supp(Pᵢ) ⋐ Wᵢ is compact containment, and the local extension of step 2 lives on a ball
strictly inside the chart's, so the support is first pushed into a smaller ball. A compact
subset of an open ball admits one.
The support clause follows by one more cutoff, which is how Guo reaches it: any open set the closure of the domain sits in admits a smooth cutoff equal to one on that closure, and multiplying by it moves the support inside without disturbing the agreement.
Constant of clause (iii) #
The partition, the charts, the radii and the supremum of each piece and of its partials all
depend on the domain alone, so exists_extension_bound fixes them before the class appears and
sums the local constants of exists_localExtension_bound over the finitely many pieces. That is
clause (iii): one constant, depending on the domain and the exponent, bounding the extension and
its gradient by the class and its gradient over the domain.
Main declarations #
EllipticPdes.Extension.exists_lt_radius_of_isCompact_subset_ball: a compact subset of an open ball sits in a strictly smaller one.EllipticPdes.Extension.exists_extension_bound: the class extends across the whole boundary, with a constant taken before the class.EllipticPdes.Extension.exists_extension: the same with the constant discarded.EllipticPdes.Extension.exists_cutoff_one_on_compact: a smooth cutoff between a compact set and an open one.EllipticPdes.Extension.exists_extension_subset_bound: the three clauses of the theorem.EllipticPdes.Extension.exists_extension_subset: clauses (i) and (ii).
References #
James Guo, Partial Differential Equations (Course Lecture Notes), Theorem III.2.2 (p. 20), proof step 3 (p. 22); L. C. Evans, Partial Differential Equations (2nd ed.), §5.4 Theorem 1 (p. 253).
Shrinking an open ball around a compact subset.
The partition, the radii and the pieces, all fixed by the domain #
A boundary piece of the partition is supported in its chart's ball, hence compactly.
The ball the local extension of a boundary piece is taken on: strictly inside the chart's, and still containing the support of the piece. Chosen from the partition alone.
Equations
Instances For
What pieceRadius was chosen for.
The chosen ball sits strictly inside the chart's.
The chosen ball still contains the support of the piece.
One piece of the glued extension. The interior piece is the class extended by zero and
cut down by its piece of the partition; a boundary piece is the local extension of its chart,
cut down the same way. The cutoff comes after the extension, which is what makes the piece
agree with Pᵢ u on the domain.
Equations
- One or more equations did not get rendered due to their size.
- EllipticPdes.Extension.extPiece P none u = fun (y : EuclideanSpace ℝ (Fin d)) => P.part none y * Ω.indicator u y
Instances For
Gradient of one piece, with the product rule's second term.
Equations
Instances For
Glued extension. The pieces add to the class on the domain because the partition adds to one there.
Equations
- EllipticPdes.Extension.extFun P u y = ∑ i : Option ↥P.centres, EllipticPdes.Extension.extPiece P i u y
Instances For
Gradient of the glued extension.
Equations
- EllipticPdes.Extension.extFunGrad P u g k y = ∑ i : Option ↥P.centres, EllipticPdes.Extension.extPieceGrad P i u g k y
Instances For
Guo's third step with its constant (Theorem III.2.2, proof step 3, p. 22): the local extensions glued with the partition of unity extend the class across the whole boundary, and one constant, taken before the class, bounds the extension and its gradient by the class and its gradient over the domain.
Guo's third step with its constant, with the partition and the extension quantified away. This is the form the support clause and the embedding consume.
Guo's third step (Theorem III.2.2, proof step 3, p. 22): the local extensions glued with the partition of unity extend the class across the whole boundary.
Cutting between a compact set and an open one. A smooth cutoff equal to one on the compact set and compactly supported inside the open one.
Extension with its support cut into a given open set. One more cutoff, equal to one on the closure of the domain, which leaves the agreement alone and moves the support.
Equations
- EllipticPdes.Extension.extSubsetFun P χ u y = χ y * EllipticPdes.Extension.extFun P u y
Instances For
Gradient of that extension, with the cutoff's own derivative.
Equations
- EllipticPdes.Extension.extSubsetGrad P χ u g k y = χ y * EllipticPdes.Extension.extFunGrad P u g k y + EllipticPdes.Sobolev.partialD k χ y * EllipticPdes.Extension.extFun P u y
Instances For
extSubsetFun unapplied, which is the form the support statements read.
extSubsetGrad unapplied.
Guo's Theorem III.2.2 (p. 20), all three clauses. The extension agrees with the class on
the domain, is supported inside any open set the closure of the domain sits in, and is bounded
in every Lᵖ seminorm, together with its gradient, by the class and its gradient over the
domain, with one constant taken before the class.
Guo's Theorem III.2.2 (p. 20), all three clauses, with the partition, the cutoff and the extension quantified away.
Clauses (i) and (ii) of Guo's Theorem III.2.2 (p. 20). The extension agrees with the class on the domain and is supported inside any open set the closure of the domain sits in.