OAI/Analysis/CircleDomains/Probability/HitFusionTree.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.ClosedHitCandidate line 23
  2. theorem OAI.CircleDomainRigidity.ClosedHitCandidate.nonempty line 34
  3. structure OAI.CircleDomainRigidity.HitFusionSplit line 40
  4. theorem OAI.CircleDomainRigidity.nonempty_hitFusionSplit line 55
  5. def OAI.CircleDomainRigidity.HitFusionSplit.index line 74

    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.HitFusionSplit

  6. theorem OAI.CircleDomainRigidity.HitFusionSplit.index_val line 79
  7. def OAI.CircleDomainRigidity.hitFusionNode line 91
  8. def OAI.CircleDomainRigidity.hitFusionScheme line 96
  9. structure OAI.CircleDomainRigidity.HitFusionData line 104

    Source documentation

    The data generated by the proved finite splitting construction.

    structure HitFusionData where
…
  10. def OAI.CircleDomainRigidity.HitFusionData.node line 116
  11. def OAI.CircleDomainRigidity.HitFusionData.scheme line 119
  12. def OAI.CircleDomainRigidity.HitFusionData.splitAt line 122
  13. theorem OAI.CircleDomainRigidity.HitFusionData.node_cons line 126