OAI/Combinatorics/CliqueFree/FiniteKernel.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CliqueFreeIndependence.FiniteKernel.Kernel line 21
  2. def OAI.CliqueFreeIndependence.FiniteKernel.Stochastic line 25
  3. def OAI.CliqueFreeIndependence.FiniteKernel.Stationary line 26
  4. def OAI.CliqueFreeIndependence.FiniteKernel.Reversible line 27
  5. def OAI.CliqueFreeIndependence.FiniteKernel.lazy line 29
  6. def OAI.CliqueFreeIndependence.FiniteKernel.smoothed line 32
  7. def OAI.CliqueFreeIndependence.FiniteKernel.avgEntropy line 36
  8. lemma OAI.CliqueFreeIndependence.FiniteKernel.stochastic_one line 38
  9. lemma OAI.CliqueFreeIndependence.FiniteKernel.stochastic_mul line 47
  10. lemma OAI.CliqueFreeIndependence.FiniteKernel.stochastic_pow line 52
  11. lemma OAI.CliqueFreeIndependence.FiniteKernel.stochastic_lazy line 58
  12. lemma OAI.CliqueFreeIndependence.FiniteKernel.stochastic_smoothed line 70
  13. lemma OAI.CliqueFreeIndependence.FiniteKernel.stationary_of_reversible line 73
  14. lemma OAI.CliqueFreeIndependence.FiniteKernel.stationary_lazy line 80
  15. lemma OAI.CliqueFreeIndependence.FiniteKernel.reversible_one line 92
  16. lemma OAI.CliqueFreeIndependence.FiniteKernel.reversible_mul line 99
  17. lemma OAI.CliqueFreeIndependence.FiniteKernel.reversible_pow line 117
  18. lemma OAI.CliqueFreeIndependence.FiniteKernel.reversible_lazy line 127
  19. lemma OAI.CliqueFreeIndependence.FiniteKernel.lazy_eq line 137
  20. lemma OAI.CliqueFreeIndependence.FiniteKernel.commute_lazy line 142
  21. lemma OAI.CliqueFreeIndependence.FiniteKernel.reversible_smoothed line 148
  22. lemma OAI.CliqueFreeIndependence.FiniteKernel.smoothed_zero line 154
  23. lemma OAI.CliqueFreeIndependence.FiniteKernel.smoothed_succ line 158
  24. lemma OAI.CliqueFreeIndependence.FiniteKernel.smoothed_succ_right line 164
  25. lemma OAI.CliqueFreeIndependence.FiniteKernel.smoothed_density line 169
  26. lemma OAI.CliqueFreeIndependence.FiniteKernel.pair_isProb line 181
  27. lemma OAI.CliqueFreeIndependence.FiniteKernel.stationary_average line 190
  28. lemma OAI.CliqueFreeIndependence.FiniteKernel.entropy_increment line 197
  29. lemma OAI.CliqueFreeIndependence.FiniteKernel.entropy_increment_nonneg line 208
  30. lemma OAI.CliqueFreeIndependence.FiniteKernel.entropy_increment_tv line 222
  31. lemma OAI.CliqueFreeIndependence.FiniteKernel.lazy_triangle_tv line 233
  32. lemma OAI.CliqueFreeIndependence.FiniteKernel.smoothed_entropy_mono line 261
  33. lemma OAI.CliqueFreeIndependence.FiniteKernel.smoothed_row_distance_sq line 270
  34. lemma OAI.CliqueFreeIndependence.FiniteKernel.exists_smoothed_row_distance line 289

    Source documentation

    Entropy telescoping gives the averaged triangle-row estimate.

    lemma exists_smoothed_row_distance {π w : I → ℝ} (hπ : IsProb π) (hw : ∀ i, 0 < w i)
    {P : Kernel I} (hP : Stochastic P) (hs : Stationary π P)
    {R : ℕ} (hR : 0 < R) {D : ℝ}
    (hD : avgEntropy π w (smoothed P R) - avgEntropy π w (smoothed P 0) ≤ D) :
    ∃ j < R, (∑ i, π i * ∑ z, P i z * tv (smoothed P j i) (smoothed P j z)) ^ 2 ≤
      4 * D / R := by
…

    Mentions: OAI.CliqueFreeIndependence.FiniteKernel.Kernel, OAI.CliqueFreeIndependence.FiniteKernel.Stochastic, OAI.CliqueFreeIndependence.FiniteKernel.Stationary, OAI.CliqueFreeIndependence.FiniteKernel.avgEntropy, OAI.CliqueFreeIndependence.FiniteKernel.smoothed

  35. def OAI.CliqueFreeIndependence.FiniteKernel.Preserves line 314
  36. lemma OAI.CliqueFreeIndependence.FiniteKernel.preserves_one line 318
  37. lemma OAI.CliqueFreeIndependence.FiniteKernel.preserves_mul line 323
  38. lemma OAI.CliqueFreeIndependence.FiniteKernel.preserves_pow line 334
  39. lemma OAI.CliqueFreeIndependence.FiniteKernel.preserves_lazy line 341
  40. lemma OAI.CliqueFreeIndependence.FiniteKernel.preserves_smoothed line 347
  41. def OAI.CliqueFreeIndependence.FiniteKernel.rowMass line 351
  42. lemma OAI.CliqueFreeIndependence.FiniteKernel.rowMass_le_one line 353
  43. lemma OAI.CliqueFreeIndependence.FiniteKernel.rowMass_mul line 358
  44. lemma OAI.CliqueFreeIndependence.FiniteKernel.rowMass_compl line 364
  45. lemma OAI.CliqueFreeIndependence.FiniteKernel.leakage_mul_le line 370
  46. lemma OAI.CliqueFreeIndependence.FiniteKernel.reversed_entropy_tail line 388