OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteFrameDifferentiation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Differentiability of a finite-dimensional frame

  1. theorem OAI.PolycyclicRecognition.differentiableAt_clm_of_apply line 17

    Source documentation

    A finite basis makes pointwise differentiability sufficient for an operator-valued frame.

    theorem differentiableAt_clm_of_apply {A : X → E →L[ℝ] F} {x : X}
    (hA : ∀ v : E, DifferentiableAt ℝ (fun z => A z v) x) :
    DifferentiableAt ℝ A x := by
…
  2. theorem OAI.PolycyclicRecognition.differentiableAt_chartInvariantFrame line 41