OAI/AlgebraicGeometry/Seshadri/Interpolation/CompressionRanks.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MaximalSeshadri.Interpolation.JetIndex line 10
  2. def OAI.MaximalSeshadri.Interpolation.finiteJetColumn line 12
  3. theorem OAI.MaximalSeshadri.Interpolation.finite_jet_rank_persistence line 18
  4. theorem OAI.MaximalSeshadri.Interpolation.contDiff_iteratedDeriv_parameter line 30
  5. theorem OAI.MaximalSeshadri.Interpolation.compression_row_smooth line 44
  6. theorem OAI.MaximalSeshadri.Interpolation.compression_row_derivative_limit line 48
  7. theorem OAI.MaximalSeshadri.Interpolation.mixed_deriv_separated line 59
  8. theorem OAI.MaximalSeshadri.Interpolation.compression_mixed_derivative_limit line 65
  9. theorem OAI.MaximalSeshadri.Interpolation.compression_finite_rank line 72
  10. theorem OAI.MaximalSeshadri.Interpolation.linearIndependent_of_span_le line 86
  11. theorem OAI.MaximalSeshadri.Interpolation.iteratedDeriv_polynomial line 96
  12. def OAI.MaximalSeshadri.Interpolation.polynomialJetMap line 109
  13. theorem OAI.MaximalSeshadri.Interpolation.polynomialJetMap_eq line 117
  14. theorem OAI.MaximalSeshadri.Interpolation.polynomial_image_mem_span line 127
  15. def OAI.MaximalSeshadri.Interpolation.compressionRowMap line 142
  16. theorem OAI.MaximalSeshadri.Interpolation.compressionRowMap_pow line 150
  17. theorem OAI.MaximalSeshadri.Interpolation.compressionRowMap_inverse line 154
  18. theorem OAI.MaximalSeshadri.Interpolation.compression_inverse_degree line 165