OAI/Analysis/FourierLLogL/Compress/Fraction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Partial refinements

  1. lemma OAI.FourierLLogL.Compress.mix_send line 14
  2. lemma OAI.FourierLLogL.Compress.marked_cond line 20
  3. def OAI.FourierLLogL.Compress.retag line 53
  4. lemma OAI.FourierLLogL.Compress.retag_inj line 56
  5. abbrev OAI.FourierLLogL.Compress.blend line 61
  6. lemma OAI.FourierLLogL.Compress.blend_refines line 65
  7. lemma OAI.FourierLLogL.Compress.retag_Hcond line 76
  8. lemma OAI.FourierLLogL.Compress.blend_H line 82
  9. def OAI.FourierLLogL.Compress.upRows line 95
  10. def OAI.FourierLLogL.Compress.packedH line 98
  11. lemma OAI.FourierLLogL.Compress.retag_trial line 101
  12. lemma OAI.FourierLLogL.Compress.retag_trial_rows line 125
  13. lemma OAI.FourierLLogL.Compress.exact_rent line 130
  14. lemma OAI.FourierLLogL.Compress.blend_I line 137
  15. lemma OAI.FourierLLogL.Compress.blend_G1 line 163