OAI/Combinatorics/SumProduct/Alignment/RoughProduct03.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RoughCubeUniform.larger_scale_uniform line 28
  2. lemma OAI.RoughProductRemoval.power_domination_nonneg line 82
  3. lemma OAI.RoughProductRemoval.domination_smaller line 90
  4. lemma OAI.RoughProductRemoval.residual_power_domination line 101
  5. def OAI.RoughProductRemoval.totalScale line 122
  6. lemma OAI.RoughProductRemoval.totalScale_succ line 124
  7. lemma OAI.RoughProductRemoval.totalScale_bounds line 129
  8. lemma OAI.RoughProductRemoval.totalScale_pos_eventually line 138
  9. lemma OAI.RoughProductRemoval.tail_domination line 145
  10. lemma OAI.RoughProductRemoval.product_tail_bound line 156
  11. lemma OAI.RoughProductRemoval.filter_union_bound line 190
  12. lemma OAI.RoughProductRemoval.smooth_nat_coprime_rough line 206
  13. theorem OAI.RoughProductRemoval.firstBad_card_bound line 217
  14. theorem OAI.RoughProductRemoval.firstBad_fiber_eventual line 243