RawReindexedDerivative.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.rawFrontFin line 13
Source documentation
The derivative slot is numbered zero; all old slots follow in order.
```
def rawFrontFin (n : ℕ) : Fin 1 ⊕ Fin n ≃ Fin (n+1) :=
…
```
lemma OAI.Mahler.rawFrontFin_inl line 16
lemma OAI.Mahler.rawFrontFin_inr line 21
def OAI.Mahler.rawReindexDerivative line 26
lemma OAI.Mahler.HasRawFDerivAt.reindex line 34
lemma OAI.Mahler.rawPrefix_uncurry_reindex line 43

theorem OAI.Mahler.extDeriv_of_reindexed_raw line 57

Source documentation

Exterior differentiation with an arbitrary explicit ordering of raw slots, retaining the order of the distinguished derivative slot.

theorem extDeriv_of_reindexed_raw {n : ℕ} (e : ι ≃ Fin n)
    {a : E → MultilinearMap ℝ (fun _ : ι => E) ℂ}
    {D : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : ι => E) ℂ}
    {ω : E → E [⋀^Fin n]→L[ℝ] ℂ} {x : E}
    (hω : DifferentiableAt ℝ ω x)
    (heq : ∀ᶠ y in 𝓝 x, (ω y).toAlternatingMap = (a y).alternatization.domDomCongr e)
    (ha : HasRawFDerivAt a D x) :
    (extDeriv ω x).toAlternatingMap = (rawPrefix D).alternatization.domDomCongr
      ((Equiv.sumCongr (Equiv.refl (Fin 1)) e).trans (rawFrontFin n)) := by
…

Mentions: OAI.Mahler.HasRawFDerivAt, OAI.Mahler.rawPrefix, OAI.Mahler.rawFrontFin