OAI/Analysis/FourierLLogL/Thermal/Posterior.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Past observation profiles and posterior lower bound

  1. abbrev OAI.FourierLLogL.Dyadic.Thermal.Profile line 16
  2. def OAI.FourierLLogL.Dyadic.Thermal.sumE line 19

    Source documentation

    Energy of a history against test input.

    def sumE (s : Profile M) (x : Grid M) : ℝ := (s.map fun t => form t.1 (t.2-x)).sum

    Mentions: OAI.FourierLLogL.Dyadic.Thermal.Profile, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Thermal.form

  3. def OAI.FourierLLogL.Dyadic.Thermal.mixForm line 20
  4. def OAI.FourierLLogL.Dyadic.Thermal.tune line 21
  5. def OAI.FourierLLogL.Dyadic.Thermal.admissible line 23
  6. def OAI.FourierLLogL.Dyadic.Thermal.prefixE line 26
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.tune_pos line 28
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.prefixE_nonneg line 29
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.tune_cons line 34
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.mix_cons line 39
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.mix_bound line 42
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.mix_nonneg line 57
  13. lemma OAI.FourierLLogL.Dyadic.Thermal.sumE_compare line 65
  14. lemma OAI.FourierLLogL.Dyadic.Thermal.profile_envelope line 79
  15. lemma OAI.FourierLLogL.Dyadic.Thermal.close_kept line 97
  16. lemma OAI.FourierLLogL.Dyadic.Thermal.even_prob line 125
  17. lemma OAI.FourierLLogL.Dyadic.Thermal.label_node_inside line 132
  18. lemma OAI.FourierLLogL.Dyadic.Thermal.posterior_denominator line 169