OAI/InformationTheory/SoftChannel/CurvatureCertificates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureBernstein line 15
  2. theorem OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureBernstein_pos line 36
  3. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureChunk0 line 39
  4. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureExpanded0 line 42
  5. lemma OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureChunk0_eq line 63
  6. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureChunk1 line 67
  7. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureExpanded1 line 70
  8. lemma OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureChunk1_eq line 86
  9. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureChunk2 line 90
  10. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureExpanded2 line 93
  11. lemma OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureChunk2_eq line 104
  12. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureChunk3 line 108
  13. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureExpanded3 line 111
  14. lemma OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_curvatureChunk3_eq line 117
  15. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_lambdaBernsteinLow line 121
  16. def OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_lambdaBernsteinHigh line 132
  17. theorem OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_lambdaBernsteinLow_pos line 143
  18. theorem OAI.LeanBlast.CourtadeKumar.CurvatureCertificates_lambdaBernsteinHigh_pos line 146