OAI/Computability/UniqueGames/Decoding/WeightedPartition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Weighted total probability for the public clean-coordinate observation. The observation may have zero-probability fibres. Only its positive fibres require a conditional bound; the identity itself is proved from finite sums.

  1. def OAI.UniqueGamesTheorem.Clean.WeightedPartition.fibre line 23
  2. theorem OAI.UniqueGamesTheorem.Clean.WeightedPartition.sum_fibre_inter line 26
  3. theorem OAI.UniqueGamesTheorem.Clean.WeightedPartition.sum_fibre_bound line 37
  4. theorem OAI.UniqueGamesTheorem.Clean.WeightedPartition.probability_le_conditional_bounds line 52

    Source documentation

    The averaging step for a genuine weighted observation. No conditional independence or law-of-total-probability equality is supplied as a premise.

    theorem probability_le_conditional_bounds (μ : FiniteDistribution Ω)
    (observe : Ω → H) (event : Ω → Bool) (bound : H → ℝ)
    (conditional : ∀ h (positive : 0 < μ.probability (fibre observe h)),
      (μ.condition (fibre observe h) positive).probability event ≤ bound h) :
    μ.probability event ≤ μ.expectation (fun x => bound (observe x)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Clean.WeightedPartition.fibre

  5. theorem OAI.UniqueGamesTheorem.Clean.WeightedPartition.probability_le_of_conditional_le line 69

    Source documentation

    A constant bound survives arbitrary public outside observations.

    theorem probability_le_of_conditional_le (μ : FiniteDistribution Ω)
    (observe : Ω → H) (event : Ω → Bool) (bound : ℝ)
    (conditional : ∀ h (positive : 0 < μ.probability (fibre observe h)),
      (μ.condition (fibre observe h) positive).probability event ≤ bound) :
    μ.probability event ≤ bound := by
…

    Mentions: OAI.UniqueGamesTheorem.Clean.WeightedPartition.fibre