OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexWitness.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. structure OAI.MatrixMultiplication.ComplexWitness.FiniteRectangularWitness line 18
  2. abbrev OAI.MatrixMultiplication.ComplexWitness.CurveCoordinate line 34
  3. abbrev OAI.MatrixMultiplication.ComplexWitness.CurveLeaf line 35
  4. def OAI.MatrixMultiplication.ComplexWitness.curveApproximation line 37
  5. theorem OAI.MatrixMultiplication.ComplexWitness.curve_leaf_count line 41
  6. theorem OAI.MatrixMultiplication.ComplexWitness.curve_leaf_coefficient line 44
  7. theorem OAI.MatrixMultiplication.ComplexWitness.curve_support_exhausted line 49
  8. def OAI.MatrixMultiplication.ComplexWitness.curveFiber line 56
  9. def OAI.MatrixMultiplication.ComplexWitness.curveFiberSize line 62
  10. theorem OAI.MatrixMultiplication.ComplexWitness.mem_curveFiber line 64
  11. def OAI.MatrixMultiplication.ComplexWitness.curveFiberEquiv line 76
  12. theorem OAI.MatrixMultiplication.ComplexWitness.curveFiberSize_eq_card line 85
  13. theorem OAI.MatrixMultiplication.ComplexWitness.curveFiberSize_pos line 91
  14. theorem OAI.MatrixMultiplication.ComplexWitness.curve_fiber_histogram line 94
  15. theorem OAI.MatrixMultiplication.ComplexWitness.curve_fiber_values line 101
  16. theorem OAI.MatrixMultiplication.ComplexWitness.sum_curveLeaves_by_X line 106
  17. theorem OAI.MatrixMultiplication.ComplexWitness.sum_curveFiberSizes line 113
  18. abbrev OAI.MatrixMultiplication.ComplexWitness.CurveLabel line 128
  19. def OAI.MatrixMultiplication.ComplexWitness.curveLabels line 130
  20. def OAI.MatrixMultiplication.ComplexWitness.curveFirstSide line 138
  21. def OAI.MatrixMultiplication.ComplexWitness.curveSecondSide line 142
  22. def OAI.MatrixMultiplication.ComplexWitness.curveFirstReader line 146
  23. def OAI.MatrixMultiplication.ComplexWitness.curveSecondReader line 154
  24. theorem OAI.MatrixMultiplication.ComplexWitness.curveFirstReader_readable line 162
  25. theorem OAI.MatrixMultiplication.ComplexWitness.curveSecondReader_readable line 173
  26. theorem OAI.MatrixMultiplication.ComplexWitness.curve_completeRecord_injective line 184
  27. def OAI.MatrixMultiplication.ComplexWitness.encodeCurveX line 193
  28. def OAI.MatrixMultiplication.ComplexWitness.decodeCurveX line 197
  29. theorem OAI.MatrixMultiplication.ComplexWitness.decode_encodeCurveX line 200
  30. theorem OAI.MatrixMultiplication.ComplexWitness.encodeCurveX_injective line 210
  31. theorem OAI.MatrixMultiplication.ComplexWitness.curve_incidentPrefix line 213
  32. theorem OAI.MatrixMultiplication.ComplexWitness.curve_incidentPrefix_eq_iff line 216
  33. theorem OAI.MatrixMultiplication.ComplexWitness.curve_incidentPrefix_entropy line 221
  34. def OAI.MatrixMultiplication.ComplexWitness.curveReaderPair line 237
  35. theorem OAI.MatrixMultiplication.ComplexWitness.curveReaderPair_incident_prefix line 243
  36. theorem OAI.MatrixMultiplication.ComplexWitness.curveIncidentRate_eq_entropy_X line 247
  37. theorem OAI.MatrixMultiplication.ComplexWitness.curveHiddenRate_eq_entropy_sub_X line 255
  38. theorem OAI.MatrixMultiplication.ComplexWitness.exists_finite_score_gt line 262
  39. theorem OAI.MatrixMultiplication.ComplexWitness.omega_lt_of_score_limit line 269