OAI/Combinatorics/SumProduct/Alignment/CubeLocal03.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ComparableBoxLeibman.halfOpenBox line 27
  2. lemma OAI.ComparableBoxLeibman.mem_halfOpenBox line 30
  3. lemma OAI.ComparableBoxLeibman.halfOpen_bounds line 49
  4. theorem OAI.CubeLocalHaar.smooth_halfOpen_cube_haar line 109
  5. def OAI.CubeLocalHaar.progressionLo line 175
  6. def OAI.CubeLocalHaar.progressionHi line 177
  7. lemma OAI.CubeLocalHaar.progression_box_bounds line 180
  8. lemma OAI.CubeLocalHaar.progression_normalized_mem line 217
  9. def OAI.CubeLocalHaar.sourceCenter line 238
  10. def OAI.CubeLocalHaar.sourceResidue line 240
  11. lemma OAI.CubeLocalHaar.source_box_bounds line 244
  12. lemma OAI.CubeLocalHaar.source_box_geometry line 262
  13. def OAI.CubeLocalHaar.sourceVertex line 288
  14. lemma OAI.CubeLocalHaar.sourceVertex_emod line 292
  15. lemma OAI.CubeLocalHaar.sourceVertex_real line 299
  16. lemma OAI.CubeLocalHaar.sourceVertex_normalized line 306