Shear of a C¹ boundary chart

A bounded domain with C¹ boundary is, near a boundary point and after relabelling the coordinates, the region above the graph of a C¹ function γ of the remaining coordinates. The map that flattens the boundary is the shear y ↦ y + γ(y) • eⱼ, whose inverse is the shear by -γ, and whose derivative is the identity plus a rank-one map that annihilates its own direction. Its determinant is therefore 1, so it preserves Lebesgue measure and the change of variables leaves every integral unchanged.

Main declarations

• EllipticPdes.Extension.shear: the map.
• EllipticPdes.Extension.shear_shear_neg: the shear by -γ inverts it.
• EllipticPdes.Extension.det_shearDeriv: the derivative has determinant 1.
• EllipticPdes.Extension.integral_comp_shear: the change of variables.
• EllipticPdes.Extension.shearHomeomorph: the shear as a homeomorphism of the whole space.
• EllipticPdes.Extension.measurePreserving_shear: the shear preserves Lebesgue measure.
• EllipticPdes.Extension.partialD_comp_shear: the chain rule through a shear.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.4, and §C.1 for the boundary chart.

noncomputable def EllipticPdes.Extension.shear {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) (y : EuclideanSpace ℝ (Fin d)) : EuclideanSpace ℝ (Fin d)

Shear of a boundary chart. The point y moves along the j-th axis by γ y.

Equations

• EllipticPdes.Extension.shear j γ y = y + γ y • EuclideanSpace.single j 1

def EllipticPdes.Extension.IndepCoord {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) : Prop

γ does not depend on the j-th coordinate, which is what makes the shear invertible by a shear and its derivative nilpotent.

Equations

• EllipticPdes.Extension.IndepCoord j γ = ∀ (y : EuclideanSpace ℝ (Fin d)) (t : ℝ), γ (y + t • EuclideanSpace.single j 1) = γ y

theorem EllipticPdes.Extension.shear_shear_neg {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hind : IndepCoord j γ) (y : EuclideanSpace ℝ (Fin d)) : shear j (fun (z : EuclideanSpace ℝ (Fin d)) => -γ z) (shear j γ y) = y

Inversion of the shear by γ.

theorem EllipticPdes.Extension.shear_neg_shear {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hind : IndepCoord j γ) (y : EuclideanSpace ℝ (Fin d)) : shear j γ (shear j (fun (z : EuclideanSpace ℝ (Fin d)) => -γ z) y) = y

Inversion of the shear by -γ.

theorem EllipticPdes.Extension.bijective_shear {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hind : IndepCoord j γ) : Function.Bijective (shear j γ)

The shear is a bijection of the whole space.

theorem EllipticPdes.Extension.partialD_eq_zero_of_indepCoord {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Differentiable ℝ γ) (hind : IndepCoord j γ) (y : EuclideanSpace ℝ (Fin d)) : (fderiv ℝ γ y) (EuclideanSpace.single j 1) = 0

Vanishing j-th partial of a function independent of that coordinate.

noncomputable def EllipticPdes.Extension.shearDeriv {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) (y : EuclideanSpace ℝ (Fin d)) : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)

The derivative of the shear: the identity plus a rank-one map in the direction eⱼ.

Equations

• EllipticPdes.Extension.shearDeriv j γ y = ContinuousLinearMap.id ℝ (EuclideanSpace ℝ (Fin d)) + (fderiv ℝ γ y).smulRight (EuclideanSpace.single j 1)

theorem EllipticPdes.Extension.hasFDerivAt_shear {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Differentiable ℝ γ) (y : EuclideanSpace ℝ (Fin d)) : HasFDerivAt (shear j γ) (shearDeriv j γ y) y

Derivative of the shear.

theorem EllipticPdes.Extension.det_shearDeriv {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Differentiable ℝ γ) (hind : IndepCoord j γ) (y : EuclideanSpace ℝ (Fin d)) : (shearDeriv j γ y).det = 1

Determinant 1 of the shear derivative. In the standard basis the matrix is the identity with row j replaced by eⱼ + ∇γ. Multilinearity in that row splits the determinant into det 1 and the determinant of the identity with row j replaced by ∇γ, and the latter reads off as the j-th component of ∇γ, which vanishes.

theorem EllipticPdes.Extension.integral_comp_shear {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Differentiable ℝ γ) (hind : IndepCoord j γ) (g : EuclideanSpace ℝ (Fin d) → ℝ) : ∫ (y : EuclideanSpace ℝ (Fin d)), g (shear j γ y) = ∫ (x : EuclideanSpace ℝ (Fin d)), g x

Change of variables through a shear. The Jacobian determinant is 1, so the shear leaves every integral unchanged.

The shear as a homeomorphism, and its measure

theorem EllipticPdes.Extension.continuous_shear {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Continuous γ) : Continuous (shear j γ)

The shear is continuous when the chart is.

theorem EllipticPdes.Extension.contDiff_shear {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} {n : ℕ∞} (hγ : ContDiff ℝ (↑n) γ) : ContDiff ℝ (↑n) (shear j γ)

The shear is C^n when the chart is.

theorem EllipticPdes.Extension.IndepCoord.neg {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hind : IndepCoord j γ) : IndepCoord j fun (z : EuclideanSpace ℝ (Fin d)) => -γ z

Negating a chart preserves independence of the j-th coordinate.

noncomputable def EllipticPdes.Extension.shearHomeomorph {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Continuous γ) (hind : IndepCoord j γ) : EuclideanSpace ℝ (Fin d) ≃ₜ EuclideanSpace ℝ (Fin d)

Shear as a homeomorphism of the whole space, inverted by the shear by -γ.

Equations

• One or more equations did not get rendered due to their size.

theorem EllipticPdes.Extension.measurableEmbedding_shear {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Continuous γ) (hind : IndepCoord j γ) : MeasurableEmbedding (shear j γ)

The shear is a measurable embedding, being a homeomorphism.

theorem EllipticPdes.Extension.measurePreserving_shear {d : ℕ} {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Differentiable ℝ γ) (hind : IndepCoord j γ) : MeasureTheory.MeasurePreserving (shear j γ) MeasureTheory.volume MeasureTheory.volume

Preservation of Lebesgue measure by a shear. Its inverse is the shear by -γ, whose derivative has determinant 1, so the image of a measurable set has the measure of the set.

The chain rule through a shear

theorem EllipticPdes.Extension.partialD_comp_shear {d : ℕ} {j : Fin d} {γ φ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Differentiable ℝ γ) (hφ : Differentiable ℝ φ) (k : Fin d) (y : EuclideanSpace ℝ (Fin d)) : Sobolev.partialD k (fun (z : EuclideanSpace ℝ (Fin d)) => φ (shear j γ z)) y = Sobolev.partialD k φ (shear j γ y) + Sobolev.partialD j φ (shear j γ y) * Sobolev.partialD k γ y

Partial derivatives through a shear. The derivative of the shear is the identity plus a rank-one map in the direction eⱼ, so a partial derivative of a composition adds to the corresponding partial of the outer function the j-th one times the partial of the chart.