OAI/Combinatorics/GraphThreshold/TreeReduction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LeanBlast.SecondKahnKalai.retainedMass line 18
2. abbrev OAI.LeanBlast.SecondKahnKalai.RetainedIndex line 21
3. theorem OAI.LeanBlast.SecondKahnKalai.sum_retained line 23
4. theorem OAI.LeanBlast.SecondKahnKalai.sum_retained_weights line 37
5. theorem OAI.LeanBlast.SecondKahnKalai.sum_retained_indicator line 41
6. def OAI.LeanBlast.SecondKahnKalai.retainedLaw line 48

   Source documentation

   The actual normalized child law, after removing all zero-mass targets.

   def retainedLaw (w : B → ℝ) (G : B → Prop) (hw : ∀ b, 0 ≤ w b)
       (hpos : 0 < retainedMass w G) : FiniteLaw (RetainedIndex w G) where
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.retainedMass, OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.RetainedIndex

7. theorem OAI.LeanBlast.SecondKahnKalai.retainedLaw_positive line 56
8. theorem OAI.LeanBlast.SecondKahnKalai.retainedLaw_prob line 61
9. theorem OAI.LeanBlast.SecondKahnKalai.retainedLaw_isSpread line 71
10. theorem OAI.LeanBlast.SecondKahnKalai.target_fragment_mass_le_source line 95
11. theorem OAI.LeanBlast.SecondKahnKalai.one_sub_exp_neg_nat_pos line 141
12. theorem OAI.LeanBlast.SecondKahnKalai.good_retainedMass_pos line 146
13. def OAI.LeanBlast.SecondKahnKalai.reduceTree line 157

    Source documentation

    Explicit good-node pruning and normalization. The depth is preserved in the result type. Every retained label is the actual fragment of its original label.

    def reduceTree (ρ : ℝ) (m : ℕ → ℕ) (W : Finset X) {d : ℕ}
        (T : ProbabilityTree X d) (hρ : 0 < ρ) (hm : ∀ j < d, 0 < m j)
        (hg : Good ρ m W T) : ProbabilityTree X d :=
    …

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

14. theorem OAI.LeanBlast.SecondKahnKalai.reduceTree_support_subset line 174
15. theorem OAI.LeanBlast.SecondKahnKalai.reduceTree_hasCapacities line 190
16. theorem OAI.LeanBlast.SecondKahnKalai.reduceTree_isDisjoint line 205
17. theorem OAI.LeanBlast.SecondKahnKalai.reduceTree_path_recovery line 222
18. theorem OAI.LeanBlast.SecondKahnKalai.reduceTree_hasSpread line 249