OAI/Probability/FKMaps/ConditionedTrees.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_singleton line 11
2. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.marked_singleton line 16
3. lemma OAI.FKCRT.Inventory.CoreTree.word_length_degrees line 35
4. lemma OAI.FKCRT.Inventory.CoreTree.labels_length line 49
5. def OAI.FKCRT.Inventory.CoreTree.toCode line 54
6. abbrev OAI.FKCRT.Inventory.CoreTree.MarkedCode line 67
7. abbrev OAI.FKCRT.Inventory.CoreTree.Sized line 69
8. def OAI.FKCRT.Inventory.CoreTree.ofMarkedCode line 71
9. lemma OAI.FKCRT.Inventory.CoreTree.ofMarkedCode_labels line 79
10. lemma OAI.FKCRT.Inventory.CoreTree.ofMarkedCode_size line 83
11. lemma OAI.FKCRT.Inventory.CoreTree.ofMarkedCode_injective line 86
12. def OAI.FKCRT.Inventory.CoreTree.sizedEquiv line 98
13. theorem OAI.FKCRT.Inventory.actual_marked_singleton line 116

    Source documentation

    The actual conditioned independent marking density, with no change of root distribution and no appeal to a conditional GW law as a hypothesis.

    theorem actual_marked_singleton (P : Parameters) (n : ℕ)
        (d : Code (2*n+1)) (a : Fin (2*n+1) → CoreLabel) :
        (actualOffspring P).markedCodeLaw (fun k => (CoreLabel.markLaw P k).toMeasure) n {(d,a)}=
          (if ∀ i,(a i).arity=(d.val i).val then ∏ i,CoreLabel.rootLaw P (a i) else 0)/
            ENNReal.ofReal (codePartition (actualOffspring P) (2*n+1)) := by
    …

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.CoreLabel, OAI.FKCRT.Inventory.actualOffspring, OAI.FKCRT.Inventory.CoreLabel.markLaw, OAI.FKCRT.Inventory.CoreLabel.rootLaw

14. def OAI.FKCRT.Inventory.CoreTree.sizedWordEquiv line 150

    Source documentation

    The actual successful words and compatible independently marked tree codes are equivalent at each fixed total edge size.

    def sizedWordEquiv (N : ℕ) : Sized (N+1) ≃ {w : EmptyTypedWord // w.val.length=N} :=
    …

    Mentions: OAI.FKCRT.Inventory.CoreTree.Sized, OAI.FKCRT.Inventory.EmptyTypedWord

15. abbrev OAI.FKCRT.Inventory.CoreTree.SizedWord line 164
16. def OAI.FKCRT.Inventory.CoreTree.markedWordEquiv line 166
17. lemma OAI.FKCRT.Inventory.CoreTree.markedWordEquiv_word line 169
18. lemma OAI.FKCRT.Inventory.CoreTree.rootMass_product line 172
19. lemma OAI.FKCRT.Inventory.CoreTree.rootLaw_product line 180
20. theorem OAI.FKCRT.Inventory.actual_marked_word_density line 192

    Source documentation

    Complete pointwise finite-law density, now expressed in the word of the original map bijection. Every leaf, every admissible arity and the common normalizing factor are retained.

    theorem actual_marked_word_density (P : Parameters) (n : ℕ)
        (x : CoreTree.MarkedCode (2*n+1)) :
        (actualOffspring P).markedCodeLaw (fun k => (CoreLabel.markLaw P k).toMeasure) n {x.val}=
          ENNReal.ofReal (wordMonomial (flexParameter P) (Real.sqrt (radiusParameter P))
            ((CoreTree.markedWordEquiv (2*n)) x).val.val/emptyTotal P)/
              ENNReal.ofReal (codePartition (actualOffspring P) (2*n+1)) := by
    …

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.CoreTree.MarkedCode, OAI.FKCRT.Inventory.actualOffspring, OAI.FKCRT.Inventory.CoreLabel.markLaw, OAI.FKCRT.Inventory.wordMonomial, OAI.FKCRT.Inventory.flexParameter, OAI.FKCRT.Inventory.radiusParameter, OAI.FKCRT.Inventory.CoreTree.markedWordEquiv, OAI.FKCRT.Inventory.emptyTotal

21. theorem OAI.FKCRT.Inventory.actual_marked_compatible line 204

    Source documentation

    There is no positive mass on inconsistent marks. In particular the arbitrary mark at an impossible offspring value is irrelevant.

    theorem actual_marked_compatible (P : Parameters) (n : ℕ) :
        ∀ᵐ x ∂(actualOffspring P).markedCodeLaw (fun k => (CoreLabel.markLaw P k).toMeasure) n,
          ∀ i,(x.2 i).arity=(x.1.val i).val := by
    …

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.actualOffspring, OAI.FKCRT.Inventory.CoreLabel.markLaw