OAI/Analysis/CircleDomains/Probability/HitFusionCaps.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform upper bounds on a closed child control every continuation of a fusion branch. The weighted sum of these bounds is the original split bound.

  1. def OAI.CircleDomainRigidity.HitFusionSplit.hitCap line 25
  2. theorem OAI.CircleDomainRigidity.HitFusionSplit.hitCap_bddAbove line 30
  3. theorem OAI.CircleDomainRigidity.HitFusionSplit.le_hitCap line 37
  4. theorem OAI.CircleDomainRigidity.HitFusionSplit.hitCap_nonneg line 44
  5. theorem OAI.CircleDomainRigidity.HitFusionSplit.hitCap_le_card line 50
  6. theorem OAI.CircleDomainRigidity.HitFusionSplit.weighted_hitCap_le line 57