OAI/Probability/SKGap/Localization/EqualityCurve.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.scalarCurve line 14
  2. def OAI.SKGap.scalarBMoment line 17
  3. def OAI.SKGap.scalarEMoment line 19
  4. lemma OAI.SKGap.scalarBMoment_integral line 21
  5. lemma OAI.SKGap.scalarEMoment_integral line 27
  6. lemma OAI.SKGap.scalarBMoment_pos line 34
  7. lemma OAI.SKGap.scalarBMoment_le_one line 43
  8. lemma OAI.SKGap.scalarEMoment_nonneg line 48
  9. lemma OAI.SKGap.continuous_scalarBMoment line 52
  10. lemma OAI.SKGap.continuous_scalarEMoment line 53
  11. lemma OAI.SKGap.continuous_scalarFixedPoint_nonneg line 55
  12. lemma OAI.SKGap.continuous_scalarCurve_nonneg line 66
  13. lemma OAI.SKGap.scalarQMoment_curve line 76
  14. lemma OAI.SKGap.scalarM_curve line 79
  15. lemma OAI.SKGap.scalarD_curve line 86
  16. lemma OAI.SKGap.scalarS_curve line 91
  17. lemma OAI.SKGap.scalarA_curve line 96
  18. lemma OAI.SKGap.scalarMomentGram_curve line 119
  19. lemma OAI.SKGap.GaussianDensity.map_withDensity_leftInverse line 140
  20. theorem OAI.SKGap.GaussianDensity.matrix_map_gaussian_density line 154