OAI/Combinatorics/SumProduct/Alignment/RoughLiteral01.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RoughSourceExceptional.Ico_eq_range line 24
  2. def OAI.RoughSourceExceptional.timeLength line 34
  3. def OAI.RoughSourceExceptional.firstTime line 35
  4. def OAI.RoughSourceExceptional.times line 36
  5. lemma OAI.RoughSourceExceptional.times_eq_range line 38
  6. lemma OAI.RoughSourceExceptional.mem_times line 48
  7. lemma OAI.RoughSourceExceptional.time_injective line 64
  8. lemma OAI.RoughSourceExceptional.times_card line 70
  9. lemma OAI.RoughSourceExceptional.scale_at_index line 74
  10. lemma OAI.RoughSourceExceptional.firstTime_rough line 82
  11. lemma OAI.RoughSourceExceptional.timeLength_tendsto line 88
  12. lemma OAI.RoughSourceExceptional.integer_scales_of_real line 103
  13. def OAI.RoughSourceExceptional.exceptional line 126
  14. lemma OAI.RoughSourceExceptional.exceptional_card line 132
  15. theorem OAI.RoughSourceExceptional.source_exceptional_bound line 149
  16. def OAI.RoughLiteralBoxes.lower line 197
  17. def OAI.RoughLiteralBoxes.upper line 199
  18. def OAI.RoughLiteralBoxes.leftCondition line 201
  19. def OAI.RoughLiteralBoxes.rightCondition line 202
  20. lemma OAI.RoughLiteralBoxes.lower_le_iff line 204
  21. lemma OAI.RoughLiteralBoxes.lt_upper_iff line 210
  22. lemma OAI.RoughLiteralBoxes.lower_bounds line 216
  23. lemma OAI.RoughLiteralBoxes.upper_bounds line 223
  24. def OAI.RoughLiteralBoxes.points line 233
  25. lemma OAI.RoughLiteralBoxes.mem_points line 236
  26. lemma OAI.RoughLiteralBoxes.points_eq_box line 242
  27. def OAI.RoughLiteralBoxes.residuePoints line 250
  28. lemma OAI.RoughLiteralBoxes.residuePoints_eq_box line 254
  29. lemma OAI.RoughLiteralBoxes.rounded_geometry line 260
  30. def OAI.RoughLiteralBoxes.BadAt line 281
  31. lemma OAI.RoughLiteralBoxes.badAt_halfopen line 292
  32. def OAI.RoughLiteralBoxes.exceptional line 303
  33. lemma OAI.RoughLiteralBoxes.exceptional_subset line 309
  34. theorem OAI.RoughLiteralBoxes.source_literal_bound line 326