OAI/Analysis/FourierLLogL/Thermal/Alarm.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Probability cost of clone evidence under the comparison model

  1. def OAI.FourierLLogL.Dyadic.Thermal.cushion line 15
  2. def OAI.FourierLLogL.Dyadic.Thermal.clones line 16
  3. abbrev OAI.FourierLLogL.Dyadic.Thermal.Clutch line 18
  4. def OAI.FourierLLogL.Dyadic.Thermal.fresh line 20
  5. def OAI.FourierLLogL.Dyadic.Thermal.Update.consistent line 26
  6. def OAI.FourierLLogL.Dyadic.Thermal.Update.single line 29
  7. def OAI.FourierLLogL.Dyadic.Thermal.Update.alarm line 32
  8. def OAI.FourierLLogL.Dyadic.Thermal.Update.alarmQ line 36
  9. def OAI.FourierLLogL.Dyadic.Thermal.Update.singleQ line 39
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.Update.alarm_le line 42
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.Update.shift_app line 66
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.Update.one_moment line 73
  13. lemma OAI.FourierLLogL.Dyadic.Thermal.Update.consistent_length line 124
  14. theorem OAI.FourierLLogL.Dyadic.Thermal.Update.one_clone_tail line 143