OAI/Combinatorics/SumProduct/Alignment/AllLevel07.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AllLevelFactorization.Factorization.realization_of_residue line 31
  2. def OAI.AllLevelFactorization.Factorization.vertex line 41
  3. lemma OAI.AllLevelFactorization.Factorization.vertex_mod line 44
  4. lemma OAI.AllLevelFactorization.Factorization.affine_vertex_mod line 53
  5. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.cube_realization line 68
  6. def OAI.AllLevelFactorization.Factorization.ResidueCover.limitIntegral line 104
  7. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.local_integerBox line 111
  8. theorem OAI.CompactTwoScale.freezing_uniform line 168
  9. theorem OAI.AllLevelFactorization.Factorization.smooth_neighborhood_uniform line 213
  10. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.two_scale_uniform line 254
  11. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.local_integerBox_uniform line 288