OAI/Combinatorics/GraphThreshold/ProbabilityTreePaths.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Full-path interpretation of supports and structural disjointness.

  1. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathUnion_subset_support line 13
  2. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.mem_pathUnion_iff line 22
  3. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathLabel_subset_pathUnion line 30
  4. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathLabel_subset_support line 35
  5. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.mem_support_iff_exists_path line 40

    Source documentation

    Every arc coordinate occurs on an actual full path, since all branches continue.

    theorem mem_support_iff_exists_path {d : ℕ} (T : ProbabilityTree X d) (x : X) :
    x ∈ T.support ↔ ∃ p : T.Path, x ∈ T.pathUnion p := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree

  6. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.support_eq_pathUnion_biUnion line 59
  7. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.isDisjoint_iff_pathDisjoint line 65
  8. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.incoming_disjoint_subtree_of_pathDisjoint line 93
  9. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.child_dependsOutside_of_pathDisjoint line 101

    Source documentation

    The locality assertion applies even when disjointness is given in the literal path form.

    theorem child_dependsOutside_of_pathDisjoint {d : ℕ} {B : Type} [Fintype B]
    {law : FiniteLaw B} {positive : law.IsPositive} {label : B → Finset X}
    {child : B → ProbabilityTree X d}
    (hT : (node B law positive label child).PathDisjoint) (b : B)
    {β : Type*} {f : Finset X → β} (hf : DependsOnlyOn (child b).support f) :
    DependsOutside (label b) f :=
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.PathDisjoint, OAI.LeanBlast.SecondKahnKalai.DependsOnlyOn, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.support, OAI.LeanBlast.SecondKahnKalai.DependsOutside

  10. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.coveredBy_mono line 109
  11. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.coveredBy_univ line 114