OAI/Combinatorics/GraphThreshold/ProbabilityTreeTrim.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Deterministic removal of initial zero-capacity levels.

  1. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstChild line 14

    Source documentation

    Choose one child deterministically from the actual nonempty child law.

    def firstChild : {d : ℕ} → ProbabilityTree X (d + 1) → ProbabilityTree X d
  | _, @node _ _ _ _ law _ _ child => child (Classical.choice (branch_nonempty law))

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

  2. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstLabel line 17
  3. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.prependChosen line 21

    Source documentation

    Prepend the chosen incoming arc to a path of the chosen child.

    def prependChosen : {d : ℕ} → (T : ProbabilityTree X (d + 1)) →
    (firstChild T).Path → T.Path
  | _, @node _ _ _ _ law _ _ _, p => ⟨Classical.choice (branch_nonempty law), p⟩

/-- Remove `k` initial levels. The additive depth form avoids subtraction casts. -/

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstChild, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Path, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.branch_nonempty

  4. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.drop line 26

    Source documentation

    Remove k initial levels. The additive depth form avoids subtraction casts.

    def drop : (k : ℕ) → {d : ℕ} → ProbabilityTree X (d + k) → ProbabilityTree X d
  | 0, _, T => T
  | k + 1, _, T => drop k (firstChild T)

/-- Lift a retained path through the fixed choices on the removed prefix. -/

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

  5. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.liftDropPath line 31

    Source documentation

    Lift a retained path through the fixed choices on the removed prefix.

    def liftDropPath : (k : ℕ) → {d : ℕ} → (T : ProbabilityTree X (d + k)) →
    (drop k T).Path → T.Path
  | 0, _, _, p => p
  | k + 1, _, T, p => prependChosen T (liftDropPath k (firstChild T) p)

/-- Reindex a tree along equality of depths, without changing its data. -/

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.drop, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Path, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.prependChosen, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstChild

  6. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.castDepth line 37

    Source documentation

    Reindex a tree along equality of depths, without changing its data.

    def castDepth {d e : ℕ} (h : d = e) (T : ProbabilityTree X d) : ProbabilityTree X e := h ▸ T

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree

  7. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.castPath line 39
  8. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.dropPrefix line 45

    Source documentation

    Subtraction-indexed convenience wrapper for removing an initial prefix.

    def dropPrefix {d : ℕ} (T : ProbabilityTree X d) (k : ℕ) (hk : k ≤ d) :
    ProbabilityTree X (d - k) :=
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree

  9. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.liftDropPrefixPath line 49
  10. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathUnion_prependChosen line 58
  11. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstChild_support_subset line 64
  12. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstChild_isDisjoint line 70
  13. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstChild_hasCapacities line 76
  14. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstChild_hasSpread line 81
  15. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstLabel_card_le line 87
  16. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstLabel_eq_empty line 93
  17. def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.prefixUnion line 100

    Source documentation

    Labels committed by the deterministic choices on the removed prefix.

    def prefixUnion : (k : ℕ) → {d : ℕ} → ProbabilityTree X (d + k) → Finset X
  | 0, _, _ => ∅
  | k + 1, _, T => firstLabel T ∪ prefixUnion k (firstChild T)

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstLabel, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.firstChild

  18. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathUnion_liftDropPath line 104
  19. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.drop_support_subset line 114
  20. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.drop_isDisjoint line 120
  21. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.drop_hasCapacities line 127
  22. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.drop_hasSpread line 135
  23. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.prefixUnion_eq_empty_of_capacities line 143
  24. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathUnion_liftDropPath_eq line 153

    Source documentation

    Removing zero-capacity levels preserves every retained full path union exactly.

    theorem pathUnion_liftDropPath_eq (k : ℕ) {d : ℕ} {T : ProbabilityTree X (d + k)}
    {m : ℕ → ℕ} (hT : T.HasCapacities m) (hm : ∀ i, i < k → m i = 0)
    (p : (drop k T).Path) : T.pathUnion (liftDropPath k T p) = (drop k T).pathUnion p := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.drop, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Path, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.liftDropPath, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathUnion

  25. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.support_castDepth line 158
  26. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.isDisjoint_castDepth line 161
  27. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.hasCapacities_castDepth line 165
  28. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.hasSpread_castDepth line 168
  29. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathUnion_castPath_symm line 171
  30. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.dropPrefix_support_subset line 175
  31. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.dropPrefix_isDisjoint line 180
  32. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.dropPrefix_hasCapacities line 186
  33. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.dropPrefix_hasSpread line 192
  34. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathUnion_liftDropPrefixPath_eq line 199

    Source documentation

    Every path after zero-prefix trimming is an original full path with exactly the same union.

    theorem pathUnion_liftDropPrefixPath_eq {d : ℕ} {T : ProbabilityTree X d} {m : ℕ → ℕ}
    (hT : T.HasCapacities m) (k : ℕ) (hk : k ≤ d)
    (hm : ∀ i, i < k → m i = 0) (p : (dropPrefix T k hk).Path) :
    T.pathUnion (liftDropPrefixPath T k hk p) = (dropPrefix T k hk).pathUnion p := by
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.dropPrefix, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Path, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.liftDropPrefixPath, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.pathUnion

  35. theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.coveredBy_of_dropPrefix line 208