OAI/Combinatorics/SumProduct/Alignment/ProductExposure03.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ProductExposureCutoff.badBin line 18
  2. lemma OAI.ProductExposureCutoff.bad_bin_geometry line 22
  3. lemma OAI.ProductExposureCutoff.bad_bin_subset_cutoff line 54
  4. lemma OAI.ProductExposureCutoff.raw_bad_bin_le_cutoff line 66
  5. theorem OAI.ProductExposureCutoff.raw_bad_bin_decay line 84
  6. def OAI.ProductExposureLabels.Good line 108
  7. lemma OAI.ProductExposureLabels.tail_marginal line 113
  8. lemma OAI.ProductExposureLabels.pivot_marginal line 123
  9. lemma OAI.ProductExposureLabels.law_ae_units line 131
  10. lemma OAI.ProductExposureLabels.joint_ae_domain line 138
  11. lemma OAI.ProductExposureLabels.joint_restrict_domain line 156
  12. lemma OAI.ProductExposureLabels.expose_bounds line 165
  13. lemma OAI.ProductExposureLabels.product_dyadic_bounds line 174
  14. lemma OAI.ProductExposureLabels.good_of_not_cutoff line 184
  15. lemma OAI.ProductExposureLabels.bad_good_bound line 222
  16. theorem OAI.ProductExposureLabels.raw_good_decay line 246