OAI/Analysis/FourierLLogL/Procedure/Likelihood.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Likelihood estimates through any terminal step

  1. lemma OAI.FourierLLogL.Dyadic.Procedure.cutoff_log line 15
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Journal.fee_neg line 31
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Journal.fee_div_sub line 39
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.minus_like_cap line 52
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.half_debit_cap line 70
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.negative_square line 106
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.neg_like_budget line 117
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.spent_top line 125
  9. def OAI.FourierLLogL.Dyadic.Procedure.Road.limitC line 135
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.mem_budget line 137
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Road.log_mass_budget line 188