OAI/Computability/MinUncut/Estimates/Away.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.Subbox.Away line 23
  2. lemma OAI.MinUncut.Subbox.card_away line 25
  3. def OAI.MinUncut.Subbox.pointedSet line 28
  4. lemma OAI.MinUncut.Subbox.mem_pointedSet_self line 31
  5. lemma OAI.MinUncut.Subbox.mem_pointedSet line 34
  6. lemma OAI.MinUncut.Subbox.pointedSet_card line 44
  7. lemma OAI.MinUncut.Subbox.pointed_membership line 52
  8. lemma OAI.MinUncut.Subbox.expect_coordinate line 62
  9. abbrev OAI.MinUncut.Subbox.PointedBox line 71
  10. def OAI.MinUncut.Subbox.InBox line 73
  11. lemma OAI.MinUncut.Subbox.point_mem line 77
  12. lemma OAI.MinUncut.Subbox.other_point_probability line 80
  13. def OAI.MinUncut.Subbox.FaceInBox line 98
  14. lemma OAI.MinUncut.Subbox.other_face_probability line 101
  15. lemma OAI.MinUncut.Subbox.exists_indicator_le line 118
  16. abbrev OAI.MinUncut.Subbox.Row line 129
  17. def OAI.MinUncut.Subbox.Removed line 131
  18. lemma OAI.MinUncut.Subbox.removal_probability line 136
  19. lemma OAI.MinUncut.RowNoise.selectedProject_filter_loss line 196
  20. lemma OAI.MinUncut.RowNoise.selectedProject_average_loss line 207
  21. lemma OAI.MinUncut.RowNoise.selectedProject_average_contraction line 221
  22. def OAI.MinUncut.Subbox.positiveSupport line 236
  23. lemma OAI.MinUncut.Subbox.positiveSupport_card line 239
  24. def OAI.MinUncut.Subbox.localizedSelection line 245
  25. lemma OAI.MinUncut.Subbox.localization_energy_loss line 249
  26. lemma OAI.MinUncut.Subbox.localized_energy_contraction line 281
  27. def OAI.MinUncut.RowNoise.zeroFree line 298
  28. lemma OAI.MinUncut.RowNoise.dual_local_sum line 301
  29. lemma OAI.MinUncut.RowNoise.character_local_sum line 324
  30. lemma OAI.MinUncut.RowNoise.character_single line 332
  31. def OAI.MinUncut.RowNoise.localSlice line 335
  32. lemma OAI.MinUncut.RowNoise.selectedProject_local_sum line 339
  33. lemma OAI.MinUncut.RowNoise.localSlice_odd line 367
  34. lemma OAI.MinUncut.RowNoise.odd_coefficient_zero line 393
  35. lemma OAI.MinUncut.RowNoise.localSlice_fourier line 405
  36. abbrev OAI.MinUncut.Inner.PairClass line 424
  37. instance OAI.MinUncut.Inner.pairClassOrder line 426
  38. def OAI.MinUncut.Inner.PairAdmissible line 430
  39. lemma OAI.MinUncut.Inner.pairAdmissible_exists line 436
  40. def OAI.MinUncut.Inner.admissibleClasses line 444
  41. def OAI.MinUncut.Inner.maskClass line 447
  42. lemma OAI.MinUncut.Inner.maskClass_some line 451
  43. lemma OAI.MinUncut.Inner.maskClass_none line 460
  44. def OAI.MinUncut.Inner.classSelection line 471
  45. lemma OAI.MinUncut.Inner.classSelection_partition line 475
  46. lemma OAI.MinUncut.Inner.joint_pair_matching line 494
  47. def OAI.MinUncut.Inner.freePairRows line 510
  48. lemma OAI.MinUncut.Inner.local_face_in_box line 514
  49. lemma OAI.MinUncut.Inner.local_free_left line 517
  50. lemma OAI.MinUncut.Inner.local_free_right line 521
  51. def OAI.MinUncut.Inner.retainedClass line 525
  52. lemma OAI.MinUncut.Inner.retained_pair_admissible line 529
  53. lemma OAI.MinUncut.Inner.retained_pair_local line 536
  54. def OAI.MinUncut.Inner.pairSlice line 553
  55. theorem OAI.MinUncut.Inner.retained_local_sum line 560
  56. theorem OAI.MinUncut.Inner.pairSlice_fourier line 577
  57. lemma OAI.MinUncut.Inner.pairSlice_background line 589
  58. lemma OAI.MinUncut.GaussianHermite.H_zero line 608
  59. lemma OAI.MinUncut.GaussianHermite.H_mean line 610
  60. lemma OAI.MinUncut.GaussianHermite.psi_update line 613
  61. lemma OAI.MinUncut.GaussianHermite.memLp_psi_update line 623
  62. lemma OAI.MinUncut.GaussianHermite.integral_psi_update line 627
  63. lemma OAI.MinUncut.GaussianHermite.psi_localized line 631