OAI/Computability/UniqueGames/Decoding/ProductLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Weighted conditional product law for the v2 clean coordinates

The equation distribution is arbitrary. All identities below are identities of finite sums of its actual weights, rather than a reduction to uniform occurrence sampling. The clean set is fixed by independently sampled advice; the only subsequently exposed question data lie outside that set. Conditioning on such data preserves the entire joint law of the clean questions.

  1. def OAI.UniqueGamesTheorem.Clean.ProductLaw.splitCoordinates line 30

    Source documentation

    Restriction to the clean and nonclean coordinates is a genuine bijection.

    def splitCoordinates (K : Finset P) :
    (P → Q) ≃ (PositionInside K → Q) × (PositionOutside K → Q) :=
…
  2. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.table_split line 36

    Source documentation

    Independent weighted sampling splits into independent clean and nonclean parts. This identity proves, rather than assumes, their independence.

    theorem table_split (μ : P → FiniteDistribution Q) (K : Finset P) :
    (FiniteDistribution.table μ).transport (splitCoordinates K) =
      (FiniteDistribution.table (fun i : PositionInside K => μ i.val)).product
        (FiniteDistribution.table (fun i : PositionOutside K => μ i.val)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Clean.ProductLaw.splitCoordinates

  3. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.probability_product_and line 60
  4. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.probability_product_right line 77
  5. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.table_inside_outside line 84

    Source documentation

    Exact factorization for an arbitrary joint event of clean coordinates and an arbitrary observation/event depending only on the nonclean coordinates.

    theorem table_inside_outside (μ : P → FiniteDistribution Q) (K : Finset P)
    (event : (PositionInside K → Q) → Bool)
    (given : (PositionOutside K → Q) → Bool) :
    (FiniteDistribution.table μ).probability
        (fun x => event (fun i => x i.val) && given (fun i => x i.val)) =
      (FiniteDistribution.table (fun i : PositionInside K => μ i.val)).probability event *
        (FiniteDistribution.table (fun i : PositionOutside K => μ i.val)).probability given := by
…
  6. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.table_outside line 95
  7. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.conditioned_inside line 103

    Source documentation

    The normalized conditional law is the ordinary independent product law. The only hypothesis is that the observed outside event has positive mass.

    theorem conditioned_inside (μ : P → FiniteDistribution Q) (K : Finset P)
    (given : (PositionOutside K → Q) → Bool)
    (positive : 0 < (FiniteDistribution.table μ).probability
      (fun x => given (fun i => x i.val)))
    (event : (PositionInside K → Q) → Bool) :
    ((FiniteDistribution.table μ).condition
      (fun x => given (fun i => x i.val)) positive).probability
        (fun x => event (fun i => x i.val)) =
      (FiniteDistribution.table (fun i : PositionInside K => μ i.val)).probability event := by
…
  8. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.seeded_inside_outside line 124

    Source documentation

    Fixing an independently sampled seed additionally exposes the intercept and all slope data, without exposing any of the clean questions. The seed's mass and the outside-observation mass factor off from every clean event.

    theorem seeded_inside_outside (ν : FiniteDistribution S)
    (μ : P → FiniteDistribution Q) (seed : S) (K : Finset P)
    (given : (PositionOutside K → Q) → Bool)
    (event : (PositionInside K → Q) → Bool) :
    (ν.product (FiniteDistribution.table μ)).probability
      (fun x => (decide (x.1 = seed) && given (fun i => x.2 i.val)) &&
        event (fun i => x.2 i.val)) =
      (FiniteDistribution.table (fun i : PositionInside K => μ i.val)).probability event *
        (ν.weight seed *
          (FiniteDistribution.table (fun i : PositionOutside K => μ i.val)).probability given) := by
…
  9. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.conditioned_seed_inside line 148

    Source documentation

    Public conditioning on the independently generated advice, including its intercept, and on arbitrary nonclean question data leaves the weighted clean product law unchanged. K may be any function of seed; it is fixed here after the public seed has been exposed.

    theorem conditioned_seed_inside (ν : FiniteDistribution S)
    (μ : P → FiniteDistribution Q) (seed : S) (K : Finset P)
    (given : (PositionOutside K → Q) → Bool)
    (positive : 0 < (ν.product (FiniteDistribution.table μ)).probability
      (fun x => decide (x.1 = seed) && given (fun i => x.2 i.val)))
    (event : (PositionInside K → Q) → Bool) :
    ((ν.product (FiniteDistribution.table μ)).condition
      (fun x => decide (x.1 = seed) && given (fun i => x.2 i.val)) positive).probability
        (fun x => event (fun i => x.2 i.val)) =
      (FiniteDistribution.table (fun i : PositionInside K => μ i.val)).probability event := by
…
  10. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.table_reindex line 164

    Source documentation

    Reindexing a finite coordinate set gives the usual iid law on Fin r.

    theorem table_reindex (μ : FiniteDistribution Q) {A : Type} [Fintype A] [DecidableEq A]
    {r : ℕ} (e : Fin r ≃ A) :
    (FiniteDistribution.table (fun _ : A => μ)).transport (coordinateReindex e) =
      μ.iid r := by
…
  11. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.conditioned_incidence_reindex line 175

    Source documentation

    Fixed advice, intercept and nonclean data preserve precisely the repeated incidence law for arbitrary occurrence weights. Repeated IDs are permitted.

    theorem conditioned_incidence_reindex
    {O N D : Type} [Fintype O] [DecidableEq O] [Fintype N] [DecidableEq N]
    [Zero D] [DecidableEq D]
    (μ : FiniteDistribution (O × Fin 3))
    (J : Finset P) (name : O → Fin 3 → N) (gamma : RawCoefficients J D)
    (observed : PositionOutside (zeroSet J gamma) → O × N)
    (positive : 0 < (FiniteDistribution.table (fun _ : P => μ)).probability
      (fun x => decide (outsideRecord (zeroSet J gamma) name x = observed)))
    {r : ℕ} (e : Fin r ≃ PositionInside (zeroSet J gamma))
    (event : (Fin r → O × N) → Bool) :
    ((FiniteDistribution.table (fun _ : P => μ)).condition
      (fun x => decide (outsideRecord (zeroSet J gamma) name x = observed))
…
  12. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.conditioned_incidence_distribution line 204

    Source documentation

    Equality of the complete conditional question distribution, not only its individual marginals. The target is the ordinary repeated incidence law.

    theorem conditioned_incidence_distribution
    {O N D : Type} [Fintype O] [DecidableEq O] [Fintype N] [DecidableEq N]
    [Zero D] [DecidableEq D]
    (μ : FiniteDistribution (O × Fin 3))
    (J : Finset P) (name : O → Fin 3 → N) (gamma : RawCoefficients J D)
    (observed : PositionOutside (zeroSet J gamma) → O × N)
    (positive : 0 < (FiniteDistribution.table (fun _ : P => μ)).probability
      (fun x => decide (outsideRecord (zeroSet J gamma) name x = observed)))
    {r : ℕ} (e : Fin r ≃ PositionInside (zeroSet J gamma)) :
    (((FiniteDistribution.table (fun _ : P => μ)).condition
      (fun x => decide (outsideRecord (zeroSet J gamma) name x = observed))
        positive).pushforward
…
  13. theorem OAI.UniqueGamesTheorem.Clean.ProductLaw.clean_mask_independent line 238

    Source documentation

    A clean-mask rule reads only the independent advice seed. Thus even after fixing the entire question tuple, its distribution is unchanged. The seed may include the projection mask, all slope columns, and the independent intercept.

    theorem clean_mask_independent (ν : FiniteDistribution S)
    (μ : FiniteDistribution Q) (clean : S → Finset P) (K : Finset P)
    (questionEvent : Q → Bool) :
    (ν.product μ).probability (fun x => decide (clean x.1 = K) && questionEvent x.2) =
      ν.probability (fun s => decide (clean s = K)) * μ.probability questionEvent := by
…