OAI/Computability/MinUncut/Estimates/ExpectResampleRow.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.RowNoise.expect_resample_row line 26
  2. lemma OAI.MinUncut.RowNoise.expect_rest line 34
  3. lemma OAI.MinUncut.RowNoise.selectedProject_continuous line 40
  4. lemma OAI.MinUncut.Inner.pairSlice_measurable line 57
  5. lemma OAI.MinUncut.Inner.pairSlice_memLp line 63
  6. lemma OAI.MinUncut.Inner.pairSlice_row line 69
  7. theorem OAI.MinUncut.Inner.pairSlice_energy_law line 86
  8. lemma OAI.MinUncut.Inner.pairSlice_atom_law line 107
  9. theorem OAI.MinUncut.Inner.pairSlice_atom_mean line 116
  10. def OAI.MinUncut.Subbox.pointBox line 130
  11. lemma OAI.MinUncut.Subbox.pointBox_set line 135
  12. def OAI.MinUncut.Inner.faceEmbed line 145
  13. lemma OAI.MinUncut.Inner.faceEmbed_injective line 149
  14. lemma OAI.MinUncut.Inner.faceEmbed_mem line 157
  15. lemma OAI.MinUncut.Inner.faceEmbed_face line 161
  16. def OAI.MinUncut.Inner.embedSingle line 164
  17. lemma OAI.MinUncut.Inner.embedSingle_injective line 167
  18. def OAI.MinUncut.Inner.extendSingle line 172
  19. lemma OAI.MinUncut.Inner.extendSingle_local line 176
  20. lemma OAI.MinUncut.Inner.extendSingle_other line 182
  21. lemma OAI.MinUncut.Inner.extendSingle_support line 190
  22. lemma OAI.MinUncut.Inner.extendSingle_zero_outside_pair line 206
  23. lemma OAI.MinUncut.Inner.pairSlice_add_rows line 218
  24. def OAI.MinUncut.Inner.pairProcessedOnBox line 231
  25. lemma OAI.MinUncut.Inner.pairProcessedOnBox_resample line 239
  26. theorem OAI.MinUncut.Inner.pairProcessedOnBox_law line 260
  27. theorem OAI.MinUncut.Inner.actual_pair_box_power line 300
  28. abbrev OAI.MinUncut.BoxGaussian.Outside line 332
  29. def OAI.MinUncut.BoxGaussian.indexEquiv line 334
  30. lemma OAI.MinUncut.BoxGaussian.indexEquiv_left line 338
  31. lemma OAI.MinUncut.BoxGaussian.indexEquiv_right line 341
  32. lemma OAI.MinUncut.BoxGaussian.indexEquiv_symm_left line 345
  33. lemma OAI.MinUncut.BoxGaussian.indexEquiv_symm_right line 351
  34. def OAI.MinUncut.BoxGaussian.joinEquiv line 356
  35. def OAI.MinUncut.BoxGaussian.join line 361
  36. lemma OAI.MinUncut.BoxGaussian.join_at line 365
  37. lemma OAI.MinUncut.BoxGaussian.join_other line 370
  38. lemma OAI.MinUncut.BoxGaussian.join_preserves line 374
  39. lemma OAI.MinUncut.BoxGaussian.integral_split line 381
  40. lemma OAI.MinUncut.Box.power_le_root line 391
  41. lemma OAI.MinUncut.Box.power_sum_root line 396
  42. lemma OAI.MinUncut.Box.square_root_power line 406
  43. lemma OAI.MinUncut.Box.cube_power_to_bound line 419
  44. lemma OAI.MinUncut.CubeRows.card_other line 432
  45. lemma OAI.MinUncut.Inner.gaussianSlice_background line 447
  46. lemma OAI.MinUncut.Inner.faceCorrelation_measurable_field line 463
  47. lemma OAI.MinUncut.Inner.gaussianSlice_joint_continuous line 480
  48. lemma OAI.MinUncut.Inner.centered_gaussianSlice_measurable line 492
  49. def OAI.MinUncut.Inner.zeroProcessedOnBox line 506
  50. lemma OAI.MinUncut.Inner.centered_gaussianSlice_diagonal_measurable line 515
  51. lemma OAI.MinUncut.Inner.zeroProcessedOnBox_measurable line 527
  52. lemma OAI.MinUncut.Inner.zeroProcessedOnBox_abs_le line 535
  53. lemma OAI.MinUncut.Inner.freeGaussianPoints_range line 542
  54. lemma OAI.MinUncut.Inner.zeroProcessedOnBox_join line 554
  55. lemma OAI.MinUncut.BoxGaussian.integral_split_power_bound line 580
  56. theorem OAI.MinUncut.Inner.actual_zero_box_power line 621
  57. lemma OAI.MinUncut.Inner.pairClass_dimension line 655
  58. theorem OAI.MinUncut.Inner.actual_pair_box_bound line 662
  59. lemma OAI.MinUncut.Inner.pairSlice_c_measurable line 674
  60. lemma OAI.MinUncut.Inner.pairProcessedOnBox_c_measurable line 681
  61. lemma OAI.MinUncut.Inner.pairProcessedOnBox_abs_le line 689
  62. theorem OAI.MinUncut.Subbox.pointed_bayes line 703
  63. theorem OAI.MinUncut.Inner.actual_pair_box_average line 728