OAI/Combinatorics/SumProduct/Alignment/ProductExposure01.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MicrocellEarlierScale.radius_dominates_square line 27
  2. lemma OAI.MicrocellEarlierScale.length_cast line 64
  3. theorem OAI.MicrocellEarlierScale.length_tendsto line 69
  4. theorem OAI.AdmissibleRawSuccess.eventually_global line 105
  5. def OAI.ProductExposureLaw.jointLaw line 181
  6. instance OAI.ProductExposureLaw.jointLaw_probability line 186
  7. def OAI.ProductExposureLaw.jointFiber line 192
  8. lemma OAI.ProductExposureLaw.law_singleton line 199
  9. lemma OAI.ProductExposureLaw.joint_singleton_mem line 205
  10. lemma OAI.ProductExposureLaw.joint_fiber_mass line 229
  11. theorem OAI.ProductExposureLaw.conditional_exact line 255