OAI/Combinatorics/SumProduct/Alignment/RoughKernel02.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.RoughKernelFactorization.Reduction line 28
  2. theorem OAI.RoughKernelFactorization.exists_reduction line 41
  3. def OAI.RoughKernelFactorization.Reduction.chart line 62
  4. def OAI.RoughKernelFactorization.Reduction.flow line 65
  5. lemma OAI.RoughKernelFactorization.Reduction.flow_character line 67
  6. lemma OAI.RoughKernelFactorization.Reduction.flow_rational line 70
  7. lemma OAI.RoughKernelFactorization.Reduction.coset_period line 74
  8. theorem OAI.RoughKernelFactorization.Reduction.lower_dimensional_factorization line 81
  9. theorem OAI.RealPolynomialDegree.rational_map_bound line 114
  10. theorem OAI.RealPolynomialDegree.log_degree_bound line 127
  11. theorem OAI.RealPolynomialDegree.coord_degree_bound line 136
  12. lemma OAI.RoughKernelFactorization.Reduction.kernel_connected line 167
  13. lemma OAI.RoughKernelFactorization.Reduction.kernel_simplyConnected line 172
  14. theorem OAI.RoughKernelFactorization.Reduction.logarithmic_factorization line 177
  15. theorem OAI.RoughKernelFactorization.exists_logarithmic_kernel_reduction line 202
  16. theorem OAI.UniformLipschitzApproximation.exists_common_bound line 240