OAI/Probability/Ballisticity/Estimates/ProtectionLoss.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.cappedLogLoss_eq_neg_log line 14
  2. lemma OAI.DirectionalTransience.exp_neg_cappedLogLoss line 21
  3. lemma OAI.DirectionalTransience.first_protection_failure_split line 36
  4. def OAI.DirectionalTransience.protectionHeight line 77
  5. def OAI.DirectionalTransience.protectionGap line 81
  6. lemma OAI.DirectionalTransience.protectionHeight_mono line 85
  7. lemma OAI.DirectionalTransience.protectionHeight_eq line 90
  8. lemma OAI.DirectionalTransience.protectionGap_eq line 96
  9. def OAI.DirectionalTransience.protectionProfile line 102
  10. lemma OAI.DirectionalTransience.protectionProfile_measurable line 111
  11. def OAI.DirectionalTransience.protectionFiltration line 121
  12. def OAI.DirectionalTransience.protectionMass line 127
  13. lemma OAI.DirectionalTransience.protectionMass_measurable line 132
  14. lemma OAI.DirectionalTransience.protectionMass_bounds line 145
  15. lemma OAI.DirectionalTransience.protection_capped_step line 151
  16. theorem OAI.DirectionalTransience.protection_capped_sum_tail line 174