OAI/Analysis/CircleDomains/Probability/HitFusionLaw.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.HitFusionData.step line 24
  2. def OAI.CircleDomainRigidity.HitFusionData.childCap line 27
  3. theorem OAI.CircleDomainRigidity.HitFusionData.childCap_bddAbove line 32
  4. theorem OAI.CircleDomainRigidity.HitFusionData.le_childCap line 39
  5. theorem OAI.CircleDomainRigidity.HitFusionData.childCap_nonneg line 46
  6. theorem OAI.CircleDomainRigidity.HitFusionData.childCap_le_card line 53
  7. theorem OAI.CircleDomainRigidity.HitFusionData.integral_childCap_le line 61
  8. def OAI.CircleDomainRigidity.HitFusionData.endpoint line 69
  9. theorem OAI.CircleDomainRigidity.HitFusionData.continuous_endpoint line 73
  10. theorem OAI.CircleDomainRigidity.HitFusionData.endpoint_mem line 78
  11. def OAI.CircleDomainRigidity.HitFusionData.addressLaw line 82
  12. theorem OAI.CircleDomainRigidity.HitFusionData.integral_endpoint_hits_le line 86