OAI/Combinatorics/SumProduct/Alignment/RoughKernel01.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RealPolynomialDegree.HasDegree line 26
  2. lemma OAI.RealPolynomialDegree.const line 29
  3. lemma OAI.RealPolynomialDegree.mono line 32
  4. lemma OAI.RealPolynomialDegree.add line 37
  5. lemma OAI.RealPolynomialDegree.mul line 43
  6. lemma OAI.RealPolynomialDegree.scale line 49
  7. lemma OAI.RealPolynomialDegree.neg line 52
  8. lemma OAI.RealPolynomialDegree.rational_eval_bound line 55
  9. lemma OAI.RoughKernelFactorization.multiplication_degree line 94
  10. lemma OAI.RoughKernelFactorization.sectionFlow_degree line 134
  11. theorem OAI.RoughKernelFactorization.residual_degree_uniform line 147
  12. def OAI.NonnormalCoset.map line 181
  13. lemma OAI.NonnormalCoset.map_mk line 192
  14. def OAI.PhysicalCubeMaps.vertices line 199
  15. def OAI.PhysicalCubeMaps.upperFace line 203
  16. lemma OAI.PhysicalCubeMaps.vertices_apply line 211
  17. lemma OAI.PhysicalCubeMaps.upperFace_apply line 213
  18. def OAI.RoughKernelFactorization.kernelInclusion line 232
  19. lemma OAI.RoughKernelFactorization.kernelInclusion_apply line 236
  20. lemma OAI.RoughKernelFactorization.kernelInclusion_continuous line 239
  21. def OAI.RoughKernelFactorization.kernelLattice line 246
  22. lemma OAI.RoughKernelFactorization.mem_kernelLattice line 248
  23. def OAI.RoughKernelFactorization.kernelTestMap line 255
  24. lemma OAI.RoughKernelFactorization.kernelTestMap_mk line 263
  25. lemma OAI.RoughKernelFactorization.character_conjugate line 273
  26. theorem OAI.RoughKernelFactorization.kernel_quotient_compact line 285
  27. theorem OAI.RoughKernelFactorization.integer_kernel_quotient_compact line 327