OAI/Combinatorics/GraphThreshold/Resampling.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LeanBlast.SecondKahnKalai.resamplingY line 15
2. def OAI.LeanBlast.SecondKahnKalai.resamplingNumerator line 17
3. def OAI.LeanBlast.SecondKahnKalai.resamplingZ line 22

   Source documentation

   The actual normalizing density Z(Y).

   def resamplingZ (ν : FiniteLaw B) (A : B → Finset X) (ρ : ℝ)
       (Y : Finset X) : ℝ :=
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw

4. def OAI.LeanBlast.SecondKahnKalai.resamplingTargetWeight line 26
5. def OAI.LeanBlast.SecondKahnKalai.resamplingWeight line 31
6. def OAI.LeanBlast.SecondKahnKalai.resamplingFragment line 36

   Source documentation

   The retained target fragment; no quotienting of the label indices occurs.

   def resamplingFragment (A : B → Finset X) (W : Finset X) (b : B) : Finset X :=
   …

7. theorem OAI.LeanBlast.SecondKahnKalai.resamplingNumerator_nonneg line 39
8. theorem OAI.LeanBlast.SecondKahnKalai.resamplingZ_nonneg line 47
9. theorem OAI.LeanBlast.SecondKahnKalai.resamplingZ_pos line 51
10. theorem OAI.LeanBlast.SecondKahnKalai.resamplingTargetWeight_nonneg line 62
11. theorem OAI.LeanBlast.SecondKahnKalai.resamplingWeight_nonneg line 68
12. theorem OAI.LeanBlast.SecondKahnKalai.resamplingTargetWeight_total line 73
13. theorem OAI.LeanBlast.SecondKahnKalai.resampling_source_marginal line 79
14. theorem OAI.LeanBlast.SecondKahnKalai.resamplingWeight_total line 85
15. def OAI.LeanBlast.SecondKahnKalai.resamplingTargetLaw line 92
16. def OAI.LeanBlast.SecondKahnKalai.resamplingLaw line 98
17. theorem OAI.LeanBlast.SecondKahnKalai.resamplingLaw_weight line 104
18. theorem OAI.LeanBlast.SecondKahnKalai.resampling_expectation_source line 108
19. theorem OAI.LeanBlast.SecondKahnKalai.resampling_prob_source line 116
20. theorem OAI.LeanBlast.SecondKahnKalai.resamplingWeight_eq_zero_of_not_subset line 127
21. theorem OAI.LeanBlast.SecondKahnKalai.resampling_target_subset_of_pos line 132
22. theorem OAI.LeanBlast.SecondKahnKalai.resamplingFragment_subset_target line 140
23. theorem OAI.LeanBlast.SecondKahnKalai.resamplingFragment_subset_source line 143
24. theorem OAI.LeanBlast.SecondKahnKalai.resamplingFragment_subset_inter line 153
25. theorem OAI.LeanBlast.SecondKahnKalai.resamplingFragment_recovery line 162

    Source documentation

    Every target label is recovered by adjoining its retained fragment to W.

    theorem resamplingFragment_recovery (A : B → Finset X) (W : Finset X) (b : B) :
        A b ⊆ W ∪ resamplingFragment A W b := by
    …

    Mentions: OAI.LeanBlast.SecondKahnKalai.resamplingFragment

26. theorem OAI.LeanBlast.SecondKahnKalai.resampling_target_subset_iff_fragment line 170
27. theorem OAI.LeanBlast.SecondKahnKalai.resamplingWeight_congr_fragments line 186

    Source documentation

    The transition depends on W only through its intersections with the labels, expressed equivalently by their retained fragments.

    theorem resamplingWeight_congr_fragments (ν : FiniteLaw B) (A : B → Finset X)
        (ρ : ℝ) {W W' : Finset X}
        (hW : ∀ b, resamplingFragment A W b = resamplingFragment A W' b) (cb : B × B) :
        resamplingWeight ν A ρ W cb = resamplingWeight ν A ρ W' cb := by
    …

    Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.resamplingFragment, OAI.LeanBlast.SecondKahnKalai.resamplingWeight