OAI/Analysis/CircleDomains/Probability/MarkedHitFusionTree.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual nested tree of nonsmall closed candidates. Every vertex carries its finite probability split, and every infinite address has a continuous limit inside every ancestor.

  1. structure OAI.CircleDomainRigidity.MarkedHit.ClosedHitCandidate line 24
  2. theorem OAI.CircleDomainRigidity.MarkedHit.ClosedHitCandidate.nonempty line 35
  3. structure OAI.CircleDomainRigidity.MarkedHit.HitFusionSplit line 41
  4. theorem OAI.CircleDomainRigidity.MarkedHit.nonempty_hitFusionSplit line 56
  5. def OAI.CircleDomainRigidity.MarkedHit.HitFusionSplit.index line 77

    Source documentation

    All natural-number addresses are valid; only the first count receive mass.

    def index (S : HitFusionSplit ι law C A n r ε η) (a : ℕ) : Fin S.count :=
…

    Mentions: OAI.CircleDomainRigidity.MarkedHit.HitFusionSplit

  6. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionSplit.index_val line 82
  7. def OAI.CircleDomainRigidity.MarkedHit.hitFusionNode line 94
  8. def OAI.CircleDomainRigidity.MarkedHit.hitFusionScheme line 99
  9. structure OAI.CircleDomainRigidity.MarkedHit.HitFusionData line 107

    Source documentation

    The data generated by the proved finite splitting construction.

    structure HitFusionData where
…
  10. def OAI.CircleDomainRigidity.MarkedHit.HitFusionData.node line 121
  11. def OAI.CircleDomainRigidity.MarkedHit.HitFusionData.scheme line 124
  12. def OAI.CircleDomainRigidity.MarkedHit.HitFusionData.splitAt line 127
  13. theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.node_cons line 131