OAI/Analysis/CircleDomains/Probability/MarkedHitFusionLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The law on the nested tree and its continuous limiting mixture. Every scheduled configuration bound survives all subsequent refinements.

  1. def OAI.CircleDomainRigidity.MarkedHit.HitFusionData.step line 25
  2. def OAI.CircleDomainRigidity.MarkedHit.HitFusionData.childCap line 28
  3. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.childCap_bddAbove line 33
  4. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.le_childCap line 40
  5. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.childCap_nonneg line 47
  6. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.childCap_le_card line 54
  7. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.integral_childCap_le line 62
  8. def OAI.CircleDomainRigidity.MarkedHit.HitFusionData.endpoint line 70
  9. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.continuous_endpoint line 74
  10. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.endpoint_mem line 79
  11. def OAI.CircleDomainRigidity.MarkedHit.HitFusionData.addressLaw line 83
  12. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.integral_endpoint_hits_le line 87