OAI/Combinatorics/SparsestCut/KernelApprox.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformSparsestCut.KernelApprox.profile line 12
  2. lemma OAI.UniformSparsestCut.KernelApprox.profile_nonneg line 14
  3. lemma OAI.UniformSparsestCut.KernelApprox.profile_le_one line 19
  4. lemma OAI.UniformSparsestCut.KernelApprox.profile_le_inv_sq line 23
  5. lemma OAI.UniformSparsestCut.KernelApprox.profile_pos line 29
  6. lemma OAI.UniformSparsestCut.KernelApprox.profile_measurable line 34
  7. lemma OAI.UniformSparsestCut.KernelApprox.profile_integrable_lower line 36
  8. lemma OAI.UniformSparsestCut.KernelApprox.profile_integrable_upper line 42
  9. lemma OAI.UniformSparsestCut.KernelApprox.profile_integrable line 53
  10. def OAI.UniformSparsestCut.KernelApprox.cstar line 57
  11. lemma OAI.UniformSparsestCut.KernelApprox.cstar_pos line 59
  12. def OAI.UniformSparsestCut.KernelApprox.scaled line 70
  13. lemma OAI.UniformSparsestCut.KernelApprox.scaled_eq_profile line 72
  14. lemma OAI.UniformSparsestCut.KernelApprox.scaled_nonneg line 81
  15. lemma OAI.UniformSparsestCut.KernelApprox.scaled_le_one line 84
  16. lemma OAI.UniformSparsestCut.KernelApprox.scaled_le_tail line 87
  17. lemma OAI.UniformSparsestCut.KernelApprox.scaled_measurable line 93
  18. lemma OAI.UniformSparsestCut.KernelApprox.scaled_integrable_lower line 95
  19. lemma OAI.UniformSparsestCut.KernelApprox.scaled_integrable_upper line 102
  20. lemma OAI.UniformSparsestCut.KernelApprox.scaled_integrable line 113
  21. lemma OAI.UniformSparsestCut.KernelApprox.full_integral line 118
  22. lemma OAI.UniformSparsestCut.KernelApprox.lower_tail_bound line 127
  23. lemma OAI.UniformSparsestCut.KernelApprox.upper_tail_bound line 134
  24. lemma OAI.UniformSparsestCut.KernelApprox.truncated_error line 150