OAI/Computability/UniqueGames/Decoding/UniformConditioning.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A finite experiment whose sample weights are constant on the selected event becomes exactly uniform after conditioning on that event. The event is allowed to have arbitrary positive mass, so this applies after the complete visible datum and the chosen column constraints have both been fixed.

  1. theorem OAI.UniqueGamesTheorem.Decoder.UniformConditioning.sum_over_event line 25
  2. theorem OAI.UniqueGamesTheorem.Decoder.UniformConditioning.probability_as_subtype_sum line 30
  3. theorem OAI.UniqueGamesTheorem.Decoder.UniformConditioning.probability_and_as_subtype_sum line 34
  4. theorem OAI.UniqueGamesTheorem.Decoder.UniformConditioning.probability_of_constant_weight line 46
  5. theorem OAI.UniqueGamesTheorem.Decoder.UniformConditioning.condition_probability_uniform line 60

    Source documentation

    Every remaining point receives equal conditional weight. Positivity of the conditioning event justifies cancellation; no unconditional uniform law on the original ambient experiment is required.

    theorem condition_probability_uniform (μ : FiniteDistribution Ω)
    (given event : Ω → Bool) (positive : 0 < μ.probability given)
    (c : ℝ) (hconstant : ∀ x, given x = true → μ.weight x = c) :
    (μ.condition given positive).probability event =
      𝔼 x : {x : Ω // given x = true}, if event x.val then (1 : ℝ) else 0 := by
…
  6. theorem OAI.UniqueGamesTheorem.Decoder.UniformConditioning.condition_probability_equiv line 88

    Source documentation

    A proved bijection with the actual affine matrix slice identifies the conditional target probability with that slice's complete uniform average.

    theorem condition_probability_equiv {Y : Type*} [Fintype Y]
    (μ : FiniteDistribution Ω) (given event : Ω → Bool)
    (positive : 0 < μ.probability given) (c : ℝ)
    (hconstant : ∀ x, given x = true → μ.weight x = c)
    (e : {x : Ω // given x = true} ≃ Y) (target : Y → Bool)
    (hevent : ∀ x, event x.val = target (e x)) :
    (μ.condition given positive).probability event =
      𝔼 y : Y, if target y then (1 : ℝ) else 0 := by
…