Weak gradient through a shear

Flattening a C¹ boundary is a shear, and a Sobolev class has to travel through it. The test function travels the other way, and a smooth test function pulled back through a C¹ shear is C¹ and no better, which is the class hasWeakGradOn_contDiffOne integrates by parts against.

One term of the chain rule asks for more. The pull-back multiplies the test function by a partial derivative of the chart, which for a C¹ chart is continuous and no better, so the product sits outside the C¹ class. That factor does not depend on the j-th coordinate, mollification preserves that independence, and a mollified factor is smooth, so the product rule in the j-th direction leaves only the term the weak gradient names. Dominated convergence returns the identity as the mollification shrinks.

Main declarations

• EllipticPdes.Extension.fderiv_eq_of_indepCoord: the derivative of a chart independent of the j-th coordinate is itself independent of it.
• EllipticPdes.Extension.indepCoord_partialD: the same for a partial derivative.
• EllipticPdes.Extension.indepCoord_convolution: mollification preserves that independence.
• EllipticPdes.Extension.integral_mul_indepCoord: the identity of a weak gradient in the j-th direction, against a test function scaled by such a factor.
• EllipticPdes.Extension.hasWeakGradOn_comp_shear: the weak gradient of a class composed with a shear, the transpose of the shear's derivative applied to the gradient.

References

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

Independence of a coordinate, under differentiation and under mollification

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

Independence of the j-th coordinate passes to a partial derivative. Translating along eⱼ leaves the chart alone, so it leaves the derivative alone.

theorem EllipticPdes.Extension.indepCoord_partialD {d : ℕ} {j k : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : Differentiable ℝ γ) (hind : IndepCoord j γ) : IndepCoord j (Sobolev.partialD k γ)

theorem EllipticPdes.Extension.indepCoord_convolution {d : ℕ} {j : Fin d} {c : EuclideanSpace ℝ (Fin d) → ℝ} (hind : IndepCoord j c) (ρ : ContDiffBump 0) : IndepCoord j (MeasureTheory.convolution (ρ.normed MeasureTheory.volume) c (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

Mollification preserves independence of a coordinate. The convolution averages the factor over translations, each of which leaves it alone.

theorem EllipticPdes.Extension.norm_convolution_normed_le_of_bound {d : ℕ} (ρ : ContDiffBump 0) {h : EuclideanSpace ℝ (Fin d) → ℝ} (hc : Continuous h) {M : ℝ} (hM : ∀ (y : EuclideanSpace ℝ (Fin d)), ‖h y‖ ≤ M) (x : EuclideanSpace ℝ (Fin d)) : ‖MeasureTheory.convolution (ρ.normed MeasureTheory.volume) h (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x‖ ≤ M

Bound on a mollification of a bounded factor. The normed bump is a probability density, so the convolution is an average and inherits the bound with no compact support to lean on.

Integration by parts against a scaled test function

theorem EllipticPdes.Extension.integral_mul_indepCoord {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} (hBopen : IsOpen B) {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) {j : Fin d} {c : EuclideanSpace ℝ (Fin d) → ℝ} (hc : Continuous c) (hcind : IndepCoord j c) {M : ℝ} (hcb : ∀ (y : EuclideanSpace ℝ (Fin d)), ‖c y‖ ≤ M) {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hψ : ContDiff ℝ 1 ψ) (hψcs : HasCompactSupport ψ) (hψs : tsupport ψ ⊆ B) : ∫ (x : EuclideanSpace ℝ (Fin d)) in B, u x * (c x * Sobolev.partialD j ψ x) = -∫ (x : EuclideanSpace ℝ (Fin d)) in B, g j x * (c x * ψ x)

Integration by parts against a bounded factor independent of the j-th coordinate. The identity of a weak gradient in the j-th direction survives multiplication of the test function by such a factor, which need only be continuous. Mollification makes the factor smooth and leaves it independent of the j-th coordinate, so the product rule contributes nothing beyond the term the identity names, and dominated convergence takes the mollification away.

The weak gradient of a composition with a shear

theorem EllipticPdes.Extension.hasWeakGradOn_comp_shear {d : ℕ} {B : Set (EuclideanSpace ℝ (Fin d))} (hBopen : IsOpen B) {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) {j : Fin d} {γ : EuclideanSpace ℝ (Fin d) → ℝ} (hγ : ContDiff ℝ 1 γ) (hind : IndepCoord j γ) {M : ℝ} (hγb : ∀ (k : Fin d) (y : EuclideanSpace ℝ (Fin d)), ‖Sobolev.partialD k γ y‖ ≤ M) : Embedding.HasWeakGradOn (shear j γ ⁻¹' B) (fun (y : EuclideanSpace ℝ (Fin d)) => u (shear j γ y)) fun (k : Fin d) (y : EuclideanSpace ℝ (Fin d)) => g k (shear j γ y) + g j (shear j γ y) * Sobolev.partialD k γ y

Weak gradient through a shear. If u has weak gradient g on B, then u ∘ S has weak gradient k ↦ gₖ ∘ S + (g_j ∘ S) ∂ₖγ on the preimage of B, which is the transpose of the shear's derivative applied to the gradient.

A smooth test function pulled back through the inverse shear is C¹, and the chain rule splits the identity in two. The first half is the weak gradient tested against that pull-back. The second has the chart's k-th partial as a factor on the test function, and that factor is independent of the j-th coordinate, which is what integral_mul_indepCoord asks of it.