OAI/Combinatorics/CliqueFree/LocalWalk.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.transition line 26

    Source documentation

    The disjoint union of the neighborhood transition kernels.

    noncomputable def transition : Kernel (EdgeState G) := fun e f ↦
…

    Mentions: OAI.CliqueFreeIndependence.WeightedGraph.EdgeState

  2. def OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.normalizer line 31
  3. def OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.law line 34
  4. def OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.vertexWeight line 37
  5. def OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.fiber line 39
  6. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.mem_fiber line 43
  7. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.fiber_mass line 47
  8. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.normalizer_eq line 51
  9. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.transition_stochastic line 57
  10. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.normalizer_pos line 77
  11. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.law_isProb line 81
  12. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.transition_reversible line 91
  13. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.transition_fixed_src line 106
  14. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.transition_density line 109
  15. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.smoothed_fixed_src line 122
  16. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.smoothed_supported line 126
  17. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.smoothed_density line 133
  18. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.entropy_bounds line 140