OAI/Analysis/CircleDomains/Probability/MarkedHitFusionCaps.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.MarkedHit.HitFusionSplit.hitCap line 26
  2. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionSplit.hitCap_bddAbove line 31
  3. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionSplit.le_hitCap line 38
  4. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionSplit.hitCap_nonneg line 45
  5. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionSplit.hitCap_le_card line 51
  6. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionSplit.weighted_hitCap_le line 58