OAI/Computability/MinUncut/Estimates/Density.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.OuterSmoothness.expect_prod line 13
  2. lemma OAI.MinUncut.OuterSmoothness.expect_pair line 19
  3. structure OAI.MinUncut.OuterSmoothness.Density line 23
  4. instance OAI.MinUncut.OuterSmoothness.Density.(instance at line 30) line 30
  5. lemma OAI.MinUncut.OuterSmoothness.Density.pointwise_le_card line 32
  6. def OAI.MinUncut.OuterSmoothness.Density.tvUniform line 42
  7. lemma OAI.MinUncut.OuterSmoothness.Density.tvUniform_le_sqrt line 44
  8. def OAI.MinUncut.OuterSmoothness.Density.ofMap line 56
  9. lemma OAI.MinUncut.OuterSmoothness.Density.expect_ofMap line 66
  10. lemma OAI.MinUncut.OuterSmoothness.Density.ofMap_eq_of_invariant line 79
  11. lemma OAI.MinUncut.OuterSmoothness.Density.ofMap_surjective_hom line 87
  12. lemma OAI.MinUncut.OuterSmoothness.Density.ofMap_pi line 104
  13. lemma OAI.MinUncut.OuterSmoothness.Density.ofMap_fst line 117
  14. lemma OAI.MinUncut.OuterSmoothness.Density.ofMap_snd line 126
  15. lemma OAI.MinUncut.OuterSmoothness.Density.ofMap_family line 133
  16. lemma OAI.MinUncut.OuterSmoothness.Density.ofMap_uniform_shift line 138
  17. def OAI.MinUncut.OuterSmoothness.hiddenDensity line 161
  18. lemma OAI.MinUncut.OuterSmoothness.hiddenDensity_eq_prod line 170
  19. lemma OAI.MinUncut.OuterSmoothness.hiddenDensity_cross_disjoint line 174
  20. lemma OAI.MinUncut.OuterSmoothness.hiddenDensity_le line 190
  21. def OAI.MinUncut.OuterSmoothness.mixture line 197
  22. lemma OAI.MinUncut.OuterSmoothness.mixture_variance line 205
  23. abbrev OAI.MinUncut.OuterSmoothness.FixedSets line 220
  24. lemma OAI.MinUncut.OuterSmoothness.fixedSets_nonempty line 223
  25. def OAI.MinUncut.OuterSmoothness.fixedSetsEquiv line 227
  26. lemma OAI.MinUncut.OuterSmoothness.membership_probability_eq line 233
  27. lemma OAI.MinUncut.OuterSmoothness.membership_probability line 240
  28. lemma OAI.MinUncut.OuterSmoothness.overlap_union_bound line 262
  29. lemma OAI.MinUncut.OuterSmoothness.fixedSet_overlap_probability line 274
  30. lemma OAI.MinUncut.OuterSmoothness.mixture_tv_bound line 294
  31. abbrev OAI.MinUncut.OuterSmoothness.JointForms.F₂ line 331
  32. abbrev OAI.MinUncut.OuterSmoothness.JointForms.Triple line 332
  33. abbrev OAI.MinUncut.OuterSmoothness.JointForms.Block line 340
  34. abbrev OAI.MinUncut.OuterSmoothness.JointForms.HiddenRaw line 341
  35. abbrev OAI.MinUncut.OuterSmoothness.JointForms.FullRaw line 342
  36. abbrev OAI.MinUncut.OuterSmoothness.JointForms.Raw line 343
  37. def OAI.MinUncut.OuterSmoothness.JointForms.fullPull line 345
  38. lemma OAI.MinUncut.OuterSmoothness.JointForms.fullPull_surjective line 348
  39. def OAI.MinUncut.OuterSmoothness.JointForms.hiddenPull line 354
  40. def OAI.MinUncut.OuterSmoothness.JointForms.hiddenLaw line 357
  41. lemma OAI.MinUncut.OuterSmoothness.JointForms.fullPull_uniform line 360
  42. lemma OAI.MinUncut.OuterSmoothness.JointForms.card_block line 364
  43. def OAI.MinUncut.OuterSmoothness.JointForms.output line 371
  44. lemma OAI.MinUncut.OuterSmoothness.JointForms.output_density line 375
  45. def OAI.MinUncut.OuterSmoothness.JointForms.offset line 391
  46. def OAI.MinUncut.OuterSmoothness.JointForms.affineOutput line 394
  47. lemma OAI.MinUncut.OuterSmoothness.JointForms.joint_density line 399
  48. theorem OAI.MinUncut.OuterSmoothness.JointForms.joint_smoothness line 416
  49. lemma OAI.MinUncut.BinaryFourier.coefficient_sum line 446
  50. lemma OAI.MinUncut.BinaryFourier.coefficient_character line 452
  51. lemma OAI.MinUncut.BinaryFourier.coefficient_scale line 456
  52. lemma OAI.MinUncut.BinaryFourier.coefficient_sub line 460
  53. lemma OAI.MinUncut.BinaryFourier.fourth_moment line 464
  54. def OAI.MinUncut.BinaryFourier.largeSpectrum line 483
  55. def OAI.MinUncut.BinaryFourier.largePart line 486
  56. def OAI.MinUncut.BinaryFourier.remainder line 489
  57. lemma OAI.MinUncut.BinaryFourier.coefficient_largePart line 491
  58. lemma OAI.MinUncut.BinaryFourier.coefficient_remainder line 499
  59. lemma OAI.MinUncut.BinaryFourier.energy_le_of_bounded line 507
  60. lemma OAI.MinUncut.BinaryFourier.largeSpectrum_card line 513
  61. lemma OAI.MinUncut.BinaryFourier.remainder_fourth_bound line 527
  62. lemma OAI.MinUncut.BinaryFourier.remainder_abs_bound line 544
  63. lemma OAI.MinUncut.BinaryFourier.coefficient_projected_sum line 572
  64. lemma OAI.MinUncut.BinaryFourier.coefficient_pullback line 585
  65. lemma OAI.MinUncut.BinaryFourier.coefficient_largePart_pullback line 595
  66. lemma OAI.MinUncut.BinaryFourier.large_preimage_of_nonzero line 601
  67. lemma OAI.MinUncut.BinaryFourier.extract_matched_odd line 613
  68. lemma OAI.MinUncut.OuterSmoothness.Density.abs_expect_le line 641
  69. lemma OAI.MinUncut.OuterSmoothness.Density.expect_difference line 645