Differentiation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ArnoldCounterexample.CriticalBound.contDiff_multilinear_apply line 15

Source documentation

Smooth evaluation including all moving vector arguments.

theorem contDiff_multilinear_apply {E : Type uE} {F : Type uF} {G : Type uG}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [NormedAddCommGroup G] [NormedSpace ℝ G]
    {k : ℕ∞ω} {n : ℕ} {f : E → F [×n]→L[ℝ] G}
    (hf : ContDiff ℝ k f) {v : Fin n → E → F} (hv : ∀ i, ContDiff ℝ k (v i)) :
    ContDiff ℝ k (fun x ↦ f x (v · x)) := by
…

theorem OAI.ArnoldCounterexample.CriticalBound.contDiff_alternating_apply line 34
abbrev OAI.ArnoldCounterexample.CriticalBound.MatForm line 50
Source documentation
Matrix forms use the topology of the chosen operator norm. The orthogonal group retains its original (definitionally distinct) product topology.
```
abbrev MatForm (n : ℕ) := by
…
```
lemma OAI.ArnoldCounterexample.CriticalBound.fderiv_rightMul line 55
lemma OAI.ArnoldCounterexample.CriticalBound.lieBracket_rightMul line 60
theorem OAI.ArnoldCounterexample.CriticalBound.integral_extDeriv_rightMul_eq_zero line 71
Source documentation
Haar--Stokes on horizontal tuples of left-invariant fields. The bracket hypothesis is basicness in the vertical directions; it is purely a pointwise algebraic condition, not a Stokes or nonexactness assumption.
```
theorem integral_extDeriv_rightMul_eq_zero {n : ℕ}
    (W : RM → MatForm (n + 1)) (hW : ContDiff ℝ ∞ W)
    (X : Fin (n + 2) → RM) (hX : ∀ i, star (X i) = -X i)
    (hvertical : ∀ (A : O5) (i j : Fin (n + 1)),
      W A (Matrix.vecCons ((A : RM) * (X i.castSucc * X j.succ - X j.succ * X i.castSucc))
        (j.removeNth (i.castSucc.removeNth (fun k ↦ (A : RM) * X k)))) = 0) :
    ∫ A : O5, extDeriv W (A : RM) (fun i ↦ (A : RM) * X i) ∂haar = 0 := by
…
```
Mentions: OAI.ArnoldCounterexample.CriticalBound.RM, OAI.ArnoldCounterexample.CriticalBound.MatForm, OAI.ArnoldCounterexample.CriticalBound.O5, OAI.ArnoldCounterexample.CriticalBound.haar