OAI/Combinatorics/GraphThreshold/TreeReductionData.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Fixed-input local masses and the deterministic good-node predicate.

  1. def OAI.LeanBlast.SecondKahnKalai.successfulTargetMass line 18
  2. def OAI.LeanBlast.SecondKahnKalai.localFailureMass line 22
  3. theorem OAI.LeanBlast.SecondKahnKalai.successfulTargetMass_nonneg line 26
  4. theorem OAI.LeanBlast.SecondKahnKalai.localFailureMass_nonneg line 35
  5. theorem OAI.LeanBlast.SecondKahnKalai.localFailureMass_add_successfulTargetMass line 46
  6. theorem OAI.LeanBlast.SecondKahnKalai.localFailureMass_eq_prob line 66
  7. theorem OAI.LeanBlast.SecondKahnKalai.successfulTargetMass_pos_capacity line 76
  8. theorem OAI.LeanBlast.SecondKahnKalai.resamplingZ_congr_fragments line 83
  9. theorem OAI.LeanBlast.SecondKahnKalai.localSuccess_congr_fragments line 95
  10. theorem OAI.LeanBlast.SecondKahnKalai.successfulTargetMass_congr_fragments line 105
  11. theorem OAI.LeanBlast.SecondKahnKalai.localFailureMass_congr_fragments line 119
  12. theorem OAI.LeanBlast.SecondKahnKalai.fragments_eq_of_inter_label_union_eq line 135
  13. theorem OAI.LeanBlast.SecondKahnKalai.successfulTargetMass_dependsOnlyOn line 148
  14. theorem OAI.LeanBlast.SecondKahnKalai.localFailureMass_dependsOnlyOn line 155
  15. def OAI.LeanBlast.SecondKahnKalai.Good line 168

    Source documentation

    Goodness is evaluated on the fixed input tree, using local nonfailure target masses before any pruning or reweighting.

    def Good (ρ : ℝ) (m : ℕ → ℕ) (W : Finset X) {d : ℕ} (T : ProbabilityTree X d) : Prop :=
…

    Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree