OAI/Analysis/FourierLLogL/Procedure/Fisher.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Dyadic.Procedure.local_deficit_dry line 16

   Source documentation

   locally charge entropy to height. useful for static.

   lemma local_deficit_dry (s : Scene M) {α : Type} [Fintype α] (P : Law α)
       (hp : s.here.ok M) (hh : 0 ≤ s.wage) (hm : 0 < s.mass)
       (d : ℝ) (h : ∀ x, s.wage x ≤ exp d) :
       deficit s (fun _ => P) ≤ d-log s.mass := by
   …

   Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Law, OAI.FourierLLogL.Dyadic.Procedure.deficit

2. lemma OAI.FourierLLogL.Dyadic.Procedure.no_label line 51
3. def OAI.FourierLLogL.Dyadic.Procedure.givenD line 55
4. def OAI.FourierLLogL.Dyadic.Procedure.massInfo line 57
5. def OAI.FourierLLogL.Dyadic.Procedure.Event.infoFee line 61
6. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.one_split_price line 68
7. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.fisher_bound line 118