OAI/Combinatorics/SumProduct/Alignment/PointLaw01.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SourcePointLaw.interval_induction line 31
  2. theorem OAI.SourcePointLaw.tendsto_of_local_interval_law line 69
  3. def OAI.SourcePointLaw.residueInterval line 152
  4. lemma OAI.SourcePointLaw.mem_residueInterval line 155
  5. lemma OAI.SourcePointLaw.residueInterval_affine line 159
  6. theorem OAI.SourcePointLaw.residueInterval_card_error line 190
  7. theorem OAI.SourcePointLaw.residueInterval_card_scaled_error line 209
  8. theorem OAI.SourcePointLaw.residueInterval_card_tendsto line 225
  9. lemma OAI.SourcePointLaw.residueInterval_union line 236
  10. lemma OAI.SourcePointLaw.residueInterval_disjoint line 250
  11. def OAI.SourcePointLaw.windowSum line 261
  12. lemma OAI.SourcePointLaw.windowSum_add line 264
  13. lemma OAI.SourcePointLaw.windowSum_eq line 274