OAI/Analysis/FourierLLogL/Thermal/History.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Thermal certificates and tightening

  1. def OAI.FourierLLogL.Dyadic.Thermal.place line 15
  2. lemma OAI.FourierLLogL.Dyadic.Thermal.place_valid line 17
  3. lemma OAI.FourierLLogL.Dyadic.Thermal.loc_scale line 19
  4. lemma OAI.FourierLLogL.Dyadic.Thermal.place_internal line 21
  5. def OAI.FourierLLogL.Dyadic.Thermal.flat line 32

    Source documentation

    A plate distributes the free energy cost over a long range of factors.

    def flat (h err : ℝ) (A D : Form M) : Prop :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Thermal.Form

  6. structure OAI.FourierLLogL.Dyadic.Thermal.Certified line 36

    Source documentation

    certificate of a main form. n is the addition count and p the latest interval.

    structure Certified (h err : ℝ) (n : ℕ) (p : Node) (A : Form M) : Prop where
…

    Mentions: OAI.FourierLLogL.Dyadic.Node, OAI.FourierLLogL.Dyadic.Thermal.Form

  7. lemma OAI.FourierLLogL.Dyadic.Thermal.certified_start line 44
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.certified_add line 49
  9. def OAI.FourierLLogL.Dyadic.Thermal.tilde line 140

    Source documentation

    tightening used by compression and evidence posterior bounds.

    def tilde (h : ℝ) (A : Form M) (p : Node) : Form M :=
…

    Mentions: OAI.FourierLLogL.Dyadic.Thermal.Form, OAI.FourierLLogL.Dyadic.Node

  10. lemma OAI.FourierLLogL.Dyadic.Thermal.tilde_le line 143
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.tilde_tight line 148
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.space_increment line 174