OAI/Analysis/FourierLLogL/Procedure/Memory.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Observation records in the comparison proof

  1. structure OAI.FourierLLogL.Dyadic.Procedure.Memory line 15
  2. def OAI.FourierLLogL.Dyadic.Procedure.Memory.piece line 20
  3. def OAI.FourierLLogL.Dyadic.Procedure.Memory.stash line 23
  4. structure OAI.FourierLLogL.Dyadic.Procedure.Memory.Ready line 26
  5. def OAI.FourierLLogL.Dyadic.Procedure.Memory.temp line 32
  6. def OAI.FourierLLogL.Dyadic.Procedure.Memory.loadE line 34
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Memory.stash_ready line 37
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Memory.stash_length_bound line 55
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Memory.sumE_piece line 62
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Memory.sumE_stash line 67
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Memory.form_in_past line 72
  12. def OAI.FourierLLogL.Dyadic.Procedure.Memory.stashRate line 92
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Memory.multiply_stash line 95
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Memory.rate_positive line 115
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Memory.batch_expected line 118
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Memory.batch_scale line 127