OAI/Analysis/TracialSplitting/OrthogonalPacking.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.projection_orthogonal_of_le_complement line 17
  2. structure OAI.CurrentMain.ProjectionInsertion line 23
  3. lemma OAI.CurrentMain.ProjectionInsertion.monotone line 38
  4. lemma OAI.CurrentMain.ProjectionInsertion.inserted_le_next line 44
  5. lemma OAI.CurrentMain.ProjectionInsertion.inserted_occupied_orthogonal line 48
  6. lemma OAI.CurrentMain.ProjectionInsertion.orthogonal line 52
  7. lemma OAI.CurrentMain.ProjectionInsertion.final_eq line 64
  8. lemma OAI.CurrentMain.ProjectionInsertion.initial_orthogonal line 79
  9. lemma OAI.CurrentMain.exists_projection_insertion line 92
  10. structure OAI.CurrentMain.PackingStepBounds line 133
  11. lemma OAI.CurrentMain.re_difference_le_of_complex line 155
  12. lemma OAI.CurrentMain.exists_packing_step line 160
  13. structure OAI.CurrentMain.SampledPackingRound line 208
  14. lemma OAI.CurrentMain.exists_sampled_packing_round line 225
  15. lemma OAI.CurrentMain.signed_weighted_sum line 267
  16. def OAI.CurrentMain.SampledPackingRound.sampledMass line 282
  17. def OAI.CurrentMain.SampledPackingRound.targetMass line 284
  18. def OAI.CurrentMain.SampledPackingRound.overlap line 287
  19. def OAI.CurrentMain.SampledPackingRound.totalError line 290
  20. lemma OAI.CurrentMain.SampledPackingRound.sampledMass_nonneg line 292
  21. lemma OAI.CurrentMain.SampledPackingRound.overlap_nonneg line 295
  22. lemma OAI.CurrentMain.SampledPackingRound.sampledMass_error line 300
  23. lemma OAI.CurrentMain.SampledPackingRound.totalError_nonneg line 311
  24. lemma OAI.CurrentMain.SampledPackingRound.insertedMass_bounds line 314
  25. lemma OAI.CurrentMain.SampledPackingRound.initial_le_final line 328
  26. lemma OAI.CurrentMain.SampledPackingRound.overlap_le_target line 332
  27. lemma OAI.CurrentMain.SampledPackingRound.sampled_linear_sum line 350
  28. lemma OAI.CurrentMain.SampledPackingRound.sampled_energy_sum line 361
  29. lemma OAI.CurrentMain.SampledPackingRound.inserted_energy_sum line 372