OAI/LinearAlgebra/MatrixFields/Parameters/NativeCapacity.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.marginal line 20
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.pairLaw line 24
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.designated line 28
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.singletonEntropy line 32
  5. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.residualLaw line 37
  6. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.groupedEntropy line 44
  7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeCapacity line 49
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeCapacity_first line 55
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeCapacity_sharing line 61
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.residual_entropy_eq_mass_mul line 69
  11. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageACapacity line 78
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageBCapacity line 82
  13. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.stageCCapacity line 86
  14. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeLA line 89
  15. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeLB line 92
  16. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.interiorPairs line 95
  17. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.interiorMass line 99
  18. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.interiorEntropy line 101
  19. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeT line 104
  20. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeB line 106
  21. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeHigh line 110
  22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeCstar line 112
  23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeLambda line 114
  24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeLC line 117
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeLC_expansion line 121
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeLC_balanced line 137
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.native_balanced line 142
  28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeBeta line 147
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldNativeCapacity.nativeBeta_nonnegative line 150