Extension across a flat boundary by reflection

A Sobolev class on the half space extends across the interface by reflecting it: the value at a point below the interface is the value at its mirror image. The gradient extends the same way, with a sign in the normal direction, and the extended pair is a weak gradient on the whole space.

The identity is tested against an arbitrary test function of the whole space. Splitting the integral at the interface and reflecting the lower half turns it into an integral over the half space, tested against φ + s (φ ∘ R) with s the sign of the direction. In the normal direction that combination is odd, so it vanishes on the interface, which is exactly the hypothesis under which the boundary term of EllipticPdes.Extension.integral_partialD_of_eq disappears.

Main declarations

• EllipticPdes.Extension.evenExt: the reflected extension of a function.
• EllipticPdes.Extension.evenExtGrad: the reflected extension of its gradient.
• EllipticPdes.Extension.integral_split_interface: an integral splits at the interface.
• EllipticPdes.Extension.hasWeakGradOn_evenExt: the weak gradient of the extension.
• EllipticPdes.Extension.eLpNorm_evenExt_le: its bound in every Lᵖ seminorm.
• EllipticPdes.Extension.aestronglyMeasurable_evenExt: the extension is measurable.
• EllipticPdes.Extension.eLpNorm_evenExtGrad_le: the gradient's bound in every Lᵖ seminorm.
• EllipticPdes.Extension.integrable_evenExt and EllipticPdes.Extension.integrable_evenExtGrad: the extension and its gradient are integrable on the whole space whenever the class is integrable on the half space.

References

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

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

The open half space below the interface.

Equations

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

theorem EllipticPdes.Extension.measurableSet_halfSpaceNeg {d : ℕ} (j : Fin d) : MeasurableSet (halfSpaceNeg j)

theorem EllipticPdes.Extension.disjoint_halfSpace {d : ℕ} (j : Fin d) : Disjoint (halfSpace j) (halfSpaceNeg j)

theorem EllipticPdes.Extension.univ_ae_eq_union {d : ℕ} (j : Fin d) : Set.univ =ᵐ[MeasureTheory.volume] halfSpace j ∪ halfSpaceNeg j

Up to the null interface, the whole space is the union of the two open half spaces.

theorem EllipticPdes.Extension.integral_split_interface {d : ℕ} {j : Fin d} {f : EuclideanSpace ℝ (Fin d) → ℝ} (h1 : MeasureTheory.IntegrableOn f (halfSpace j) MeasureTheory.volume) (h2 : MeasureTheory.IntegrableOn f (halfSpaceNeg j) MeasureTheory.volume) : ∫ (x : EuclideanSpace ℝ (Fin d)), f x = (∫ (x : EuclideanSpace ℝ (Fin d)) in halfSpace j, f x) + ∫ (x : EuclideanSpace ℝ (Fin d)) in halfSpaceNeg j, f x

Splitting of an integral over the whole space at the interface.

The reflected extension

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

Reflected extension of a function: below the interface it takes the value at the mirror image.

Equations

• EllipticPdes.Extension.evenExt j u x = if 0 ≤ x.ofLp j then u x else u ((EllipticPdes.Extension.reflectLI j) x)

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

Reflected extension of a gradient, with a sign in the normal direction.

Equations

• EllipticPdes.Extension.evenExtGrad j g k x = if 0 ≤ x.ofLp j then g k x else EllipticPdes.Extension.reflectSign j k * g k ((EllipticPdes.Extension.reflectLI j) x)

theorem EllipticPdes.Extension.preimage_reflectLI_halfSpaceNeg {d : ℕ} (j : Fin d) : ⇑(reflectLI j) ⁻¹' halfSpaceNeg j = halfSpace j

theorem EllipticPdes.Extension.setIntegral_halfSpaceNeg {d : ℕ} (j : Fin d) (f : EuclideanSpace ℝ (Fin d) → ℝ) : ∫ (x : EuclideanSpace ℝ (Fin d)) in halfSpaceNeg j, f x = ∫ (y : EuclideanSpace ℝ (Fin d)) in halfSpace j, f ((reflectLI j) y)

Integral over the lower half space as the reflected integral over the upper one.

theorem EllipticPdes.Extension.partialD_add {d : ℕ} {f h : EuclideanSpace ℝ (Fin d) → ℝ} (k : Fin d) {x : EuclideanSpace ℝ (Fin d)} (hf : DifferentiableAt ℝ f x) (hh : DifferentiableAt ℝ h x) : Sobolev.partialD k (fun (y : EuclideanSpace ℝ (Fin d)) => f y + h y) x = Sobolev.partialD k f x + Sobolev.partialD k h x

The partial derivative is additive.

theorem EllipticPdes.Extension.partialD_const_mul {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (k : Fin d) (c : ℝ) {x : EuclideanSpace ℝ (Fin d)} (hf : DifferentiableAt ℝ f x) : Sobolev.partialD k (fun (y : EuclideanSpace ℝ (Fin d)) => c * f y) x = c * Sobolev.partialD k f x

The partial derivative commutes with a constant multiple.

theorem EllipticPdes.Extension.reflectLI_eq_self_of_interface {d : ℕ} {j : Fin d} {x : EuclideanSpace ℝ (Fin d)} (hx : x.ofLp j = 0) : (reflectLI j) x = x

The reflection fixes the interface.

theorem EllipticPdes.Extension.hasWeakGradOn_evenExt {d : ℕ} {j : Fin d} {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.IntegrableOn u (halfSpace j) MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.IntegrableOn (g k) (halfSpace j) MeasureTheory.volume) (hwg : Embedding.HasWeakGradOn (halfSpace j) u g) : Embedding.HasWeakGradOn Set.univ (evenExt j u) (evenExtGrad j g)

Weak gradient of the reflected extension on the whole space. Splitting the integral at the interface and reflecting the lower half tests the class against φ + s (φ ∘ R), which in the normal direction is odd and so vanishes on the interface. That is the hypothesis under which no boundary term survives.

The bound

theorem EllipticPdes.Extension.evenExt_ae_eq {d : ℕ} (j : Fin d) (u : EuclideanSpace ℝ (Fin d) → ℝ) : evenExt j u =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ (Fin d)) => (halfSpace j).indicator u x + (halfSpaceNeg j).indicator (fun (y : EuclideanSpace ℝ (Fin d)) => u ((reflectLI j) y)) x

The extension is, almost everywhere, the sum of the class and its reflection, each on its own side of the interface.

theorem EllipticPdes.Extension.measurePreserving_reflectLI_halfSpaceNeg {d : ℕ} (j : Fin d) : MeasureTheory.MeasurePreserving (⇑(reflectLI j)) (MeasureTheory.volume.restrict (halfSpaceNeg j)) (MeasureTheory.volume.restrict (halfSpace j))

Reflection of the lower half space onto the upper one, preserving measure.

theorem EllipticPdes.Extension.eLpNorm_evenExt_le {d : ℕ} {j : Fin d} {u : EuclideanSpace ℝ (Fin d) → ℝ} {p : ENNReal} (hp : 1 ≤ p) (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (halfSpace j))) : MeasureTheory.eLpNorm (evenExt j u) p MeasureTheory.volume ≤ 2 * MeasureTheory.eLpNorm u p (MeasureTheory.volume.restrict (halfSpace j))

Bound for the extension in every Lᵖ seminorm. The reflection preserves measure, so each side contributes the seminorm on the half space.

Integrability of the extension

theorem EllipticPdes.Extension.evenExtGrad_ae_eq {d : ℕ} (j : Fin d) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : evenExtGrad j g k =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ (Fin d)) => (halfSpace j).indicator (g k) x + (halfSpaceNeg j).indicator (fun (y : EuclideanSpace ℝ (Fin d)) => reflectSign j k * g k ((reflectLI j) y)) x

The extended gradient is, almost everywhere, the sum of the component and its signed reflection, each on its own side of the interface.

theorem EllipticPdes.Extension.aestronglyMeasurable_evenExt {d : ℕ} {j : Fin d} {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (halfSpace j))) : MeasureTheory.AEStronglyMeasurable (evenExt j u) MeasureTheory.volume

Measurability of the reflected extension, from the description of it as a sum of two indicators.

theorem EllipticPdes.Extension.integrable_evenExt {d : ℕ} {j : Fin d} {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.IntegrableOn u (halfSpace j) MeasureTheory.volume) : MeasureTheory.Integrable (evenExt j u) MeasureTheory.volume

Integrability of the reflected extension. Each side of the interface contributes the integral over the half space, the reflection preserving measure.

theorem EllipticPdes.Extension.integrable_evenExtGrad {d : ℕ} {j : Fin d} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (k : Fin d) (hg : MeasureTheory.IntegrableOn (g k) (halfSpace j) MeasureTheory.volume) : MeasureTheory.Integrable (evenExtGrad j g k) MeasureTheory.volume

Integrability of the extended gradient, componentwise.

The gradient's bound

theorem EllipticPdes.Extension.abs_reflectSign {d : ℕ} (j k : Fin d) : |reflectSign j k| = 1

The sign a reflection attaches to a direction has absolute value 1.

theorem EllipticPdes.Extension.aestronglyMeasurable_evenExtGrad {d : ℕ} {j : Fin d} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (k : Fin d) (hg : MeasureTheory.AEStronglyMeasurable (g k) (MeasureTheory.volume.restrict (halfSpace j))) : MeasureTheory.AEStronglyMeasurable (evenExtGrad j g k) MeasureTheory.volume

Measurability of the extended gradient, componentwise.

theorem EllipticPdes.Extension.eLpNorm_evenExtGrad_le {d : ℕ} {j : Fin d} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (k : Fin d) {p : ENNReal} (hp : 1 ≤ p) (hg : MeasureTheory.AEStronglyMeasurable (g k) (MeasureTheory.volume.restrict (halfSpace j))) : MeasureTheory.eLpNorm (evenExtGrad j g k) p MeasureTheory.volume ≤ 2 * MeasureTheory.eLpNorm (g k) p (MeasureTheory.volume.restrict (halfSpace j))

Bound on the extended gradient in every Lᵖ seminorm. The reflection preserves measure and the sign has absolute value 1, so each side contributes the seminorm on the half space.