OAI/Analysis/FourierLLogL/Compress/Observe.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The block observation

  1. def OAI.FourierLLogL.Compress.sumLaw line 16
  2. lemma OAI.FourierLLogL.Compress.full_pair line 19
  3. lemma OAI.FourierLLogL.Compress.G_as_sum line 25
  4. lemma OAI.FourierLLogL.Compress.I_single line 30
  5. lemma OAI.FourierLLogL.Compress.K_as_sum line 34
  6. def OAI.FourierLLogL.Compress.sumPlus line 38
  7. def OAI.FourierLLogL.Compress.rowPlus line 42
  8. lemma OAI.FourierLLogL.Compress.sumLaw_succ line 45
  9. abbrev OAI.FourierLLogL.Compress.observe line 56
  10. lemma OAI.FourierLLogL.Compress.observe_refines line 60
  11. lemma OAI.FourierLLogL.Compress.rowPlus_inj line 70
  12. lemma OAI.FourierLLogL.Compress.observe_row_ent line 76
  13. lemma OAI.FourierLLogL.Compress.observe_cost line 106
  14. lemma OAI.FourierLLogL.Compress.observe_cond line 113
  15. lemma OAI.FourierLLogL.Compress.observe_save line 171