OAI/Analysis/FourierLLogL/Thermal/Update.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Update records and validity

  1. structure OAI.FourierLLogL.Dyadic.Thermal.Update line 18

    Source documentation

    Data determining an update.

    structure Update (j M : ℕ) (p : Node) where
…

    Mentions: OAI.FourierLLogL.Dyadic.Node

  2. def OAI.FourierLLogL.Dyadic.Thermal.Update.adjust line 30
  3. def OAI.FourierLLogL.Dyadic.Thermal.Update.changeForm line 31
  4. def OAI.FourierLLogL.Dyadic.Thermal.Update.next line 33
  5. def OAI.FourierLLogL.Dyadic.Thermal.Update.app line 34
  6. def OAI.FourierLLogL.Dyadic.Thermal.Update.tiltMean line 39

    Source documentation

    At a regular attempt membership uses the specified old-channel conditional mean, never a sample.

    def tiltMean (u : Update j M p) (A : Form M) (y : Grid M) : ℂ :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Thermal.Update, OAI.FourierLLogL.Dyadic.Thermal.Form, OAI.FourierLLogL.Dyadic.Grid

  7. def OAI.FourierLLogL.Dyadic.Thermal.Update.take line 41
  8. def OAI.FourierLLogL.Dyadic.Thermal.Update.chances line 43
  9. def OAI.FourierLLogL.Dyadic.Thermal.Update.encoded line 44
  10. def OAI.FourierLLogL.Dyadic.Thermal.Update.bill line 45
  11. structure OAI.FourierLLogL.Dyadic.Thermal.Update.Good line 47
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.Update.chance_bias line 64
  13. lemma OAI.FourierLLogL.Dyadic.Thermal.paid_tighten line 102
  14. lemma OAI.FourierLLogL.Dyadic.Thermal.make_update line 113