OAI/Probability/SKGap/Localization/UnitBall.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.quadratic_interpolation line 54
  2. abbrev OAI.SKGap.UnitBall line 65
  3. instance OAI.SKGap.(instance at line 68) line 68
  4. lemma OAI.SKGap.norm_UnitBall_le line 70
  5. def OAI.SKGap.diagonalOffset line 73
  6. def OAI.SKGap.diagonalProcess line 76
  7. def OAI.SKGap.diagonalLinearProcess line 81
  8. def OAI.SKGap.diagonalWeights line 86
  9. def OAI.SKGap.diagonalT line 90
  10. lemma OAI.SKGap.continuous_diagonalOffset line 93
  11. lemma OAI.SKGap.continuous_diagonalCoeff line 97
  12. lemma OAI.SKGap.integrable_diagonalProcess line 105
  13. lemma OAI.SKGap.integrable_diagonalLinearProcess line 110
  14. lemma OAI.SKGap.diagonalT_norm line 115
  15. lemma OAI.SKGap.diagonalWeights_sum line 126
  16. lemma OAI.SKGap.diagonalWeights_sum_sq line 131
  17. lemma OAI.SKGap.diagonalT_integrable line 136
  18. lemma OAI.SKGap.diagonalT_fluctuation line 148
  19. lemma OAI.SKGap.diagonalLinearProcess_le line 164
  20. theorem OAI.SKGap.diagonalProcess_expected_margin line 215
  21. lemma OAI.SKGap.diagonalProcess_lipschitz line 247
  22. theorem OAI.SKGap.diagonalProcess_path_le line 268