OAI/Combinatorics/SumProduct/Alignment/RoughDyadic01.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RoughAnalyticRationalization.cast_progression_bounds line 28
  2. lemma OAI.RoughAnalyticRationalization.split_comp line 37
  3. theorem OAI.RoughAnalyticRationalization.rational_split_from_discrepancies line 70
  4. def OAI.RoughDyadicFiltration.weight line 198
  5. lemma OAI.RoughDyadicFiltration.weight_mono line 199
  6. def OAI.RoughDyadicFiltration.cutoff line 203
  7. lemma OAI.RoughDyadicFiltration.cutoff_le line 205
  8. lemma OAI.RoughDyadicFiltration.cutoff_spec line 207
  9. def OAI.RoughDyadicFiltration.level line 210
  10. lemma OAI.RoughDyadicFiltration.mem_level line 211
  11. lemma OAI.RoughDyadicFiltration.unweight_level line 213
  12. lemma OAI.RoughDyadicFiltration.level_antitone line 215
  13. lemma OAI.RoughDyadicFiltration.level_top line 219
  14. lemma OAI.RoughDyadicFiltration.level_terminal line 226
  15. lemma OAI.RoughDyadicFiltration.twice_weight line 238
  16. lemma OAI.RoughDyadicFiltration.commutator_le_of_le line 244
  17. lemma OAI.RoughDyadicFiltration.bracket line 256
  18. def OAI.RoughDyadicFiltration.filtration line 262
  19. instance OAI.RoughDyadicFiltration.normal line 266
  20. lemma OAI.RoughDyadicFiltration.filtration_zero line 268
  21. lemma OAI.RoughDyadicFiltration.filtration_one line 269
  22. lemma OAI.RoughDyadicFiltration.coordinate_adapted line 274
  23. theorem OAI.RoughDyadicFiltration.logarithmic_adapted line 301