Half space and its interface

The extension of a Sobolev class across a flat boundary is by reflection, and what has to be proved is that the reflected class has a weak gradient across the interface. The identity of a weak gradient on the open half space applies only to test functions supported strictly inside it, so the test function is first multiplied by slabCut j ε and the slab is then let shrink.

Two terms survive the product rule. The one with the cutoff's own derivative vanishes identically in the directions along the interface, since the cutoff depends on the j-th coordinate alone. In the remaining direction it is the boundary term, and it vanishes in the limit whenever the test function vanishes on the interface, which is exactly what the odd part of a reflection does.

Main declarations

• EllipticPdes.Extension.halfSpace: the open half space {xⱼ > 0}.
• EllipticPdes.Extension.volume_interface: the interface is null.
• EllipticPdes.Extension.integral_partialD_of_ne: no boundary term along the interface.
• EllipticPdes.Extension.integral_partialD_of_eq: none in the remaining direction either, for a test function vanishing on the interface.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.4 Theorem 1.

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

Open half space above the interface {xⱼ = 0}.

Equations

• EllipticPdes.Extension.halfSpace j = {x : EuclideanSpace ℝ (Fin d) | 0 < x.ofLp j}

theorem EllipticPdes.Extension.isOpen_halfSpace {d : ℕ} (j : Fin d) : IsOpen (halfSpace j)

theorem EllipticPdes.Extension.measurableSet_halfSpace {d : ℕ} (j : Fin d) : MeasurableSet (halfSpace j)

theorem EllipticPdes.Extension.volume_interface {d : ℕ} (j : Fin d) : MeasureTheory.volume {x : EuclideanSpace ℝ (Fin d) | x.ofLp j = 0} = 0

Nullity of the interface, being a proper linear subspace.

theorem EllipticPdes.Extension.preimage_reflectLI_halfSpace {d : ℕ} (j : Fin d) : ⇑(reflectLI j) ⁻¹' halfSpace j = {x : EuclideanSpace ℝ (Fin d) | x.ofLp j < 0}

The reflection sends the half space onto the other side.

No boundary term

theorem EllipticPdes.Extension.abs_le_of_vanishes_on_interface {d : ℕ} {j : Fin d} {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hψ : Differentiable ℝ ψ) {M : ℝ} (hM : ∀ (z : EuclideanSpace ℝ (Fin d)), ‖fderiv ℝ ψ z‖ ≤ M) (hzero : ∀ (z : EuclideanSpace ℝ (Fin d)), z.ofLp j = 0 → ψ z = 0) (x : EuclideanSpace ℝ (Fin d)) (hx : 0 ≤ x.ofLp j) : |ψ x| ≤ M * x.ofLp j

C¹ class vanishing on the interface is bounded by its gradient and the distance to it. This is what makes the boundary term vanish in the limit.

theorem EllipticPdes.Extension.integral_partialD_of_ne {d : ℕ} {j : Fin d} {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} {ψ : EuclideanSpace ℝ (Fin d) → ℝ} {k : Fin d} (hk : k ≠ j) (hu : MeasureTheory.IntegrableOn u (halfSpace j) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn (g k) (halfSpace j) MeasureTheory.volume) (hwg : Embedding.HasWeakGradOn (halfSpace j) u g) (hψ : ContDiff ℝ (↑⊤) ψ) (hψcs : HasCompactSupport ψ) : ∫ (x : EuclideanSpace ℝ (Fin d)) in halfSpace j, u x * Sobolev.partialD k ψ x = -∫ (x : EuclideanSpace ℝ (Fin d)) in halfSpace j, g k x * ψ x

No boundary term along the interface. The cutoff depends on the j-th coordinate alone, so in every other direction its derivative vanishes and the identity passes to a test function that need not vanish near the interface.

theorem EllipticPdes.Extension.integral_partialD_of_eq {d : ℕ} {j : Fin d} {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.IntegrableOn u (halfSpace j) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn (g j) (halfSpace j) MeasureTheory.volume) (hwg : Embedding.HasWeakGradOn (halfSpace j) u g) (hψ : ContDiff ℝ (↑⊤) ψ) (hψcs : HasCompactSupport ψ) (hzero : ∀ (z : EuclideanSpace ℝ (Fin d)), z.ofLp j = 0 → ψ z = 0) : ∫ (x : EuclideanSpace ℝ (Fin d)) in halfSpace j, u x * Sobolev.partialD j ψ x = -∫ (x : EuclideanSpace ℝ (Fin d)) in halfSpace j, g j x * ψ x

No boundary term in the remaining direction either, for a test function vanishing on the interface. Where the cutoff's derivative is C/ε the test function is at most 2ε times its gradient, so the product is bounded uniformly and supported in a slab that shrinks to nothing.