OAI/Analysis/SegmentLenses/FiniteLaws.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite probability laws and joint square-root budgets

  1. theorem OAI.SegmentLenses.joint_sqrt_bound line 19
  2. theorem OAI.SegmentLenses.joint_budget_tail line 34
  3. structure OAI.SegmentLenses.FiniteLaw line 46
  4. def OAI.SegmentLenses.FiniteLaw.mean line 54
  5. theorem OAI.SegmentLenses.FiniteLaw.mean_const line 56
  6. theorem OAI.SegmentLenses.FiniteLaw.mean_add line 59
  7. theorem OAI.SegmentLenses.FiniteLaw.mean_sub line 63
  8. theorem OAI.SegmentLenses.FiniteLaw.mean_mul line 67
  9. theorem OAI.SegmentLenses.FiniteLaw.mean_nonneg line 71
  10. theorem OAI.SegmentLenses.FiniteLaw.mean_mono line 74
  11. theorem OAI.SegmentLenses.FiniteLaw.sq_mean_le line 79
  12. theorem OAI.SegmentLenses.FiniteLaw.joint_identity line 96