OAI/Algebra/Determinantal/SchurDifferentials.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differentiableAt_right line 11
  2. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differentiableAt_left line 20
  3. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differentiableAt_scalar line 29
  4. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differential_mulVec line 42
  5. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differential_scalar line 65
  6. def OAI.PermanentBorder.PolarAnalysis.Schur.auxiliaryLinear line 125
  7. theorem OAI.PermanentBorder.PolarAnalysis.Schur.auxiliaryLinear_apply line 131
  8. theorem OAI.PermanentBorder.PolarAnalysis.Schur.auxiliaryLinear_invertible line 134
  9. def OAI.PermanentBorder.PolarAnalysis.Schur.auxiliary line 149
  10. def OAI.PermanentBorder.PolarAnalysis.Schur.graphKernels line 153
  11. theorem OAI.PermanentBorder.PolarAnalysis.Schur.auxiliary_solved line 158
  12. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differentiableAt_graphKernels line 165
  13. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differentiableAt_auxiliary line 175
  14. theorem OAI.PermanentBorder.PolarAnalysis.Schur.fderiv_auxiliary_inr line 200
  15. theorem OAI.PermanentBorder.PolarAnalysis.Schur.simple_kernel_elimination line 213
  16. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differential_det_block line 240
  17. theorem OAI.PermanentBorder.PolarAnalysis.Schur.contDiff_det line 265
  18. theorem OAI.PermanentBorder.PolarAnalysis.Schur.contDiff_adjugate line 272
  19. theorem OAI.PermanentBorder.PolarAnalysis.Schur.contDiffAt_inverse line 284
  20. theorem OAI.PermanentBorder.PolarAnalysis.Schur.contDiffAt_scalar line 291
  21. theorem OAI.PermanentBorder.PolarAnalysis.simple_unit_multiplier_iff line 310
  22. def OAI.PermanentBorder.PolarAnalysis.triangularMultiplier line 319
  23. theorem OAI.PermanentBorder.PolarAnalysis.triangularMultiplier_apply line 323
  24. theorem OAI.PermanentBorder.PolarAnalysis.triangularMultiplier_invertible line 327
  25. theorem OAI.PermanentBorder.PolarAnalysis.differentiableAt_triangularMultiplier line 334
  26. theorem OAI.PermanentBorder.PolarAnalysis.simple_triangular_system_iff line 342
  27. def OAI.PermanentBorder.PolarAnalysis.polarPair line 362
  28. theorem OAI.PermanentBorder.PolarAnalysis.differentiableAt_polarPair line 365
  29. theorem OAI.PermanentBorder.PolarAnalysis.simple_polarPair_unit line 376