OAI/Analysis/Mahler/PullbackRegularity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerStokes.contDiffAt_of_toMultilinear line 14
2. theorem OAI.MahlerStokes.contDiffAt_compAlternating line 36

   Source documentation

   The pullback operation is C1 jointly in the form and the linear map. It is polynomial in the linear map, so C1 regularity needs no extra premise.

   theorem contDiffAt_compAlternating {d n : ℕ} {X : Type*}
       [NormedAddCommGroup X] [NormedSpace ℝ X]
       {f : X → (Fin d → ℝ) [⋀^Fin n]→L[ℝ] ℝ}
       {L : X → (Fin d → ℝ) →L[ℝ] (Fin d → ℝ)} {x : X}
       (hf : ContDiffAt ℝ 1 f x) (hL : ContDiffAt ℝ 1 L x) :
       ContDiffAt ℝ 1 (fun y => (f y).compContinuousLinearMap (L y)) x := by
   …

3. theorem OAI.MahlerStokes.contDiffAt_pullbackForm line 56

   Source documentation

   A C2 parametrization and C1 ambient form give a C1 actual pullback.

   theorem contDiffAt_pullbackForm {d n : ℕ}
       {φ : (Fin d → ℝ) → (Fin d → ℝ)}
       {ω : (Fin d → ℝ) → (Fin d → ℝ) [⋀^Fin n]→L[ℝ] ℝ} {x : Fin d → ℝ}
       (hφ : ContDiffAt ℝ 2 φ x) (hω : ContDiffAt ℝ 1 ω (φ x)) :
       ContDiffAt ℝ 1 (pullbackForm φ ω) x := by
   …

   Mentions: OAI.MahlerStokes.pullbackForm