OAI/Combinatorics/GraphThreshold/ProbabilityTreeFacts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Path and locality facts for the stable finite probability-tree representation.

  1. theorem OAI.LeanBlast.SecondKahnKalai.DependsOnlyOn.mono line 16
  2. theorem OAI.LeanBlast.SecondKahnKalai.DependsOnlyOn.dependsOutside line 28
  3. theorem OAI.LeanBlast.SecondKahnKalai.DependsOutside.sdiff_eq line 40
  4. theorem OAI.LeanBlast.SecondKahnKalai.dependsOutside_iff_sdiff line 46
  5. theorem OAI.LeanBlast.SecondKahnKalai.DependsOutside.union_eq line 53
  6. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.branch_nonempty line 69

    Source documentation

    A finite law of total mass one has a nonempty underlying type.

    theorem branch_nonempty {B : Type} [Fintype B] (law : FiniteLaw B) : Nonempty B := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw

  7. instance OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathNonempty line 77

    Source documentation

    Every equal-depth probability tree has at least one full path.

    instance pathNonempty {d : ℕ} (T : ProbabilityTree X d) : Nonempty T.Path := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree

  8. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.choosePath line 85

    Source documentation

    A fixed deterministic full path, used only to resolve finite choices.

    def choosePath {d : ℕ} (T : ProbabilityTree X d) : T.Path := Classical.choice (pathNonempty T)

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathNonempty

  9. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathLabels_length line 87
  10. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.label_subset_support line 99
  11. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.child_support_subset line 106
  12. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.labels_support_subset line 113
  13. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.child_dependsOutside line 121