OAI/Analysis/Mahler/ChartExtension.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerStokes.extendedChartForm line 13

   Source documentation

   The oriented pullback, extended by zero outside the actual chart target.

   def extendedChartForm {d n : ℕ}
       (e : OpenPartialHomeomorph (Fin d → ℝ) (Fin d → ℝ))
       (ω : (Fin d → ℝ) → (Fin d → ℝ) [⋀^Fin n]→L[ℝ] ℝ) :
       (Fin d → ℝ) → (Fin d → ℝ) [⋀^Fin n]→L[ℝ] ℝ :=
   …

2. theorem OAI.MahlerStokes.chart_inverse_det_ne_zero line 20
3. theorem OAI.MahlerStokes.tsupport_extendedChartForm line 42
4. theorem OAI.MahlerStokes.hasCompactSupport_extendedChartForm line 63
5. theorem OAI.MahlerStokes.extendedChartForm_eventuallyEq line 71
6. theorem OAI.MahlerStokes.contDiff_extendedChartForm line 86

   Source documentation

   Compact support inside the chart makes extension by zero C1. This proves the pullback regularity rather than adding it as a Stokes hypothesis.

   theorem contDiff_extendedChartForm {d n : ℕ}
       (e : OpenPartialHomeomorph (Fin d → ℝ) (Fin d → ℝ))
       (ω : (Fin d → ℝ) → (Fin d → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (he : ContDiffOn ℝ 2 e e.source) (hi : ContDiffOn ℝ 2 e.symm e.target)
       (hω : ContDiff ℝ 1 ω) (hc : HasCompactSupport ω) (hs : tsupport ω ⊆ e.source) :
       ContDiff ℝ 1 (extendedChartForm e ω) := by
   …

   Mentions: OAI.MahlerStokes.extendedChartForm

7. theorem OAI.MahlerStokes.extDeriv_extendedChartForm line 112

   Source documentation

   On the target, the derivative of the oriented extension is the oriented pullback of the derivative. The orientation is locally constant.

   theorem extDeriv_extendedChartForm {d n : ℕ}
       (e : OpenPartialHomeomorph (Fin d → ℝ) (Fin d → ℝ))
       (ω : (Fin d → ℝ) → (Fin d → ℝ) [⋀^Fin n]→L[ℝ] ℝ) {y : Fin d → ℝ}
       (hy : y ∈ e.target) (hi : ContDiffAt ℝ 2 e.symm y)
       (hdet : (fderiv ℝ e.symm y).det ≠ 0) (hω : DifferentiableAt ℝ ω (e.symm y)) :
       extDeriv (extendedChartForm e ω) y =
         jacobianOrientation (fderiv ℝ e.symm y).det •
           (extDeriv ω (e.symm y)).compContinuousLinearMap (fderiv ℝ e.symm y) := by
   …

   Mentions: OAI.MahlerStokes.extendedChartForm, OAI.MahlerStokes.jacobianOrientation