OAI/LinearAlgebra/MatrixFields/Extraction/GroupPairWindows.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.exists_pos_le_family_inline_MatrixMultiplication_JointCompatibilityControls line 22
  2. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.residualBase line 45
  3. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.designatedBase line 48
  4. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.totalCenterCount line 51
  5. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.residualCenter line 55
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.residualBase_mul_center line 62
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.residualCenter_nonneg line 79
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.residualCenter_le_one line 88
  9. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.groupCenter line 102
  10. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.groupCap line 108
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.groupCap_nonneg line 114
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.exists_group_entropy_window_inline_MatrixMultiplication_JointCompatibilityControls line 129
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.residual_card_repeated line 148
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.repeated_mixture_balance line 162
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.repeated_residual_width_le_inline_MatrixMultiplication_JointCompatibilityControls line 181
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.exists_uniform_sideEntropyControl line 211
  17. def OAI.MatrixAllFields.MatrixMultiplication.JointCompatibilityControls.control_mono_width line 264
  18. def OAI.MatrixAllFields.MatrixMultiplication.JointPairMixtureControls.pairMixture line 319
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPairMixtureControls.sum_first_fiber line 325
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPairMixtureControls.sum_second_fiber line 335
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPairMixtureControls.base_eq_zero_of_size_eq_zero line 345
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPairMixtureControls.totalCenterCount_eq_zero_of_size_eq_zero line 352
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPairMixtureControls.pairMixture_left_balance line 360
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPairMixtureControls.pairMixture_right_balance line 385
  25. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.base line 435
  26. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.q line 439
  27. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.Positions line 445
  28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.pairCounts line 450
  29. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.parentBase line 457
  30. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.parentPair line 460
  31. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.classMass line 466
  32. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.windowFactor line 470
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.windowFactor_pos line 473
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.parentBase_pos line 478
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.parent_positions_card line 482
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.positions_card line 490
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.parentPair_eq_parentCenter line 504
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.parentPair_eq_native line 519
  39. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.parentStatistic line 533
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.parent_window line 539
  41. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.weightCode line 573
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.weightCode_val line 579
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.weightCode_statistic line 583
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.left_supported_zero line 588
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.filtered_pair_sum line 603
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.q_eq_conditionalCenter line 641
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.classMass_pos line 656
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.fiber_mass line 662
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.width_le line 676
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.sharing_window line 699
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.q_eq_one_of_subsingleton line 727
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.pairWindow_of_completeKeep line 763
  53. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupPairWindows.passing_pairWindow line 796