OAI/Probability/GaussianInformation/Dyadic/HeavyCells.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RepeatedLocalization.heavyThreshold line 19
  2. lemma OAI.RepeatedLocalization.heavyThreshold_pos line 21
  3. lemma OAI.RepeatedLocalization.heavyThreshold_zero line 22
  4. lemma OAI.RepeatedLocalization.heavyThreshold_add line 23
  5. def OAI.RepeatedLocalization.deepHeavyDepth line 30
  6. lemma OAI.RepeatedLocalization.deepHeavyDepth_le line 35
  7. lemma OAI.RepeatedLocalization.le_deepHeavyDepth line 43
  8. lemma OAI.RepeatedLocalization.measurable_deepHeavyDepth line 51
  9. lemma OAI.RepeatedLocalization.deepHeavyDepth_heavy line 59
  10. def OAI.RepeatedLocalization.deepHeavyCell line 69
  11. lemma OAI.RepeatedLocalization.measurable_cellAt_variable line 74
  12. lemma OAI.RepeatedLocalization.measurable_deepHeavyCell line 82
  13. lemma OAI.RepeatedLocalization.deepHeavyCell_mem line 90
  14. lemma OAI.RepeatedLocalization.deepHeavyCell_subset line 96
  15. lemma OAI.RepeatedLocalization.deepHeavyCell_level line 105
  16. lemma OAI.RepeatedLocalization.finite_cells_bounded_level line 110
  17. lemma OAI.RepeatedLocalization.finite_range_deepHeavyCell line 116
  18. lemma OAI.RepeatedLocalization.heavyThreshold_pow line 127
  19. lemma OAI.RepeatedLocalization.heavyThreshold_sq line 132
  20. lemma OAI.RepeatedLocalization.heavyThreshold_tendsto_zero line 139
  21. lemma OAI.RepeatedLocalization.exists_heavy_cutoff line 150
  22. lemma OAI.RepeatedLocalization.deepHeavyDepth_maximal line 169
  23. lemma OAI.RepeatedLocalization.selected_inter_heavy_descendant_empty line 178
  24. lemma OAI.RepeatedLocalization.measurable_heavySelectionEvent line 194
  25. lemma OAI.RepeatedLocalization.selected_posterior_spread line 199
  26. lemma OAI.RepeatedLocalization.cellSet_disjoint_of_level_eq line 234
  27. lemma OAI.RepeatedLocalization.heavy_cell_weight_budget line 244
  28. lemma OAI.RepeatedLocalization.heavy_selection_range_properties line 281