OAI/Computability/UniqueGames/Foundations/PinskerLemmas.lean

GitHub source file

40 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.UniqueGamesTheorem.Foundations.Information.hellingerSquared line 23
  2. theorem OAI.UniqueGamesTheorem.Foundations.Information.sqrt_distance_le_relativeEntropy_term line 26
  3. theorem OAI.UniqueGamesTheorem.Foundations.Information.hellingerSquared_le_relativeEntropy line 51
  4. theorem OAI.UniqueGamesTheorem.Foundations.Information.totalVariation_sq_le_hellingerSquared line 59
  5. theorem OAI.UniqueGamesTheorem.Foundations.Information.totalVariation_sq_le_relativeEntropy line 84
  6. theorem OAI.UniqueGamesTheorem.Foundations.Information.posterior_totalVariation_sq_le_log line 90
  7. def OAI.UniqueGamesTheorem.Foundations.Information.coordinateMarginal line 112
  8. def OAI.UniqueGamesTheorem.Foundations.Information.independentProduct line 116
  9. theorem OAI.UniqueGamesTheorem.Foundations.Information.coordinateMarginal_isProbability line 118
  10. theorem OAI.UniqueGamesTheorem.Foundations.Information.point_le_coordinateMarginal line 132
  11. theorem OAI.UniqueGamesTheorem.Foundations.Information.marginal_expectation line 140
  12. theorem OAI.UniqueGamesTheorem.Foundations.Information.independentProduct_isProbability line 149
  13. theorem OAI.UniqueGamesTheorem.Foundations.Information.joint_supportedBy_product_coordinateMarginals line 157
  14. theorem OAI.UniqueGamesTheorem.Foundations.Information.relativeEntropy_independent_reference line 165
  15. theorem OAI.UniqueGamesTheorem.Foundations.Information.coordinate_relativeEntropy_sum_le line 208
  16. theorem OAI.UniqueGamesTheorem.Foundations.Information.coordinate_totalVariation_sq_sum_le line 218
  17. theorem OAI.UniqueGamesTheorem.Foundations.Information.posterior_coordinate_supportedBy line 227
  18. theorem OAI.UniqueGamesTheorem.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_log line 245

    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.UniqueGamesTheorem.Foundations.Information.IsProbability, OAI.UniqueGamesTheorem.Foundations.Information.independentProduct, OAI.UniqueGamesTheorem.Foundations.Information.totalVariation, OAI.UniqueGamesTheorem.Foundations.Information.coordinateMarginal, OAI.UniqueGamesTheorem.Foundations.Information.posterior

  19. theorem OAI.UniqueGamesTheorem.Foundations.Information.posterior_coordinate_totalVariation_sum_le_sqrt line 259

    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.UniqueGamesTheorem.Foundations.Information.IsProbability, OAI.UniqueGamesTheorem.Foundations.Information.independentProduct, OAI.UniqueGamesTheorem.Foundations.Information.totalVariation, OAI.UniqueGamesTheorem.Foundations.Information.coordinateMarginal, OAI.UniqueGamesTheorem.Foundations.Information.posterior

  20. theorem OAI.UniqueGamesTheorem.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_binaryLog line 286

    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.UniqueGamesTheorem.Foundations.Information.IsProbability, OAI.UniqueGamesTheorem.Foundations.Information.independentProduct, OAI.UniqueGamesTheorem.Foundations.Information.totalVariation, OAI.UniqueGamesTheorem.Foundations.Information.coordinateMarginal, OAI.UniqueGamesTheorem.Foundations.Information.posterior

  21. def OAI.UniqueGamesTheorem.Foundations.Information.posteriorOrOriginal line 307
  22. theorem OAI.UniqueGamesTheorem.Foundations.Information.posteriorOrOriginal_isProbability line 312
  23. theorem OAI.UniqueGamesTheorem.Foundations.Information.mass_mul_posteriorOrOriginal line 323
  24. theorem OAI.UniqueGamesTheorem.Foundations.Information.weighted_coordinate_posterior_recombine line 343
  25. theorem OAI.UniqueGamesTheorem.Foundations.Information.side_information_bound line 365
  26. theorem OAI.UniqueGamesTheorem.Foundations.Information.finite_side_information_bound line 435

    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.UniqueGamesTheorem.Foundations.Information.IsProbability, OAI.UniqueGamesTheorem.Foundations.Information.independentProduct, OAI.UniqueGamesTheorem.Foundations.Information.totalVariation

  27. structure OAI.UniqueGamesTheorem.Foundations.Target.Literal line 492
  28. def OAI.UniqueGamesTheorem.Foundations.Target.Literal.eval line 497
  29. abbrev OAI.UniqueGamesTheorem.Foundations.Target.Clause line 500
  30. def OAI.UniqueGamesTheorem.Foundations.Target.Clause.eval line 502
  31. structure OAI.UniqueGamesTheorem.Foundations.Target.Formula line 507

    Source documentation

    A finite conjunction of clauses with exactly three literal slots each. Repeated variables and repeated literals are allowed.

    structure Formula where
…
  32. def OAI.UniqueGamesTheorem.Foundations.Target.Formula.Satisfiable line 511
  33. theorem OAI.UniqueGamesTheorem.Foundations.Target.PermutationTable.images_injective line 518

    Source documentation

    Finite forward and inverse tables make totality and invertibility explicit. An eventual external encoding only needs to serialize the forward table.

    theorem PermutationTable.images_injective {q : Nat} (table : PermutationTable q)
    {x y : Fin q} (h : table.images[x] = table.images[y]) : x = y := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.PermutationTable

  34. theorem OAI.UniqueGamesTheorem.Foundations.Target.PermutationTable.images_surjective line 523
  35. theorem OAI.UniqueGamesTheorem.Foundations.Target.countSatisfied_le_length line 530

    Source documentation

    Constraint occurrences are list entries, so repeated parallel edges retain their multiplicity. No weights are hidden in this representation.

    theorem countSatisfied_le_length {n q : Nat} (labeling : Fin n → Fin q)
    (constraints : List (Constraint n q)) :
    countSatisfied labeling constraints ≤ constraints.length := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Constraint, OAI.UniqueGamesTheorem.Foundations.Target.countSatisfied

  36. theorem OAI.UniqueGamesTheorem.Foundations.Target.Instance.constraintCount_positive line 539
  37. structure OAI.UniqueGamesTheorem.Foundations.Target.RationalError line 547

    Source documentation

    The rational number numerator / denominator lies strictly between 0 and 1/2. No normalization to lowest terms is needed for the gap predicates.

    structure RationalError where
…
  38. def OAI.UniqueGamesTheorem.Foundations.Target.CompleteAt line 555

    Source documentation

    At least one labeling satisfies a fraction at least 1 - error.

    def CompleteAt {q : Nat} (error : RationalError) (game : Instance q) : Prop :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.RationalError, OAI.UniqueGamesTheorem.Foundations.Target.Instance

  39. def OAI.UniqueGamesTheorem.Foundations.Target.SoundAt line 562

    Source documentation

    Every labeling satisfies a fraction at most error.

    def SoundAt {q : Nat} (error : RationalError) (game : Instance q) : Prop :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.RationalError, OAI.UniqueGamesTheorem.Foundations.Target.Instance

  40. structure OAI.UniqueGamesTheorem.Foundations.Target.SemanticGapReduction line 569

    Source documentation

    Only the semantic part of a reduction. This is not a definition of an efficient reduction or an NP-hardness certificate.

    structure SemanticGapReduction (completenessError soundnessError : RationalError) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Target.RationalError