Extension across a C¹ boundary chart

Near a boundary point a domain with C¹ boundary is, after relabelling the coordinates, the region above the graph of a C¹ function γ of the remaining ones. This file extends a Sobolev class across that graph, which is the local half of Guo's extension operator.

The route is the composite of the three maps the chapter has built. The shear S y = y + γ(y)eⱼ inverts the flattening, so the flattening T = S⁻¹ sends the region above the graph onto the half space; the class travels the other way, through S, and picks up the transpose of the shear's derivative on its gradient. The flattened class is then reflected across the interface, and the reflection returns through T.

Main declarations

• EllipticPdes.Extension.aboveGraph: the region above the graph of a chart.
• EllipticPdes.Extension.preimage_shear_aboveGraph: the shear pulls that region back to the half space.
• EllipticPdes.Extension.chartExt and EllipticPdes.Extension.chartExtGrad: the extension and its gradient.
• EllipticPdes.Extension.hasWeakGradOn_chartExt: the extension has that weak gradient on the whole space.
• EllipticPdes.Extension.chartExt_eq_of_mem: the extension agrees with the class on the region it extends.
• EllipticPdes.Extension.eLpNorm_chartExt_le and EllipticPdes.Extension.eLpNorm_chartExtGrad_le: the extension and its gradient, bounded in every Lᵖ seminorm.

References

James Guo, Partial Differential Equations (Course Lecture Notes), Theorem III.2.2 steps 1 and 2 (p. 21); L. C. Evans, Partial Differential Equations (2nd ed.), §5.4 Theorem 1 and §C.1.

The region above a graph

def EllipticPdes.Extension.aboveGraph {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) : Set (EuclideanSpace ℝ (Fin d))

Region above the graph of a chart, in the j-th coordinate.

Equations

• EllipticPdes.Extension.aboveGraph j γ = {y : EuclideanSpace ℝ (Fin d) | γ y < y.ofLp j}

theorem EllipticPdes.Extension.isOpen_aboveGraph {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Continuous γ) : IsOpen (aboveGraph j γ)

theorem EllipticPdes.Extension.shear_coord {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (y : EuclideanSpace ℝ (Fin d)) : (shear j γ y).ofLp j = y.ofLp j + γ y

The j-th coordinate of a sheared point.

theorem EllipticPdes.Extension.aboveGraph_eq_preimage {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} : aboveGraph j γ = (shear j fun (z : EuclideanSpace ℝ (Fin d)) => -γ z) ⁻¹' halfSpace j

Pull-back of the half space through the flattening.

theorem EllipticPdes.Extension.preimage_shear_aboveGraph {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hind : IndepCoord j γ) : shear j γ ⁻¹' aboveGraph j γ = halfSpace j

Pull-back of the region above the graph through the shear.

The extension

noncomputable def EllipticPdes.Extension.shearGrad {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : EuclideanSpace ℝ (Fin d) → ℝ

Gradient of a class pulled back through the shear, the transpose of the shear's derivative applied to the gradient.

Equations

• EllipticPdes.Extension.shearGrad j γ g k x = g k (EllipticPdes.Extension.shear j γ x) + g j (EllipticPdes.Extension.shear j γ x) * EllipticPdes.Sobolev.partialD k γ x

noncomputable def EllipticPdes.Extension.chartExt {d : ℕ} (j : Fin d) (γ u : EuclideanSpace ℝ (Fin d) → ℝ) : EuclideanSpace ℝ (Fin d) → ℝ

Extension across a C¹ boundary chart. The chart is flattened by the shear, the flattened class is reflected across the interface, and the reflection returns through the inverse shear.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EllipticPdes.Extension.chartExtGrad {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : EuclideanSpace ℝ (Fin d) → ℝ

Gradient of the extension across a C¹ boundary chart. The second term is the shear's own contribution, with the sign of the inverse chart.

Equations

• One or more equations did not get rendered due to their size.

theorem EllipticPdes.Extension.partialD_neg {d : ℕ} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (k : Fin d) (y : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD k (fun (z : EuclideanSpace ℝ (Fin d)) => -γ z) y = -Sobolev.partialD k γ y

The partial derivative of a negated chart.

theorem EllipticPdes.Extension.hasWeakGradOn_chartExt {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : ContDiff ℝ 1 γ) (hind : IndepCoord j γ) {M : ℝ} (hγb : ∀ (k : Fin d) (y : EuclideanSpace ℝ (Fin d)), ‖Sobolev.partialD k γ y‖ ≤ M) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.IntegrableOn u (aboveGraph j γ) MeasureTheory.volume) (hgi : ∀ (k : Fin d), MeasureTheory.IntegrableOn (g k) (aboveGraph j γ) MeasureTheory.volume) (hwg : Embedding.HasWeakGradOn (aboveGraph j γ) u g) : Embedding.HasWeakGradOn Set.univ (chartExt j γ u) (chartExtGrad j γ g)

Weak gradient of the extension across a C¹ boundary chart, on the whole space. The class travels through the shear onto the half space, the reflection extends it across the interface, and the inverse shear returns it, each of the three steps supplying its own half of the gradient.

theorem EllipticPdes.Extension.chartExt_eq_of_mem {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hind : IndepCoord j γ) {u : EuclideanSpace ℝ (Fin d) → ℝ} {y : EuclideanSpace ℝ (Fin d)} (hy : y ∈ aboveGraph j γ) : chartExt j γ u y = u y

Agreement of the extension with the class on the region it extends.

theorem EllipticPdes.Extension.eLpNorm_chartExt_le {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Differentiable ℝ γ) (hind : IndepCoord j γ) {p : ENNReal} (hp : 1 ≤ p) {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (aboveGraph j γ))) : MeasureTheory.eLpNorm (chartExt j γ u) p MeasureTheory.volume ≤ 2 * MeasureTheory.eLpNorm u p (MeasureTheory.volume.restrict (aboveGraph j γ))

Bound on the extension in every Lᵖ seminorm. Both shears preserve measure and the reflection doubles, so the extension over the whole space is bounded by twice the seminorm over the region above the graph.

The gradient's bound

theorem EllipticPdes.Extension.measurePreserving_shear_halfSpace {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Differentiable ℝ γ) (hind : IndepCoord j γ) : MeasureTheory.MeasurePreserving (shear j γ) (MeasureTheory.volume.restrict (halfSpace j)) (MeasureTheory.volume.restrict (aboveGraph j γ))

Restriction of the shear to the half space, preserving measure onto the region above the graph.

theorem EllipticPdes.Extension.shearGrad_normal {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Differentiable ℝ γ) (hind : IndepCoord j γ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) : shearGrad j γ g j = fun (x : EuclideanSpace ℝ (Fin d)) => g j (shear j γ x)

Normal component of the gradient through the shear, untouched, the chart having no partial derivative in the direction it is a graph in.

theorem EllipticPdes.Extension.eLpNorm'_mul_bounded_le {d : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} {f h : EuclideanSpace ℝ (Fin d) → ℝ} {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ (x : EuclideanSpace ℝ (Fin d)), ‖h x‖ ≤ C) {p : ℝ} (hp : 0 < p) : MeasureTheory.eLpNorm' (fun (x : EuclideanSpace ℝ (Fin d)) => f x * h x) p μ ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm' f p μ

Scaling of an Lᵖ seminorm by a bounded factor.

theorem EllipticPdes.Extension.eLpNorm_mul_bounded_le {d : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} {f h : EuclideanSpace ℝ (Fin d) → ℝ} {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ (x : EuclideanSpace ℝ (Fin d)), ‖h x‖ ≤ C) {p : ENNReal} (hfh : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin d)) => f x * h x) μ) : MeasureTheory.eLpNorm (fun (x : EuclideanSpace ℝ (Fin d)) => f x * h x) p μ ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm f p μ

Scaling of an Lᵖ seminorm by a bounded factor.

theorem EllipticPdes.Extension.eLpNorm_shearGrad_le {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : ContDiff ℝ 1 γ) (hind : IndepCoord j γ) {M : ℝ} (hM0 : 0 ≤ M) (hγb : ∀ (k : Fin d) (y : EuclideanSpace ℝ (Fin d)), ‖Sobolev.partialD k γ y‖ ≤ M) {p : ENNReal} (hp : 1 ≤ p) {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hgm : ∀ (k : Fin d), MeasureTheory.AEStronglyMeasurable (g k) (MeasureTheory.volume.restrict (aboveGraph j γ))) (k : Fin d) : MeasureTheory.eLpNorm (shearGrad j γ g k) p (MeasureTheory.volume.restrict (halfSpace j)) ≤ MeasureTheory.eLpNorm (g k) p (MeasureTheory.volume.restrict (aboveGraph j γ)) + ENNReal.ofReal M * MeasureTheory.eLpNorm (g j) p (MeasureTheory.volume.restrict (aboveGraph j γ))

Bound on the transported gradient, componentwise. The shear contributes the chart's bound against the normal component.

theorem EllipticPdes.Extension.eLpNorm_chartExtGrad_le {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : ContDiff ℝ 1 γ) (hind : IndepCoord j γ) {M : ℝ} (hM0 : 0 ≤ M) (hγb : ∀ (k : Fin d) (y : EuclideanSpace ℝ (Fin d)), ‖Sobolev.partialD k γ y‖ ≤ M) {p : ENNReal} (hp : 1 ≤ p) {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hgm : ∀ (k : Fin d), MeasureTheory.AEStronglyMeasurable (g k) (MeasureTheory.volume.restrict (aboveGraph j γ))) (k : Fin d) : MeasureTheory.eLpNorm (chartExtGrad j γ g k) p MeasureTheory.volume ≤ 2 * MeasureTheory.eLpNorm (g k) p (MeasureTheory.volume.restrict (aboveGraph j γ)) + 4 * ENNReal.ofReal M * MeasureTheory.eLpNorm (g j) p (MeasureTheory.volume.restrict (aboveGraph j γ))

Bound on the gradient of the extension across a C¹ boundary chart. Each of the three maps plays its part: the shear contributes the chart's bound against the normal component, the reflection doubles, and the inverse shear contributes the bound again.