OAI/Combinatorics/SumProduct/Alignment/RoughKernel03.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformLipschitzApproximation.compact_pullback line 29
2. theorem OAI.UniformLipschitzApproximation.compact_pullback_complex line 72
3. def OAI.RoughKernelFactorization.kernelTestJoint line 134
4. abbrev OAI.RoughKernelFactorization.kernelCompatibleMetric line 150
5. theorem OAI.RoughKernelFactorization.uniform_kernel_tests line 168
6. lemma OAI.RoughKernelFactorization.integer_eval_modEq line 207
7. lemma OAI.RoughKernelFactorization.polynomial_residue_coset line 222
8. theorem OAI.RoughKernelFactorization.factorization_on_residue line 234
9. lemma OAI.RoughKernelFactorization.residue_range line 251