Local boundary extension #
Guo's Theorem III.2.2 reaches its third step with a local extension for each chart: a class on the chart's neighbourhood agreeing with the original on the part of the domain that neighbourhood meets. This file proves that statement, which is the whole content of his step 2 once the chart is in hand.
The proof composes what the chapter has built. A cutoff between two balls makes the class reach the whole region above the chart's graph, the rigid motion of the chart takes it into the coordinates the graph is written in, the reflection extends it across the graph, and the motion takes the result back. Guo's step 2 works with a function smooth up to the boundary and reads the chain rule off it; here every step is a weak gradient.
Two points where the statement is narrower than the machinery. The chart asks nothing of the
gradient of its graph, as Evans' definition does not, so the proof runs on the bounded graph
exists_bounded_graph supplies, whose region agrees with the chart's on exactly the ball in
play. The conclusion is on a ball strictly inside the chart's, which is where the cutoff is one,
and is what a partition of unity subordinate to the cover asks for anyway.
Constant before the class #
Clause (iii) of the theorem asks for a constant quantified before the class, and the chain the
construction runs through re-chooses data at three places: the bounded graph of
exists_bounded_graph, the cutoff between the two balls, and the bound each supplies. All three
depend on the chart and the two radii alone, so exists_localExtension_bound fixes them first
and lets the class come after. The bound then threads the five estimates the chain has: the
cutoff's supremum, the rigid motion, the reflection, the shear, and the sum over the coordinates
the motion mixes.
Main declarations #
EllipticPdes.Extension.exists_localExtension_bound: the local boundary extension with a constant fixed before the class.EllipticPdes.Extension.exists_localExtension: the same with the constant discarded.
References #
James Guo, Partial Differential Equations (Course Lecture Notes), Theorem III.2.2 (p. 20), proof step 2 (p. 21); L. C. Evans, Partial Differential Equations (2nd ed.), §5.4 Theorem 1 (p. 253).
Two seminorm estimates the chain threads #
Seminorm of a coordinate combination. A combination of finitely many classes whose coefficients are at most one in absolute value has seminorm at most the sum of theirs. This is what the rigid motion of a chart contributes, the coordinates of the image of a unit direction being at most one.
Seminorm of a class cut off inside a neighbourhood. The cutoff vanishes off W, and on
S ∩ W the class is read on T, so the product over S is bounded by the supremum of the
cutoff against the seminorm over T. This is what lets an estimate taken over the region above
a chart's graph be stated against the domain.
Seminorm of a class scaled by a bounded factor, the factor written first.
The local extension #
Local extension as a formula in the class. The class is read in the chart's
coordinates, cut off there, extended across the flattened boundary, and returned. Every step
but the class itself is fixed by the chart, its graph γ and the cutoff ξ, so the whole is
linear in the class.
Equations
- EllipticPdes.Extension.localExtFun c γ ξ u y = EllipticPdes.Extension.chartExt c.dir γ (fun (z : EuclideanSpace ℝ (Fin d)) => ξ (c.motion.symm z) * u (c.motion.symm z)) (c.motion y)
Instances For
Gradient of the local extension. The cutoff contributes its own derivative by the product rule, the chart's rigid motion mixes the coordinates on the way in and on the way out, and the shear and the reflection supply the rest.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bounded graph the chart's extension runs on. A chart's own graph need not have a
bounded gradient, which every statement about the shear asks for, and exists_bounded_graph
supplies one agreeing with it on the chart's ball. The choice is made from the chart alone,
before any class appears, which is what keeps the extension linear.
Equations
Instances For
What chartGraph was chosen for.
The cutoff between the ball the extension is asked for and the chart's own. Chosen from the two radii alone, before any class appears.
Equations
Instances For
What chartCutoff was chosen for.
Local extension of a class. localExtFun at the graph and the cutoff the chart
fixes, so the only argument left is the class.
Equations
Instances For
Gradient of the local extension of a class.
Equations
- EllipticPdes.Extension.localExtGrad c x hrc u g = EllipticPdes.Extension.localExtGradFun c (EllipticPdes.Extension.chartGraph c x) (EllipticPdes.Extension.chartCutoff x hrc) u g
Instances For
Guo's local boundary extension with its constant (Theorem III.2.2, proof step 2, p. 21).
Near a boundary point the class extends across the boundary: on any ball strictly inside the
chart's, localExt has a weak gradient there and agrees with the original on the part of the
domain the ball meets, and both it and its gradient are bounded in every Lᵖ seminorm by the
class and its gradient over the domain, with one constant taken before the class.
The extension is named rather than existentially quantified, which is what lets the operator be assembled as a linear map.
Linearity of the local extension #
The chart extension of a class read through the chart is additive in the class.
The chart extension of a class read through the chart commutes with a scalar.
The gradient of that extension is additive in the class and its gradient.
The gradient of that extension commutes with a scalar.
Local extension is additive in the class.
Local extension commutes with a scalar.
Gradient of the local extension is additive in the class and its gradient.
Gradient of the local extension commutes with a scalar.
Guo's local boundary extension with its constant, with the extension quantified away. This is the form the gluing of step 3 consumes.
Guo's local boundary extension (Theorem III.2.2, proof step 2, p. 21). Near a boundary point the class extends across the boundary: on any ball strictly inside the chart's, there is a class with a weak gradient there agreeing with the original on the part of the domain the ball meets.