OAI/Combinatorics/SumProduct/Alignment/CubeKernel01.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubeKernel.value_sub line 27
  2. lemma OAI.CubeKernel.integer_spatial line 32
  3. lemma OAI.CubeKernel.spatial_affine line 50
  4. lemma OAI.CubeKernel.split_subspace line 65
  5. theorem OAI.CubeKernel.kernel_polynomial line 84
  6. def OAI.CubeReduction.metricIdentity line 139
  7. theorem OAI.CubeReduction.reduce_split_cubes line 147
  8. theorem OAI.CubeZero.no_cube_at line 263
  9. theorem OAI.CubeZero.eventually_no_zero_cubes line 297