OAI/Analysis/FourierLLogL/Plateau/Features.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Finite joint observation moments

  1. def OAI.FourierLLogL.Dyadic.Procedure.share line 15
  2. def OAI.FourierLLogL.Dyadic.Procedure.ante line 16
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.ante_nonneg line 18
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.ante_total line 20
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.ante_split line 22
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.share_split line 38
  7. def OAI.FourierLLogL.Dyadic.Procedure.Packet line 43
  8. def OAI.FourierLLogL.Dyadic.Procedure.addMass line 45
  9. def OAI.FourierLLogL.Dyadic.Procedure.rung line 48
  10. def OAI.FourierLLogL.Dyadic.Procedure.rungC line 51
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.nonnegative_hist line 54
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.total_hist line 58
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.rung_mono line 65
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.rung_const line 71
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.rung_add line 78
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.rung_lmul line 82
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.rung_error line 87
  18. lemma OAI.FourierLLogL.Dyadic.Procedure.rung_hist line 99
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.rung_split line 104
  20. lemma OAI.FourierLLogL.Dyadic.Procedure.hist_split line 113
  21. lemma OAI.FourierLLogL.Dyadic.Procedure.hist_le line 122
  22. lemma OAI.FourierLLogL.Dyadic.Procedure.fisher_range line 130
  23. lemma OAI.FourierLLogL.Dyadic.Procedure.fz_split line 145