OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/NativeCapacity.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldNativeCapacity.marginal line 23
  2. def OAI.MatrixMultiplication.AllFieldNativeCapacity.pairLaw line 27
  3. def OAI.MatrixMultiplication.AllFieldNativeCapacity.designated line 31
  4. def OAI.MatrixMultiplication.AllFieldNativeCapacity.singletonEntropy line 35
  5. def OAI.MatrixMultiplication.AllFieldNativeCapacity.residualLaw line 40
  6. def OAI.MatrixMultiplication.AllFieldNativeCapacity.groupedEntropy line 47
  7. def OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeCapacity line 52
  8. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeCapacity_first line 58
  9. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeCapacity_sharing line 64
  10. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.residual_entropy_eq_mass_mul line 72
  11. def OAI.MatrixMultiplication.AllFieldNativeCapacity.stageACapacity line 81
  12. def OAI.MatrixMultiplication.AllFieldNativeCapacity.stageBCapacity line 85
  13. def OAI.MatrixMultiplication.AllFieldNativeCapacity.stageCCapacity line 89
  14. def OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeLA line 92
  15. def OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeLB line 95
  16. def OAI.MatrixMultiplication.AllFieldNativeCapacity.interiorPairs line 98
  17. def OAI.MatrixMultiplication.AllFieldNativeCapacity.interiorMass line 102
  18. def OAI.MatrixMultiplication.AllFieldNativeCapacity.interiorEntropy line 104
  19. def OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeT line 107
  20. def OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeB line 109
  21. def OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeHigh line 113
  22. def OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeCstar line 115
  23. def OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeLambda line 117
  24. def OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeLC line 120
  25. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeLC_expansion line 124
  26. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeLC_balanced line 140
  27. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.native_balanced line 145
  28. def OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeBeta line 150
  29. theorem OAI.MatrixMultiplication.AllFieldNativeCapacity.nativeBeta_nonnegative line 153