Cutting a class off inside a boundary chart

Guo's Theorem III.2.2 finishes by covering the boundary with finitely many chart neighbourhoods and gluing the local extensions with a partition of unity. Each piece of that partition is a cutoff supported in one chart's ball, and the piece it cuts out has to reach the whole region above that chart's graph, where the chart describes the domain only inside the ball.

That is what this file supplies. A cutoff supported in W sends a weak gradient on B ∩ W to a weak gradient on all of B, since a test function on B multiplied by the cutoff is a test function on B ∩ W, and every integrand the identity names vanishes off W along with the cutoff. hasWeakGradOn_univ_mul_cutoff is the case W ⊆ B, where the conclusion reaches the whole space; here the cutoff straddles the boundary of B, which is what a boundary chart does.

Main declarations

• EllipticPdes.Extension.integrableOn_of_vanishing_off: integrability spreads from the part of a set inside a neighbourhood when the class vanishes outside it.
• EllipticPdes.Extension.hasWeakGradOn_mul_cutoff_inter: the weak gradient of a class cut off inside a neighbourhood, on the surrounding set.

References

James Guo, Partial Differential Equations (Course Lecture Notes), Theorem III.2.2 (p. 20), proof step 3 (p. 21); L. C. Evans, Partial Differential Equations (2nd ed.), §5.4 Theorem 1 (p. 253).

theorem EllipticPdes.Extension.integrableOn_of_vanishing_off {d : ℕ} {B W : Set (EuclideanSpace ℝ (Fin d))} (hB : MeasurableSet B) (hW : MeasurableSet W) {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : MeasureTheory.IntegrableOn f (B ∩ W) MeasureTheory.volume) (hoff : ∀ x ∉ W, f x = 0) : MeasureTheory.IntegrableOn f B MeasureTheory.volume

Integrability from a neighbourhood the class vanishes outside. A class integrable on the part of a set inside W and vanishing off W is integrable on the whole set, the rest of it contributing nothing.

theorem EllipticPdes.Extension.hasWeakGradOn_mul_cutoff_inter {d : ℕ} {B W : Set (EuclideanSpace ℝ (Fin d))} (hB : MeasurableSet B) {η : EuclideanSpace ℝ (Fin d) → ℝ} (hηc : ContDiff ℝ (↑⊤) η) (hηs : tsupport η ⊆ W) {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.IntegrableOn u (B ∩ W) MeasureTheory.volume) (hgi : ∀ (k : Fin d), MeasureTheory.IntegrableOn (g k) (B ∩ W) MeasureTheory.volume) (h : Embedding.HasWeakGradOn (B ∩ W) u g) : Embedding.HasWeakGradOn B (fun (x : EuclideanSpace ℝ (Fin d)) => η x * u x) fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => η x * g k x + Sobolev.partialD k η x * u x

Weak gradient of a class cut off inside a neighbourhood. If u has weak gradient g on B ∩ W and η is smooth with tsupport η ⊆ W, then η u has weak gradient η gₖ + u ∂ₖη on all of B. Testing against φ reduces to testing the hypothesis against η φ, whose support sits inside B ∩ W, and both sides of the identity see only W, the cutoff and its derivative vanishing off it.