OAI/Combinatorics/SparsestCut/Mollifier.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformSparsestCut.ProductMollifier.bump line 12
  2. def OAI.UniformSparsestCut.ProductMollifier.rho line 13
  3. lemma OAI.UniformSparsestCut.ProductMollifier.rho_nonneg line 14
  4. lemma OAI.UniformSparsestCut.ProductMollifier.rho_integral line 15
  5. lemma OAI.UniformSparsestCut.ProductMollifier.rho_integrable line 16
  6. lemma OAI.UniformSparsestCut.ProductMollifier.rho_smooth line 17
  7. lemma OAI.UniformSparsestCut.ProductMollifier.rho_compact line 18
  8. lemma OAI.UniformSparsestCut.ProductMollifier.rho_even line 19
  9. lemma OAI.UniformSparsestCut.ProductMollifier.rho_support line 20
  10. lemma OAI.UniformSparsestCut.ProductMollifier.rho_deriv_integrable line 24
  11. def OAI.UniformSparsestCut.ProductMollifier.density line 27
  12. lemma OAI.UniformSparsestCut.ProductMollifier.density_nonneg line 28
  13. lemma OAI.UniformSparsestCut.ProductMollifier.density_smooth line 30
  14. lemma OAI.UniformSparsestCut.ProductMollifier.density_integral line 33
  15. lemma OAI.UniformSparsestCut.ProductMollifier.density_support line 37
  16. lemma OAI.UniformSparsestCut.ProductMollifier.density_compact line 41
  17. lemma OAI.UniformSparsestCut.ProductMollifier.density_integrable line 46
  18. lemma OAI.UniformSparsestCut.ProductMollifier.density_hasDeriv line 48
  19. lemma OAI.UniformSparsestCut.ProductMollifier.density_deriv_integral line 54
  20. def OAI.UniformSparsestCut.ProductMollifier.coordinate line 63
  21. lemma OAI.UniformSparsestCut.ProductMollifier.coordinate_apply line 65
  22. def OAI.UniformSparsestCut.ProductMollifier.kernel line 67
  23. lemma OAI.UniformSparsestCut.ProductMollifier.kernel_smooth line 68
  24. lemma OAI.UniformSparsestCut.ProductMollifier.kernel_nonneg line 73
  25. lemma OAI.UniformSparsestCut.ProductMollifier.kernel_integral line 75
  26. lemma OAI.UniformSparsestCut.ProductMollifier.kernel_integrable line 78
  27. lemma OAI.UniformSparsestCut.ProductMollifier.coordinate_norm_bound line 82
  28. lemma OAI.UniformSparsestCut.ProductMollifier.kernel_support_bound line 97
  29. lemma OAI.UniformSparsestCut.ProductMollifier.kernel_compact line 105
  30. lemma OAI.UniformSparsestCut.ProductMollifier.kernel_hasFDeriv line 112
  31. lemma OAI.UniformSparsestCut.ProductMollifier.kernel_partial line 120
  32. lemma OAI.UniformSparsestCut.ProductMollifier.kernel_partial_integral line 126