OAI/Analysis/FourierLLogL/Procedure/Rating.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The score includes sizeable payments even conditional on the actual input

  1. def OAI.FourierLLogL.Dyadic.Procedure.Road.tempered line 19

    Source documentation

    Require each batch's total own-energy below temp; at success the available past temp is expanded.

    def tempered (m : Memory M) (j : ℕ) (s : Scene M) (x : Grid M) :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Memory, OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Grid

  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.temperature line 22
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.good_payment line 32
  4. def OAI.FourierLLogL.Dyadic.Procedure.Road.rating line 90
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.stake_lower line 93