OAI/LinearAlgebra/MatrixFields/Construction/ComplexRectangularASI.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.coeff_eq_sum_eval line 23
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.coeff line 38
  3. structure OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation line 63
  4. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.normalized line 74
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.polynomial_eq line 78
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.normalized_constant line 82
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.power_polynomial_eq line 88
  8. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.power line 94
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.rank_power line 120
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.rank_normalized_eval line 140
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.borderRankAtMost line 153
  12. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchCount line 195
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchCount_zero line 197
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.le_batchCount_mul line 204
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchCount_le_iff line 212
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchCount_mul_lt line 218
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchCount_pos_iff line 224
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchCount_cast_lt line 230
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchCount_cast_le line 241
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchCount_mul_cast_le line 245
  21. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchRank line 257
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchRank_zero line 261
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchRank_succ line 263
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchRank_succ_le_affine line 266
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.batchRank_pos line 272
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.repeat_batch_ceiling line 285
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.batch_product_ceiling line 290
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_batch_rank_ceiling line 297
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_rank_of_injective line 324
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_rank_of_injective line 336
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_power_rank line 350
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.square_directSum_power_rank line 362
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_fin_one_rank line 370
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_pow_batchRank line 382
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.rpow_omega_le_of_rankAtMost line 405
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.rpow_omega_le_of_rank_growth line 421
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.equalSummand_inequality_of_quadratic_bound line 446
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.equalSummand_inequality line 468
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.equalSummand_inequality_of_polynomialApproximation line 487
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.Tensor.rectangular_rank_of_injective line 523
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.Tensor.rectangular_directSum_rank_of_injective line 539
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.Tensor.rectangular_directSum_power_rank line 559
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.Tensor.rectangular_pow_batchRank line 573
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.Tensor.rectangular_polynomial_power_rank line 597
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.Tensor.rectangular_directSum_cyclic_rank line 606
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.Tensor.rectangular_directSum_rank_lower line 632
  47. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrictPolynomial line 670
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrictPolynomial_coeff line 677
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.restrictPolynomial line 685
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.restrictPolynomial_degree_le line 692
  51. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.ofRankAtMost line 710
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.ofRankAtMost_polynomial line 724
  53. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.restrict line 731
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.restrict_polynomial line 748
  55. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rectangularTagEquiv line 773
  56. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rectangularIndexEquiv line 777
  57. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.matrixMultiplication_directSum_symmetrized_rank line 781
  58. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rectangularPullback line 790
  59. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rectangularProduct line 805
  60. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.rectangularCyclic line 841
  61. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixCoefficients_directSum_of_injective line 853
  62. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixMultiplication_directSum_symmetrized line 871
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.mul_rpow_third_le_of_cube line 928
  64. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.equalRectangular_inequality line 939
  65. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Arithmetic.equalRectangular_inequality_of_polynomialApproximation line 950