OAI/Computability/MaxCut/Games/Pinsker.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

A finite Pinsker inequality with a nonoptimal constant, sufficient for the information bound used by Holenstein: TV(p,q)^2 ≤ D_nat(p || q). The proof factors the L1 distance through square roots and uses log t ≤ t-1.

  1. def OAI.MaxCutGames.Foundations.Information.hellingerSquared line 20
  2. theorem OAI.MaxCutGames.Foundations.Information.sqrt_distance_le_relativeEntropy_term line 23
  3. theorem OAI.MaxCutGames.Foundations.Information.hellingerSquared_le_relativeEntropy line 48
  4. theorem OAI.MaxCutGames.Foundations.Information.totalVariation_sq_le_hellingerSquared line 56
  5. theorem OAI.MaxCutGames.Foundations.Information.totalVariation_sq_le_relativeEntropy line 81
  6. theorem OAI.MaxCutGames.Foundations.Information.posterior_totalVariation_sq_le_log line 87
  7. def OAI.MaxCutGames.Foundations.Information.coordinateMarginal line 105
  8. def OAI.MaxCutGames.Foundations.Information.independentProduct line 109
  9. theorem OAI.MaxCutGames.Foundations.Information.coordinateMarginal_isProbability line 111
  10. theorem OAI.MaxCutGames.Foundations.Information.point_le_coordinateMarginal line 125
  11. theorem OAI.MaxCutGames.Foundations.Information.marginal_expectation line 133
  12. theorem OAI.MaxCutGames.Foundations.Information.independentProduct_isProbability line 142
  13. theorem OAI.MaxCutGames.Foundations.Information.joint_supportedBy_product_coordinateMarginals line 150
  14. theorem OAI.MaxCutGames.Foundations.Information.relativeEntropy_independent_reference line 158
  15. theorem OAI.MaxCutGames.Foundations.Information.coordinate_relativeEntropy_sum_le line 201
  16. theorem OAI.MaxCutGames.Foundations.Information.coordinate_totalVariation_sq_sum_le line 211
  17. theorem OAI.MaxCutGames.Foundations.Information.posterior_coordinate_supportedBy line 220
  18. theorem OAI.MaxCutGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_log line 238

    Source documentation

    The finite independent-coordinate conditioning inequality underlying Holenstein Lemma 4.1, with natural logarithms. w x is the conditional probability of the event given the coordinate tuple x.

    theorem posterior_coordinate_totalVariation_sq_sum_le_log
    (q : ι → α → ℝ) (hq : ∀ i, IsProbability (q i)) (w : (ι → α) → ℝ)
    (hw : ∀ x, 0 ≤ w x) (hw_one : ∀ x, w x ≤ 1) {z : ℝ} (hz : 0 < z)
    (hmass : ∑ x, independentProduct q x * w x = z) :
    (∑ i, totalVariation
      (coordinateMarginal (posterior (independentProduct q) w z) i) (q i) ^ 2) ≤
        Real.log (1 / z) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Information.IsProbability, OAI.MaxCutGames.Foundations.Information.independentProduct, OAI.MaxCutGames.Foundations.Information.totalVariation, OAI.MaxCutGames.Foundations.Information.coordinateMarginal, OAI.MaxCutGames.Foundations.Information.posterior

  19. theorem OAI.MaxCutGames.Foundations.Information.posterior_coordinate_totalVariation_sum_le_sqrt line 252

    Source documentation

    The summed-distance form (4.2), with natural logarithms.

    theorem posterior_coordinate_totalVariation_sum_le_sqrt
    (q : ι → α → ℝ) (hq : ∀ i, IsProbability (q i)) (w : (ι → α) → ℝ)
    (hw : ∀ x, 0 ≤ w x) (hw_one : ∀ x, w x ≤ 1) {z : ℝ} (hz : 0 < z)
    (hmass : ∑ x, independentProduct q x * w x = z) :
    (∑ i, totalVariation
      (coordinateMarginal (posterior (independentProduct q) w z) i) (q i)) ≤
        Real.sqrt ((Fintype.card ι : ℝ) * Real.log (1 / z)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Information.IsProbability, OAI.MaxCutGames.Foundations.Information.independentProduct, OAI.MaxCutGames.Foundations.Information.totalVariation, OAI.MaxCutGames.Foundations.Information.coordinateMarginal, OAI.MaxCutGames.Foundations.Information.posterior

  20. theorem OAI.MaxCutGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_binaryLog line 279

    Source documentation

    The base-two-logarithm normalization of the squared-distance bound.

    theorem posterior_coordinate_totalVariation_sq_sum_le_binaryLog
    (q : ι → α → ℝ) (hq : ∀ i, IsProbability (q i)) (w : (ι → α) → ℝ)
    (hw : ∀ x, 0 ≤ w x) (hw_one : ∀ x, w x ≤ 1) {z : ℝ} (hz : 0 < z)
    (hmass : ∑ x, independentProduct q x * w x = z) :
    (∑ i, totalVariation
      (coordinateMarginal (posterior (independentProduct q) w z) i) (q i) ^ 2) ≤
        Real.log (1 / z) / Real.log 2 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Information.IsProbability, OAI.MaxCutGames.Foundations.Information.independentProduct, OAI.MaxCutGames.Foundations.Information.totalVariation, OAI.MaxCutGames.Foundations.Information.coordinateMarginal, OAI.MaxCutGames.Foundations.Information.posterior

  21. theorem OAI.MaxCutGames.Foundations.Information.normalize_isProbability line 299
  22. theorem OAI.MaxCutGames.Foundations.Information.relativeEntropy_normalize_right line 307
  23. theorem OAI.MaxCutGames.Foundations.Information.neg_relativeEntropy_le_log_mass line 321
  24. theorem OAI.MaxCutGames.Foundations.Information.posterior_weighted_log_inverse_le line 334

    Source documentation

    Entropy budget for a finite posterior indexed by side information. The baseline masses b may have total mass B, rather than one. In the application, b(t,v)=P_T(t) and B is the number of possible side labels.

    theorem posterior_weighted_log_inverse_le (p b c : α → ℝ) (hp : IsProbability p)
    (hb : ∀ a, 0 ≤ b a) {z B : ℝ} (hz : 0 < z) (hB : 0 < B)
    (hmass : ∑ a, b a = B) (hpost : ∀ a, p a = b a * c a / z) :
    (∑ a, p a * Real.log (1 / c a)) ≤ Real.log (B / z) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Information.IsProbability

  25. def OAI.MaxCutGames.Foundations.Information.posteriorOrOriginal line 372
  26. theorem OAI.MaxCutGames.Foundations.Information.posteriorOrOriginal_isProbability line 377
  27. theorem OAI.MaxCutGames.Foundations.Information.mass_mul_posteriorOrOriginal line 388
  28. theorem OAI.MaxCutGames.Foundations.Information.weighted_coordinate_posterior_recombine line 408
  29. theorem OAI.MaxCutGames.Foundations.Information.side_information_bound line 430
  30. theorem OAI.MaxCutGames.Foundations.Information.finite_side_information_bound line 500

    Source documentation

    Finite Corollary 4.3 in natural-log normalization, for actual likelihood profiles of the event jointly with the finite side label.

    theorem finite_side_information_bound
    (pT : T → ℝ) (q : T → I → A → ℝ)
    (e : T × V → (I → A) → ℝ) (c w : T × V → ℝ)
    (hpT : IsProbability pT)
    (hq : ∀ t i, IsProbability (q t i))
    (he : ∀ tv x, 0 ≤ e tv x)
    (he_sum : ∀ t x, (∑ v, e (t, v) x) ≤ 1)
    (hc : ∀ tv, ∑ x, independentProduct (q tv.1) x * e tv x = c tv)
    {z : ℝ} (hz : 0 < z)
    (hZ : ∑ tv, pT tv.1 * c tv = z)
    (hweight : ∀ tv, w tv = pT tv.1 * c tv / z) :
    (∑ i, totalVariation
…

    Mentions: OAI.MaxCutGames.Foundations.Information.IsProbability, OAI.MaxCutGames.Foundations.Information.independentProduct, OAI.MaxCutGames.Foundations.Information.totalVariation