OAI/Combinatorics/CliqueFree/WalkEntropy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.liftSet line 24
  2. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.mem_liftSet line 27
  3. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.liftSet_subset_fiber line 30
  4. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.sum_liftSet line 34
  5. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.lazy_neighbor_density line 47
  6. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.liftSet_adj_mass_le line 63
  7. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.incoming_good_le line 74
  8. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.reach_leakage line 141
  9. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.law_rev line 180
  10. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.law_bad_sum line 184
  11. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.law_bad_le line 207
  12. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.entropy_good_row line 222
  13. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.averaged_entropy_bound line 247
  14. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.avg_entropy_lower line 282
  15. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.avg_entropy_upper line 296
  16. def OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.rowDistance line 333
  17. lemma OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.exists_smooth_index line 338

    Source documentation

    The C-dependent entropy smoothing bound.

    lemma exists_smooth_index [Nonempty (EdgeState G)] (hw : ∀ u, 0 < w u)
    {C x : ℝ} (hC : 1 ≤ C) (hCross : CrossBound G w C) (hx : 32 ≤ x)
    (hc : ∀ u v, G.Adj u v → 1 / x ≤ commonMass G w u v)
    (hL : ∀ u, neighborMass G w u ≤ Real.exp x) :
    ∃ j < ⌈x⌉₊,
      avgEntropy (law G w) (vertexWeight G w) (smoothed (transition G w) j) ≤
        entropyConstant C * Real.log x ∧
      rowDistance (G := G) (w := w) j ≤ smoothingConstant C * Real.sqrt (Real.log x / x) := by
…

    Mentions: OAI.CliqueFreeIndependence.WeightedGraph.EdgeState, OAI.CliqueFreeIndependence.WeightedGraph.CrossBound, OAI.CliqueFreeIndependence.WeightedGraph.commonMass, OAI.CliqueFreeIndependence.WeightedGraph.neighborMass, OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.law, OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.vertexWeight, OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.transition, OAI.CliqueFreeIndependence.WeightedGraph.entropyConstant, OAI.CliqueFreeIndependence.WeightedGraph.LocalWalk.rowDistance, OAI.CliqueFreeIndependence.WeightedGraph.smoothingConstant