OAI/Analysis/FourierLLogL/Procedure/Play.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The finite spatial and spectral play

  1. structure OAI.FourierLLogL.Dyadic.Procedure.Scene line 16
  2. def OAI.FourierLLogL.Dyadic.Procedure.cutoff line 23
  3. def OAI.FourierLLogL.Dyadic.Procedure.Scene.mass line 26
  4. def OAI.FourierLLogL.Dyadic.Procedure.Scene.actor line 27
  5. def OAI.FourierLLogL.Dyadic.Procedure.Scene.openHere line 30
  6. def OAI.FourierLLogL.Dyadic.Procedure.Scene.retire line 32
  7. def OAI.FourierLLogL.Dyadic.Procedure.Scene.enter line 34
  8. def OAI.FourierLLogL.Dyadic.Procedure.Scene.work line 35
  9. def OAI.FourierLLogL.Dyadic.Procedure.Scene.settled line 37
  10. def OAI.FourierLLogL.Dyadic.Procedure.Scene.reset line 41
  11. def OAI.FourierLLogL.Dyadic.Procedure.Scene.out line 42
  12. def OAI.FourierLLogL.Dyadic.Procedure.Scene.smaller line 43
  13. def OAI.FourierLLogL.Dyadic.Procedure.Scene.win line 44
  14. def OAI.FourierLLogL.Dyadic.Procedure.Scene.lose line 48
  15. def OAI.FourierLLogL.Dyadic.Procedure.Scene.beginPlay line 53
  16. structure OAI.FourierLLogL.Dyadic.Procedure.Scene.Safe line 60
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.Scene.actor_def line 71
  18. lemma OAI.FourierLLogL.Dyadic.Procedure.Scene.Safe.mass_lower line 78
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.Scene.Safe.mass_upper line 80
  20. lemma OAI.FourierLLogL.Dyadic.Procedure.Scene.Safe.budget line 83
  21. inductive OAI.FourierLLogL.Dyadic.Procedure.Play line 90
  22. def OAI.FourierLLogL.Dyadic.Procedure.Play.Follows line 102
  23. lemma OAI.FourierLLogL.Dyadic.Procedure.Play.first line 113