OAI/Analysis/JiangSu/DimensionDrop/DimensionDropRelations.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectComparison.comparison_dimension_drop_relations line 25
  2. lemma OAI.DimensionDropRelations.matrixUnit_mul_general line 73
  3. structure OAI.DimensionDropRelations.Witness line 80
  4. def OAI.DimensionDropRelations.Witness.column line 94
  5. def OAI.DimensionDropRelations.Witness.rangeMass line 95
  6. def OAI.DimensionDropRelations.Witness.parameter line 96
  7. lemma OAI.DimensionDropRelations.Witness.h_nonneg line 98
  8. lemma OAI.DimensionDropRelations.Witness.h_le_one line 99
  9. lemma OAI.DimensionDropRelations.Witness.h_commute line 103
  10. lemma OAI.DimensionDropRelations.Witness.h_support line 106
  11. lemma OAI.DimensionDropRelations.Witness.E_support line 109
  12. lemma OAI.DimensionDropRelations.Witness.s_square line 110
  13. lemma OAI.DimensionDropRelations.Witness.column_star line 113
  14. lemma OAI.DimensionDropRelations.Witness.matrix_column line 115
  15. lemma OAI.DimensionDropRelations.Witness.h_column line 121
  16. lemma OAI.DimensionDropRelations.Witness.E_column line 123
  17. lemma OAI.DimensionDropRelations.Witness.column_inner line 125
  18. lemma OAI.DimensionDropRelations.Witness.column_s line 134
  19. lemma OAI.DimensionDropRelations.Witness.column_star_s line 136
  20. lemma OAI.DimensionDropRelations.Witness.mass_nonneg line 139
  21. lemma OAI.DimensionDropRelations.Witness.mass_star line 140
  22. lemma OAI.DimensionDropRelations.Witness.h_mass line 141
  23. lemma OAI.DimensionDropRelations.Witness.mass_h line 143
  24. lemma OAI.DimensionDropRelations.Witness.mass_s line 146
  25. lemma OAI.DimensionDropRelations.Witness.s_mass line 150
  26. lemma OAI.DimensionDropRelations.Witness.parameter_s line 155
  27. lemma OAI.DimensionDropRelations.Witness.mass_matrix line 159
  28. lemma OAI.DimensionDropRelations.Witness.matrix_mass line 165
  29. lemma OAI.DimensionDropRelations.Witness.parameter_matrix line 168
  30. lemma OAI.DimensionDropRelations.Witness.mass_column line 178
  31. lemma OAI.DimensionDropRelations.Witness.mass_sq line 181
  32. lemma OAI.DimensionDropRelations.Witness.mass_sq_le line 184
  33. lemma OAI.DimensionDropRelations.Witness.mass_le_one line 190
  34. lemma OAI.DimensionDropRelations.Witness.parameter_nonneg line 197
  35. lemma OAI.DimensionDropRelations.Witness.parameter_le_one line 202
  36. lemma OAI.DimensionDropRelations.Witness.parameter_star line 203
  37. lemma OAI.DimensionDropRelations.Witness.E_mass line 204
  38. lemma OAI.DimensionDropRelations.Witness.parameter_h line 205
  39. lemma OAI.DimensionDropRelations.Witness.parameter_equation line 206