OAI/Combinatorics/CliqueFree/Reach.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CliqueFreeIndependence.WeightedGraph.enlarge line 21

   Source documentation

   Whole-graph sets that contain most of the walk.

   noncomputable def enlarge (G : SimpleGraph V) (w : V → ℝ) (t : ℝ) (A : Finset V) : Finset V :=
   …

2. def OAI.CliqueFreeIndependence.WeightedGraph.reach line 24
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.subset_enlarge line 28
4. lemma OAI.CliqueFreeIndependence.WeightedGraph.not_mem_enlarge line 31
5. lemma OAI.CliqueFreeIndependence.WeightedGraph.enlarge_mass line 36
6. lemma OAI.CliqueFreeIndependence.WeightedGraph.reach_mass line 59
7. lemma OAI.CliqueFreeIndependence.WeightedGraph.reach_mass_exp line 70
8. lemma OAI.CliqueFreeIndependence.WeightedGraph.growth_le_of_lower line 86
9. def OAI.CliqueFreeIndependence.WeightedGraph.badSet line 98
10. lemma OAI.CliqueFreeIndependence.WeightedGraph.badSet_subset line 102
11. lemma OAI.CliqueFreeIndependence.WeightedGraph.badSet_mass_bound line 105
12. lemma OAI.CliqueFreeIndependence.WeightedGraph.conditional_bad_bound line 120
13. lemma OAI.CliqueFreeIndependence.WeightedGraph.reach_bad_mass line 152
14. def OAI.CliqueFreeIndependence.WeightedGraph.exceptionalConstant line 184
15. def OAI.CliqueFreeIndependence.WeightedGraph.entropyConstant line 185
16. def OAI.CliqueFreeIndependence.WeightedGraph.smoothingConstant line 186
17. lemma OAI.CliqueFreeIndependence.WeightedGraph.exceptionalConstant_nonneg line 188
18. lemma OAI.CliqueFreeIndependence.WeightedGraph.reach_bad_cross line 192