OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/NativeGroupedRates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.singletonResidualGroup_transport line 25
  2. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.singletonResidual_groupedEntropy_reindex line 34
  3. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.right_conditional_sum_eq line 49
  4. def OAI.MatrixMultiplication.AllFieldNativeGroupedRates.supportSubtypeEquiv line 63
  5. def OAI.MatrixMultiplication.AllFieldNativeGroupedRates.supportIndexEquiv line 71
  6. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.supportIndexEquiv_get line 76
  7. def OAI.MatrixMultiplication.AllFieldNativeGroupedRates.boundedComplement line 83
  8. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.boundedComplement_involutive line 89
  9. def OAI.MatrixMultiplication.AllFieldNativeGroupedRates.boundedComplementEquiv line 96
  10. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.native_right_conditional_sum_eq line 106
  11. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.native_two_conditional_sums_eq line 168
  12. def OAI.MatrixMultiplication.AllFieldNativeGroupedRates.twoHalfConditionalCost line 198
  13. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.stageA_twoHalfConditionalCost_eq line 212
  14. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.stageB_twoHalfConditionalCost_eq line 242
  15. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.stageA_twoHalfConditionalCost_eq_entropy_sub_capacity line 271
  16. theorem OAI.MatrixMultiplication.AllFieldNativeGroupedRates.stageB_twoHalfConditionalCost_eq_entropy_sub_capacity line 281