Rigid motion of a boundary chart

A boundary chart relabels and reorients the coordinate axes before reading the domain off a graph, and that relabelling and reorientation is a linear isometry of the whole space. This file moves a weak gradient through one.

A linear isometry is its own derivative, so the chain rule sends the gradient to its transpose applied to the gradient, which in coordinates is the sum over the directions the isometry sends the k-th one to. The reflection of Extension/Reflect.lean is the case where that sum has a single term and a sign; the general case needs the sum, and the finite sum has to travel through an integral, which is where the integrability hypotheses enter.

Main declarations

• EllipticPdes.Extension.clm_apply_eq_sum: a continuous linear functional is the sum of its values on the standard directions.
• EllipticPdes.Extension.partialD_comp_linearIsometry: the chain rule through an isometry.
• EllipticPdes.Extension.hasWeakGradOn_comp_linearIsometry: the weak gradient through an isometry.
• EllipticPdes.Extension.eLpNorm_grad_comp_linearIsometry_le: its Lᵖ seminorm, bounded by the sum over the components the isometry mixes.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §C.1 (p. 665), where the relabelling and reorientation of the axes appears; James Guo, Partial Differential Equations (Course Lecture Notes), Theorem III.2.2 (p. 20).

theorem EllipticPdes.Extension.sum_smul_single {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) : ∑ i : Fin d, v.ofLp i • EuclideanSpace.single i 1 = v

A vector is the sum of its coordinates against the standard directions.

theorem EllipticPdes.Extension.clm_apply_eq_sum {d : ℕ} (T : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (v : EuclideanSpace ℝ (Fin d)) : T v = ∑ i : Fin d, v.ofLp i * T (EuclideanSpace.single i 1)

A continuous linear functional is the sum of its values on the standard directions.

theorem EllipticPdes.Extension.partialD_comp_linearIsometry {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : Differentiable ℝ φ) (e : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)) (k : Fin d) (y : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD k (fun (z : EuclideanSpace ℝ (Fin d)) => φ (e z)) y = ∑ i : Fin d, (e (EuclideanSpace.single k 1)).ofLp i * Sobolev.partialD i φ (e y)

Partial derivatives through a linear isometry.

theorem EllipticPdes.Extension.hasWeakGradOn_comp_linearIsometry {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.IntegrableOn u B MeasureTheory.volume) (hgi : ∀ (k : Fin d), MeasureTheory.IntegrableOn (g k) B MeasureTheory.volume) (hwg : Embedding.HasWeakGradOn B u g) (e : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)) : Embedding.HasWeakGradOn (⇑e ⁻¹' B) (fun (y : EuclideanSpace ℝ (Fin d)) => u (e y)) fun (k : Fin d) (y : EuclideanSpace ℝ (Fin d)) => ∑ i : Fin d, (e (EuclideanSpace.single k 1)).ofLp i * g i (e y)

Weak gradient through a linear isometry. The isometry is its own derivative, so the gradient transforms by its transpose, which in coordinates is the sum over the directions the isometry sends the k-th one to.

The gradient's seminorm

theorem EllipticPdes.Extension.abs_coord_le_norm {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) (i : Fin d) : |v.ofLp i| ≤ ‖v‖

A coordinate of a vector is bounded by its norm.

theorem EllipticPdes.Extension.eLpNorm_grad_comp_linearIsometry_le {d : ℕ} {p : ENNReal} (hp : 1 ≤ p) {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hgm : ∀ (i : Fin d), MeasureTheory.AEStronglyMeasurable (g i) MeasureTheory.volume) (e : EuclideanSpace ℝ (Fin d) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin d)) (k : Fin d) : MeasureTheory.eLpNorm (fun (y : EuclideanSpace ℝ (Fin d)) => ∑ i : Fin d, (e (EuclideanSpace.single k 1)).ofLp i * g i (e y)) p MeasureTheory.volume ≤ ∑ i : Fin d, MeasureTheory.eLpNorm (g i) p MeasureTheory.volume

Seminorm of the gradient through a linear isometry. Each coordinate of the image of a unit direction is at most one, so the transported component is bounded by the sum of the components it mixes.