OAI/Analysis/JiangSu/Comparison/PackingRounds.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DirectPacking.PackingStepBounds line 14
  2. lemma OAI.DirectPacking.re_difference_le_of_complex line 36
  3. lemma OAI.DirectPacking.exists_packing_step line 41
  4. structure OAI.DirectPacking.SampledPackingRound line 88
  5. lemma OAI.DirectPacking.exists_sampled_packing_round line 105
  6. lemma OAI.DirectPacking.signed_weighted_sum line 145
  7. def OAI.DirectPacking.SampledPackingRound.sampledMass line 158
  8. def OAI.DirectPacking.SampledPackingRound.targetMass line 159
  9. def OAI.DirectPacking.SampledPackingRound.overlap line 161
  10. def OAI.DirectPacking.SampledPackingRound.totalError line 164
  11. lemma OAI.DirectPacking.SampledPackingRound.sampledMass_nonneg line 166
  12. lemma OAI.DirectPacking.SampledPackingRound.overlap_nonneg line 169
  13. lemma OAI.DirectPacking.SampledPackingRound.sampledMass_error line 173
  14. lemma OAI.DirectPacking.SampledPackingRound.totalError_nonneg line 183
  15. lemma OAI.DirectPacking.SampledPackingRound.insertedMass_bounds line 185
  16. lemma OAI.DirectPacking.SampledPackingRound.initial_le_final line 199
  17. lemma OAI.DirectPacking.SampledPackingRound.overlap_le_target line 203
  18. lemma OAI.DirectPacking.SampledPackingRound.sampled_linear_sum line 220
  19. lemma OAI.DirectPacking.SampledPackingRound.sampled_energy_sum line 230
  20. lemma OAI.DirectPacking.SampledPackingRound.inserted_energy_sum line 241
  21. lemma OAI.DirectPacking.trace_mass_difference_abs_le line 265
  22. lemma OAI.DirectPacking.trace_projected_mass_perturb line 274
  23. lemma OAI.DirectPacking.WeightedBlockFamily.trace_weightedSum line 285
  24. lemma OAI.DirectPacking.WeightedBlockFamily.trace_mul_weightedSum line 290
  25. lemma OAI.DirectPacking.SampledPackingRound.targetMass_eq line 301
  26. structure OAI.DirectPacking.SampledPackingRound.Estimates line 305
  27. lemma OAI.DirectPacking.SampledPackingRound.estimates_of_average line 319
  28. lemma OAI.DirectPacking.projection_finset_sum line 392
  29. lemma OAI.DirectPacking.signed_sum line 412
  30. lemma OAI.DirectPacking.paired_sum_norm_sub_le line 416
  31. def OAI.DirectPacking.SampledPackingRound.signSum line 430
  32. lemma OAI.DirectPacking.SampledPackingRound.signSum_projection line 432
  33. lemma OAI.DirectPacking.SampledPackingRound.signSum_orthogonal line 436
  34. lemma OAI.DirectPacking.SampledPackingRound.initial_signSum_orthogonal line 444
  35. lemma OAI.DirectPacking.SampledPackingRound.subinitial_signSum_orthogonal line 448
  36. lemma OAI.DirectPacking.SampledPackingRound.final_eq_signSum line 454
  37. lemma OAI.DirectPacking.SampledPackingRound.signSum_energy line 458
  38. lemma OAI.DirectPacking.SampledPackingRound.displacement_sum_le line 468
  39. lemma OAI.DirectPacking.SampledPackingRound.signSum_balance line 492
  40. lemma OAI.DirectPacking.SampledPackingRound.Estimates.balance line 528
  41. structure OAI.DirectPacking.OrthogonalProjectionPair line 551
  42. def OAI.DirectPacking.OrthogonalProjectionPair.total line 560
  43. def OAI.DirectPacking.OrthogonalProjectionPair.energy line 561
  44. def OAI.DirectPacking.OrthogonalProjectionPair.balance line 563
  45. def OAI.DirectPacking.OrthogonalProjectionPair.remaining line 565
  46. lemma OAI.DirectPacking.OrthogonalProjectionPair.total_projection line 568
  47. lemma OAI.DirectPacking.OrthogonalProjectionPair.left_le_total line 572
  48. lemma OAI.DirectPacking.OrthogonalProjectionPair.right_le_total line 574
  49. lemma OAI.DirectPacking.OrthogonalProjectionPair.total_energy_le line 576
  50. lemma OAI.DirectPacking.OrthogonalProjectionPair.energy_nonneg line 580
  51. lemma OAI.DirectPacking.OrthogonalProjectionPair.right_signSum_orthogonal line 586
  52. lemma OAI.DirectPacking.OrthogonalProjectionPair.left_signSum_orthogonal line 589
  53. lemma OAI.DirectPacking.OrthogonalProjectionPair.signSum_right_orthogonal line 592
  54. def OAI.DirectPacking.OrthogonalProjectionPair.appendRound line 597
  55. lemma OAI.DirectPacking.OrthogonalProjectionPair.appendRound_total line 606
  56. lemma OAI.DirectPacking.OrthogonalProjectionPair.appendRound_energy line 611
  57. lemma OAI.DirectPacking.OrthogonalProjectionPair.appendRound_balance line 622