OAI/Probability/SKRatio/Matrices/UnitBall.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatioGaussian.quadratic_interpolation line 56
  2. abbrev OAI.SKRatioGaussian.UnitBall line 67
  3. instance OAI.SKRatioGaussian.(instance at line 70) line 70
  4. lemma OAI.SKRatioGaussian.norm_UnitBall_le line 72
  5. def OAI.SKRatioGaussian.diagonalOffset line 75
  6. def OAI.SKRatioGaussian.diagonalProcess line 78
  7. def OAI.SKRatioGaussian.diagonalLinearProcess line 83
  8. def OAI.SKRatioGaussian.diagonalWeights line 88
  9. def OAI.SKRatioGaussian.diagonalT line 92
  10. lemma OAI.SKRatioGaussian.continuous_diagonalOffset line 95
  11. lemma OAI.SKRatioGaussian.continuous_diagonalCoeff line 99
  12. lemma OAI.SKRatioGaussian.integrable_diagonalProcess line 107
  13. lemma OAI.SKRatioGaussian.integrable_diagonalLinearProcess line 112
  14. lemma OAI.SKRatioGaussian.diagonalT_norm line 117
  15. lemma OAI.SKRatioGaussian.diagonalWeights_sum line 128
  16. lemma OAI.SKRatioGaussian.diagonalWeights_sum_sq line 133
  17. lemma OAI.SKRatioGaussian.diagonalT_integrable line 138
  18. lemma OAI.SKRatioGaussian.diagonalT_fluctuation line 150
  19. lemma OAI.SKRatioGaussian.diagonalLinearProcess_le line 166
  20. theorem OAI.SKRatioGaussian.diagonalProcess_expected_margin line 217
  21. lemma OAI.SKRatioGaussian.diagonalProcess_lipschitz line 249
  22. theorem OAI.SKRatioGaussian.diagonalProcess_path_le line 270