OAI/Combinatorics/SparsestCut/GaussianCDF.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformSparsestCut.GaussianCDF.Φ line 12
  2. def OAI.UniformSparsestCut.GaussianCDF.φ line 13
  3. lemma OAI.UniformSparsestCut.GaussianCDF.φ_pos line 15
  4. lemma OAI.UniformSparsestCut.GaussianCDF.φ_contDiff line 16
  5. lemma OAI.UniformSparsestCut.GaussianCDF.φ_integrable line 17
  6. lemma OAI.UniformSparsestCut.GaussianCDF.Φ_integral line 18
  7. lemma OAI.UniformSparsestCut.GaussianCDF.Φ_primitive line 22
  8. lemma OAI.UniformSparsestCut.GaussianCDF.Φ_hasDeriv line 28
  9. lemma OAI.UniformSparsestCut.GaussianCDF.Φ_continuous line 37
  10. lemma OAI.UniformSparsestCut.GaussianCDF.Φ_strictMono line 38
  11. lemma OAI.UniformSparsestCut.GaussianCDF.Φ_mem line 39
  12. lemma OAI.UniformSparsestCut.GaussianCDF.Φ_surj line 44
  13. lemma OAI.UniformSparsestCut.GaussianCDF.Φ_map line 49
  14. def OAI.UniformSparsestCut.GaussianCDF.ψ line 71
  15. lemma OAI.UniformSparsestCut.GaussianCDF.ψ_hasDeriv line 72
  16. lemma OAI.UniformSparsestCut.GaussianCDF.ψ_mem line 73
  17. lemma OAI.UniformSparsestCut.GaussianCDF.ψ_contDiff line 77
  18. lemma OAI.UniformSparsestCut.GaussianCDF.ψ_deriv_bound line 85
  19. def OAI.UniformSparsestCut.GaussianCDF.uniform line 98
  20. lemma OAI.UniformSparsestCut.GaussianCDF.ψ_map line 100
  21. instance OAI.UniformSparsestCut.GaussianCDF.uniform_probability line 136