OAI/Probability/Localization/Rewards.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RepeatedLocalization.FiniteEntropy.complementMass line 12
  2. def OAI.RepeatedLocalization.FiniteEntropy.complementReward line 15
  3. def OAI.RepeatedLocalization.FiniteEntropy.continuingReward line 18
  4. def OAI.RepeatedLocalization.FiniteEntropy.accumulate line 21
  5. def OAI.RepeatedLocalization.FiniteEntropy.rewardLog line 26
  6. def OAI.RepeatedLocalization.FiniteEntropy.complementTotal line 29
  7. def OAI.RepeatedLocalization.FiniteEntropy.continuingTotal line 32
  8. def OAI.RepeatedLocalization.FiniteEntropy.truncatedDepth line 35
  9. def OAI.RepeatedLocalization.FiniteEntropy.truncatedAttempts line 38
  10. def OAI.RepeatedLocalization.FiniteEntropy.activeIndicator line 41
  11. lemma OAI.RepeatedLocalization.FiniteEntropy.accumulate_append line 44
  12. lemma OAI.RepeatedLocalization.FiniteEntropy.rewardLog_append line 51
  13. lemma OAI.RepeatedLocalization.FiniteEntropy.complementMass_nonneg line 56
  14. lemma OAI.RepeatedLocalization.FiniteEntropy.complementMass_le_one line 59
  15. lemma OAI.RepeatedLocalization.FiniteEntropy.complementReward_nonneg line 66
  16. lemma OAI.RepeatedLocalization.FiniteEntropy.continuingReward_nonneg line 75
  17. lemma OAI.RepeatedLocalization.FiniteEntropy.accumulate_nonneg line 78
  18. lemma OAI.RepeatedLocalization.FiniteEntropy.rewardLog_nonneg line 84
  19. lemma OAI.RepeatedLocalization.FiniteEntropy.neg_log_mul_le line 88
  20. lemma OAI.RepeatedLocalization.FiniteEntropy.threshold_pos line 98
  21. lemma OAI.RepeatedLocalization.FiniteEntropy.log_threshold line 100
  22. lemma OAI.RepeatedLocalization.FiniteEntropy.positive_event_descendant line 103
  23. lemma OAI.RepeatedLocalization.FiniteEntropy.state_event_append_subset line 108
  24. lemma OAI.RepeatedLocalization.FiniteEntropy.cond_event_mul line 116
  25. lemma OAI.RepeatedLocalization.FiniteEntropy.path_label_surprisal line 123