OAI/Probability/SKGap/Brownian/PathParameter.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.sqrt_parameter_holder line 14
  2. lemma OAI.SKGap.pathDiagonal_parameter line 32
  3. lemma OAI.SKGap.mean_parameter line 39
  4. lemma OAI.SKGap.pathShift_parameter line 50
  5. lemma OAI.SKGap.ComplexMatrix.spectralShift_difference line 61
  6. lemma OAI.SKGap.ComplexMatrix.complex_product_bound line 63
  7. lemma OAI.SKGap.ComplexMatrix.complex_triple_bound line 67
  8. lemma OAI.SKGap.ComplexMatrix.complex_sum_three_bound line 72
  9. lemma OAI.SKGap.ComplexMatrix.spectralShift_parameter line 76
  10. lemma OAI.SKGap.parameter_sqrt_small line 101
  11. lemma OAI.SKGap.path_parameter_factors line 105
  12. theorem OAI.SKGap.pathK_parameter_holder line 146