OAI/Analysis/TracialSplitting/ProjectionRounding.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.projection_family_orthogonal line 22
  2. lemma OAI.CurrentMain.collect_max_piece line 42
  3. theorem OAI.CurrentMain.comparison_sorted_partition line 96
  4. theorem OAI.CurrentMain.full_projection_partition line 142
  5. def OAI.CurrentMain.roundCoeff line 173
  6. def OAI.CurrentMain.roundDeficit line 175
  7. lemma OAI.CurrentMain.roundCoeff_zero_or_one line 177
  8. lemma OAI.CurrentMain.roundDeficit_bounds line 191
  9. lemma OAI.CurrentMain.roundDeficit_zero line 198
  10. lemma OAI.CurrentMain.roundCoeff_sub line 200
  11. lemma OAI.CurrentMain.weighted_differences_bounds line 206
  12. lemma OAI.CurrentMain.floor_weighted_rounding line 235
  13. lemma OAI.CurrentMain.orthogonal_projection_sum line 280
  14. lemma OAI.CurrentMain.trace_projection_real line 299
  15. lemma OAI.CurrentMain.trace_projection_le_one line 303
  16. theorem OAI.CurrentMain.proportional_projection_bound line 309
  17. theorem OAI.CurrentMain.uniform_proportional_subprojection line 347
  18. lemma OAI.CurrentMain.proportional_subprojection line 365