OAI/LinearAlgebra/MatrixFields/Construction/GroupAmbientDegree.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitCoordinateWeight line 18
  2. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitPotential line 22
  3. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitNormalizer line 26
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitLogNormalizer line 29
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitCoordinateWeight_pos line 32
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitNormalizer_pos line 38
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitWeight_log line 44
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitLaw_log line 53
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitLaw_positive_iff line 69
  10. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.physicalPotential line 80
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitLaw_log_physical line 84
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_positive_has_branch line 100
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageA_branch_log line 112
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageB_branch_log line 127
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageA_log line 142
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageB_log line 152
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.mem_shapes_of_total line 162
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.mem_below_iff line 174
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.splitShape_exhaustive line 185
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.branchShape_exhaustive line 200
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageA_positive line 232
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldActiveGibbs.placedLaw_stageB_positive line 242
  23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.distinguishedSide line 261
  24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.coordinateMass line 264
  25. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.physicalPotential line 269
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.distinguishedSide_branch line 273
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.placedLaw_stageC_branch_mass line 280
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.placedLaw_stageC_mass_of_positive line 297
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.placedLaw_stageC_mass_on_feasible line 304
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.sum_physicalPotential line 312
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.placedLaw_stageC_log line 318
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.placedLaw_positive_parent_bounds line 327
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.jointCounts_positive_reference line 335
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldStageCGibbs.localAllowed_positive_reference line 344
  35. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAmbientDegree.potential line 380
  36. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAmbientDegree.logNormalizer line 388
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAmbientDegree.placedLaw_log line 396
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAmbientDegree.localAllowed_positive line 407
  39. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAmbientDegree.orderTotal line 436
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAmbientDegree.canonicalLaw_mass_eq line 438
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAmbientDegree.localAllowed_entropy_le line 452
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAmbientDegree.tendsto_firstExponent line 474
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupAmbientDegree.eventually_sharedAmbient_first_card_le line 504