OAI/Analysis/TracialSplitting/PackingEstimates.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.trace_mass_difference_abs_le line 17
  2. lemma OAI.CurrentMain.trace_projected_mass_perturb line 26
  3. lemma OAI.CurrentMain.WeightedBlockFamily.trace_weightedSum line 39
  4. lemma OAI.CurrentMain.WeightedBlockFamily.trace_mul_weightedSum line 45
  5. lemma OAI.CurrentMain.SampledPackingRound.targetMass_eq line 60
  6. structure OAI.CurrentMain.SampledPackingRound.Estimates line 64
  7. lemma OAI.CurrentMain.SampledPackingRound.estimates_of_average line 78
  8. lemma OAI.CurrentMain.projection_finset_sum line 151
  9. lemma OAI.CurrentMain.signed_sum line 171
  10. lemma OAI.CurrentMain.paired_sum_norm_sub_le line 175
  11. def OAI.CurrentMain.SampledPackingRound.signSum line 193
  12. lemma OAI.CurrentMain.SampledPackingRound.signSum_projection line 196
  13. lemma OAI.CurrentMain.SampledPackingRound.signSum_orthogonal line 201
  14. lemma OAI.CurrentMain.SampledPackingRound.initial_signSum_orthogonal line 210
  15. lemma OAI.CurrentMain.SampledPackingRound.subinitial_signSum_orthogonal line 214
  16. lemma OAI.CurrentMain.SampledPackingRound.final_eq_signSum line 221
  17. lemma OAI.CurrentMain.SampledPackingRound.signSum_energy line 225
  18. lemma OAI.CurrentMain.SampledPackingRound.displacement_sum_le line 235
  19. lemma OAI.CurrentMain.SampledPackingRound.signSum_balance line 259
  20. lemma OAI.CurrentMain.SampledPackingRound.Estimates.balance line 295
  21. structure OAI.CurrentMain.OrthogonalProjectionPair line 318
  22. def OAI.CurrentMain.OrthogonalProjectionPair.total line 329
  23. def OAI.CurrentMain.OrthogonalProjectionPair.energy line 331
  24. def OAI.CurrentMain.OrthogonalProjectionPair.balance line 334
  25. def OAI.CurrentMain.OrthogonalProjectionPair.remaining line 337
  26. lemma OAI.CurrentMain.OrthogonalProjectionPair.total_projection line 340
  27. lemma OAI.CurrentMain.OrthogonalProjectionPair.left_le_total line 343
  28. lemma OAI.CurrentMain.OrthogonalProjectionPair.right_le_total line 345
  29. lemma OAI.CurrentMain.OrthogonalProjectionPair.total_energy_le line 347
  30. lemma OAI.CurrentMain.OrthogonalProjectionPair.energy_nonneg line 352
  31. lemma OAI.CurrentMain.OrthogonalProjectionPair.right_signSum_orthogonal line 359
  32. lemma OAI.CurrentMain.OrthogonalProjectionPair.left_signSum_orthogonal line 362
  33. lemma OAI.CurrentMain.OrthogonalProjectionPair.signSum_right_orthogonal line 365
  34. def OAI.CurrentMain.OrthogonalProjectionPair.appendRound line 370
  35. lemma OAI.CurrentMain.OrthogonalProjectionPair.appendRound_total line 379
  36. lemma OAI.CurrentMain.OrthogonalProjectionPair.appendRound_energy line 384
  37. lemma OAI.CurrentMain.OrthogonalProjectionPair.appendRound_balance line 395
  38. def OAI.CurrentMain.packingEnergy line 410
  39. def OAI.CurrentMain.packingRemainder line 412
  40. def OAI.CurrentMain.packingBalance line 415
  41. lemma OAI.CurrentMain.packingEnergy_zero line 418
  42. lemma OAI.CurrentMain.packingRemainder_zero line 420
  43. lemma OAI.CurrentMain.packingBalance_zero line 422
  44. lemma OAI.CurrentMain.packingEnergy_nonneg line 424
  45. lemma OAI.CurrentMain.packingEnergy_succ line 429
  46. lemma OAI.CurrentMain.packingEnergy_mono line 434
  47. lemma OAI.CurrentMain.packingRemainder_nonneg line 440
  48. lemma OAI.CurrentMain.packingRemainder_step line 446
  49. lemma OAI.CurrentMain.packingBalance_step line 455
  50. lemma OAI.CurrentMain.packingEnergy_exp_bound line 464
  51. lemma OAI.CurrentMain.packing_decay_exp_bound line 476
  52. def OAI.CurrentMain.mapUnitary line 487
  53. lemma OAI.CurrentMain.mapUnitary_coe line 490
  54. lemma OAI.CurrentMain.map_weightedAverage line 493
  55. lemma OAI.CurrentMain.map_average_defect line 503
  56. lemma OAI.CurrentMain.relative_coefficient_tests line 511