OAI/Computability/MinUncut/Estimates/FaceUpdateSelf.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Inner.face_update_self line 22
  2. theorem OAI.MinUncut.Inner.faceCorrelation_box_cs line 27
  3. def OAI.MinUncut.GaussianHermite.indexSym line 54
  4. lemma OAI.MinUncut.GaussianHermite.count_indexSym line 61
  5. lemma OAI.MinUncut.GaussianHermite.indexSym_injective line 65
  6. lemma OAI.MinUncut.GaussianHermite.card_low_le line 71
  7. lemma OAI.MinUncut.RowNoise.selectedProject_atom_mean_uniform line 85
  8. def OAI.MinUncut.Slice.clip line 114
  9. lemma OAI.MinUncut.Slice.clip_abs_le line 116
  10. lemma OAI.MinUncut.Slice.clip_abs_le_self line 122
  11. lemma OAI.MinUncut.Slice.clip_loss line 134
  12. lemma OAI.MinUncut.Slice.clip_sq_le line 146
  13. lemma OAI.MinUncut.Slice.coefficient_lipschitz line 151
  14. lemma OAI.MinUncut.Slice.clip_mean_loss line 161
  15. def OAI.MinUncut.Slice.oddMax line 170
  16. lemma OAI.MinUncut.Slice.oddMax_nonneg line 175
  17. lemma OAI.MinUncut.Slice.coefficient_le_oddMax line 182
  18. def OAI.MinUncut.Slice.processed line 192
  19. lemma OAI.MinUncut.Slice.processed_abs_le line 196
  20. lemma OAI.MinUncut.Slice.processed_sq_le line 203
  21. lemma OAI.MinUncut.Slice.processed_energy_le line 210
  22. lemma OAI.MinUncut.Slice.processed_coefficient_le line 222
  23. lemma OAI.MinUncut.Slice.mean_abs_le_sqrt line 251
  24. lemma OAI.MinUncut.Slice.processed_mean_loss line 259
  25. lemma OAI.MinUncut.IndependentSquares.expect_prod line 287
  26. lemma OAI.MinUncut.IndependentSquares.factor_squares line 294
  27. lemma OAI.MinUncut.IndependentSquares.independent_square_bound line 323
  28. def OAI.MinUncut.IndependentSquares.restrictLinear line 340
  29. lemma OAI.MinUncut.IndependentSquares.restrict_surjective line 346
  30. lemma OAI.MinUncut.IndependentSquares.expect_surjective_linear line 354
  31. lemma OAI.MinUncut.IndependentSquares.expect_restrict line 371
  32. lemma OAI.MinUncut.Slice.clip_memLp line 381
  33. lemma OAI.MinUncut.Slice.clip_integral_loss line 387
  34. def OAI.MinUncut.Slice.centeredClip line 395
  35. lemma OAI.MinUncut.Slice.centeredClip_mean_zero line 398
  36. lemma OAI.MinUncut.Slice.centeredClip_abs_le line 404
  37. lemma OAI.MinUncut.Slice.centeredClip_loss line 414
  38. lemma OAI.MinUncut.Slice.tail_probability line 441
  39. lemma OAI.MinUncut.Slice.integral_tail_loss line 449
  40. abbrev OAI.MinUncut.CubeRows.Other line 476
  41. def OAI.MinUncut.CubeRows.join line 478
  42. lemma OAI.MinUncut.CubeRows.join_i line 482
  43. lemma OAI.MinUncut.CubeRows.join_j line 484
  44. lemma OAI.MinUncut.CubeRows.join_other line 487
  45. def OAI.MinUncut.CubeRows.splitEquiv line 490
  46. def OAI.MinUncut.CubeRows.vertex line 496
  47. def OAI.MinUncut.CubeRows.face line 498
  48. def OAI.MinUncut.CubeRows.rowJ line 500
  49. def OAI.MinUncut.CubeRows.rowI line 503
  50. lemma OAI.MinUncut.CubeRows.bool_choice_injective line 506
  51. lemma OAI.MinUncut.CubeRows.rowJ_injective line 510
  52. lemma OAI.MinUncut.CubeRows.rowI_injective line 523
  53. lemma OAI.MinUncut.CubeRows.face_join_J line 536
  54. lemma OAI.MinUncut.CubeRows.face_join_I line 546
  55. lemma OAI.MinUncut.CubeRows.prod_split line 555
  56. def OAI.MinUncut.CubeRows.boolSplitEquiv line 569
  57. lemma OAI.MinUncut.CubeRows.expect_boolSplit line 576
  58. def OAI.MinUncut.CubeRows.cubeExpectation line 582
  59. def OAI.MinUncut.CubeRows.squareProduct line 588
  60. lemma OAI.MinUncut.CubeRows.cubeProduct_eq line 597
  61. lemma OAI.MinUncut.CubeRows.cubeExpectation_restrict line 606
  62. lemma OAI.MinUncut.CubeRows.cubeExpectation_eq_squares line 623
  63. lemma OAI.MinUncut.CubeRows.cubeExpectation_bound line 656