Reflection in a coordinate hyperplane

Reflecting the j-th coordinate is the first step of the extension operator: a function on a half-ball is continued across the flat piece of its boundary by composing with the reflection, and the higher-order reflection that matches the normal derivative is a combination of two such composites.

This file records what the reflection does to the three things the weak formulation sees. It is a linear isometry, so it preserves Lebesgue measure and is a measurable embedding; it sends the k-th partial derivative to ± the k-th partial derivative of the composite, with the sign negative exactly at k = j; and it therefore sends a weak gradient on a set to a weak gradient on the preimage of that set, with the same signs.

Nothing here asks anything of the set, which is what makes it usable both on a half-ball and on the image of one under a boundary chart.

Main declarations

• EllipticPdes.Extension.reflectLI: the reflection, as a linear isometry equivalence.
• EllipticPdes.Extension.partialD_comp_reflect: the partial derivatives of a reflected function.
• EllipticPdes.Extension.hasWeakGradOn_comp_reflect: the weak gradient of a reflected function.
• EllipticPdes.Extension.eLpNorm_comp_reflect: reflection preserves every Lᵖ seminorm.

References

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

The reflection

def EllipticPdes.Extension.reflectSign {d : ℕ} (j k : Fin d) : ℝ

The sign the reflection in the j-th coordinate hyperplane attaches to the k-th coordinate: negative exactly when the two agree.

Equations

• EllipticPdes.Extension.reflectSign j k = if k = j then -1 else 1

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

theorem EllipticPdes.Extension.reflectSign_ne_zero {d : ℕ} (j k : Fin d) : reflectSign j k ≠ 0

noncomputable def EllipticPdes.Extension.reflectLI {d : ℕ} (j : Fin d) : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)

Reflection in the j-th coordinate hyperplane, as a linear isometry equivalence of Euclidean space.

Equations

• EllipticPdes.Extension.reflectLI j = LinearIsometryEquiv.piLpCongrRight 2 fun (k : Fin d) => if k = j then LinearIsometryEquiv.neg ℝ else LinearIsometryEquiv.refl ℝ ℝ

@[simp]

theorem EllipticPdes.Extension.reflectLI_apply {d : ℕ} (j : Fin d) (x : EuclideanSpace ℝ (Fin d)) (k : Fin d) : ((reflectLI j) x).ofLp k = reflectSign j k * x.ofLp k

@[simp]

theorem EllipticPdes.Extension.reflectLI_involutive {d : ℕ} (j : Fin d) (x : EuclideanSpace ℝ (Fin d)) : (reflectLI j) ((reflectLI j) x) = x

theorem EllipticPdes.Extension.reflectLI_preimage_preimage {d : ℕ} (j : Fin d) (B : Set (EuclideanSpace ℝ (Fin d))) : ⇑(reflectLI j) ⁻¹' ⇑(reflectLI j) ⁻¹' B = B

theorem EllipticPdes.Extension.measurePreserving_reflectLI {d : ℕ} (j : Fin d) : MeasureTheory.MeasurePreserving (⇑(reflectLI j)) MeasureTheory.volume MeasureTheory.volume

theorem EllipticPdes.Extension.measurableEmbedding_reflectLI {d : ℕ} (j : Fin d) : MeasurableEmbedding ⇑(reflectLI j)

Derivatives and supports

theorem EllipticPdes.Extension.partialD_comp_reflect {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : Differentiable ℝ φ) (j k : Fin d) (x : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD k (fun (y : EuclideanSpace ℝ (Fin d)) => φ ((reflectLI j) y)) x = reflectSign j k * Sobolev.partialD k φ ((reflectLI j) x)

Partial derivatives of a reflected function.

theorem EllipticPdes.Extension.contDiff_comp_reflect {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (j : Fin d) : ContDiff ℝ ↑⊤ fun (y : EuclideanSpace ℝ (Fin d)) => φ ((reflectLI j) y)

theorem EllipticPdes.Extension.hasCompactSupport_comp_reflect {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : HasCompactSupport φ) (j : Fin d) : HasCompactSupport fun (y : EuclideanSpace ℝ (Fin d)) => φ ((reflectLI j) y)

theorem EllipticPdes.Extension.tsupport_comp_reflect_subset {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} {B : Set (EuclideanSpace ℝ (Fin d))} (j : Fin d) (h : tsupport φ ⊆ ⇑(reflectLI j) ⁻¹' B) : (tsupport fun (y : EuclideanSpace ℝ (Fin d)) => φ ((reflectLI j) y)) ⊆ B

The weak gradient of a reflected function

theorem EllipticPdes.Extension.hasWeakGradOn_comp_reflect {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (h : Embedding.HasWeakGradOn B u g) (j : Fin d) : Embedding.HasWeakGradOn (⇑(reflectLI j) ⁻¹' B) (fun (y : EuclideanSpace ℝ (Fin d)) => u ((reflectLI j) y)) fun (k : Fin d) (y : EuclideanSpace ℝ (Fin d)) => reflectSign j k * g k ((reflectLI j) y)

Reflection of a weak gradient. If u has weak gradient g on B, then u ∘ Rⱼ has weak gradient k ↦ ±(gₖ ∘ Rⱼ) on the preimage of B, with the sign negative exactly at k = j.

The proof is the change of variables under a measure-preserving involution, twice: once to move the test function onto B, where the hypothesis applies, and once to move the conclusion back.

theorem EllipticPdes.Extension.eLpNorm_comp_reflect {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (j : Fin d) (p : ENNReal) : MeasureTheory.eLpNorm (fun (y : EuclideanSpace ℝ (Fin d)) => f ((reflectLI j) y)) p MeasureTheory.volume = MeasureTheory.eLpNorm f p MeasureTheory.volume

Reflection preserves every Lᵖ seminorm, the reflection being measure preserving. This is what makes the bound on an extension by reflection a bound with no loss.