Linearity of the chart extension

Evans states the extension as a bounded linear operator, where Guo's proof produces an extension for each class. The three maps the chart extension runs on are all precomposition or multiplication by a fixed function, so the extension is linear in the class once the chart and its graph are fixed. This file records that.

Each statement is written with an explicit lambda on both sides rather than Pi.add, because the shear and the reflection are applied to the function argument and a goal written with Pi.add does not match one written with a lambda.

Main declarations

• EllipticPdes.Extension.evenExt_add and evenExt_smul: the even reflection is linear.
• EllipticPdes.Extension.evenExtGrad_add and evenExtGrad_smul: so is its gradient.
• EllipticPdes.Extension.shearGrad_add and shearGrad_smul: so is the shear's gradient.
• EllipticPdes.Extension.chartExt_add and chartExt_smul: so is the chart extension.
• EllipticPdes.Extension.chartExtGrad_add and chartExtGrad_smul: so is its gradient.

References

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

The even reflection

theorem EllipticPdes.Extension.evenExt_add {d : ℕ} (j : Fin d) (u v : EuclideanSpace ℝ (Fin d) → ℝ) : (evenExt j fun (x : EuclideanSpace ℝ (Fin d)) => u x + v x) = fun (x : EuclideanSpace ℝ (Fin d)) => evenExt j u x + evenExt j v x

The even reflection is additive in the class.

theorem EllipticPdes.Extension.evenExt_smul {d : ℕ} (j : Fin d) (c : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ) : (evenExt j fun (x : EuclideanSpace ℝ (Fin d)) => c * u x) = fun (x : EuclideanSpace ℝ (Fin d)) => c * evenExt j u x

The even reflection commutes with a scalar.

theorem EllipticPdes.Extension.evenExtGrad_add {d : ℕ} (j : Fin d) (g h : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : evenExtGrad j (fun (i : Fin d) (x : EuclideanSpace ℝ (Fin d)) => g i x + h i x) k = fun (x : EuclideanSpace ℝ (Fin d)) => evenExtGrad j g k x + evenExtGrad j h k x

The reflected gradient is additive in the gradient.

theorem EllipticPdes.Extension.evenExtGrad_smul {d : ℕ} (j : Fin d) (c : ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : evenExtGrad j (fun (i : Fin d) (x : EuclideanSpace ℝ (Fin d)) => c * g i x) k = fun (x : EuclideanSpace ℝ (Fin d)) => c * evenExtGrad j g k x

The reflected gradient commutes with a scalar.

The shear

theorem EllipticPdes.Extension.shearGrad_add {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) (g h : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) : (shearGrad j γ fun (i : Fin d) (x : EuclideanSpace ℝ (Fin d)) => g i x + h i x) = fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => shearGrad j γ g k x + shearGrad j γ h k x

The shear's gradient is additive in the gradient. The statement is at the family, not at one of its components, because the reflection takes the whole family as its argument.

theorem EllipticPdes.Extension.shearGrad_smul {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) (c : ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) : (shearGrad j γ fun (i : Fin d) (x : EuclideanSpace ℝ (Fin d)) => c * g i x) = fun (k : Fin d) (x : EuclideanSpace ℝ (Fin d)) => c * shearGrad j γ g k x

The shear's gradient commutes with a scalar.

The chart extension

theorem EllipticPdes.Extension.chartExt_add {d : ℕ} (j : Fin d) (γ u v : EuclideanSpace ℝ (Fin d) → ℝ) : (chartExt j γ fun (x : EuclideanSpace ℝ (Fin d)) => u x + v x) = fun (y : EuclideanSpace ℝ (Fin d)) => chartExt j γ u y + chartExt j γ v y

Chart extension is additive in the class.

theorem EllipticPdes.Extension.chartExt_smul {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) (c : ℝ) (u : EuclideanSpace ℝ (Fin d) → ℝ) : (chartExt j γ fun (x : EuclideanSpace ℝ (Fin d)) => c * u x) = fun (y : EuclideanSpace ℝ (Fin d)) => c * chartExt j γ u y

Chart extension commutes with a scalar.

theorem EllipticPdes.Extension.chartExtGrad_add {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) (g h : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : chartExtGrad j γ (fun (i : Fin d) (x : EuclideanSpace ℝ (Fin d)) => g i x + h i x) k = fun (y : EuclideanSpace ℝ (Fin d)) => chartExtGrad j γ g k y + chartExtGrad j γ h k y

Gradient of the chart extension is additive in the gradient.

theorem EllipticPdes.Extension.chartExtGrad_smul {d : ℕ} (j : Fin d) (γ : EuclideanSpace ℝ (Fin d) → ℝ) (c : ℝ) (g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) (k : Fin d) : chartExtGrad j γ (fun (i : Fin d) (x : EuclideanSpace ℝ (Fin d)) => c * g i x) k = fun (y : EuclideanSpace ℝ (Fin d)) => c * chartExtGrad j γ g k y

Gradient of the chart extension commutes with a scalar.