OAI/Probability/SKGap/Brownian/PathAgreement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.pathDiagonal_square line 15
  2. lemma OAI.SKGap.pathShift_one line 23
  3. lemma OAI.SKGap.symmetric_isUnit_of_lower line 27
  4. lemma OAI.SKGap.pathK_agrees line 34
  5. lemma OAI.SKGap.inverse_resolvent_relations line 50
  6. lemma OAI.SKGap.path_bilinear_agreement line 76
  7. def OAI.SKGap.pathFeature line 123
  8. def OAI.SKGap.pathFeatureLip line 127
  9. lemma OAI.SKGap.pathFeatureLip_nonneg line 130
  10. lemma OAI.SKGap.pathFeature_lip line 136
  11. lemma OAI.SKGap.pathFeature_sign line 151
  12. theorem OAI.SKGap.actual_path_affine_tail line 157