UpperBound.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniqueGamesTheorem.Clean.UpperBound.fixedAdviceSuccess line 23

Source documentation

The true weighted occurrence/position experiment at fixed visible advice.

def fixedAdviceSuccess (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (strategy : OuterStrategy (P := P) (R := R) (O := O) (N := N)) : ℝ :=
…

theorem OAI.UniqueGamesTheorem.Clean.UpperBound.reference_of_positive line 31

theorem OAI.UniqueGamesTheorem.Clean.UpperBound.conditioned_success_le_repeated_value_with_reference line 52

Source documentation

On each positive public observation fibre, the full agreement event is bounded by ordinary repetition. The reference draw is fixed public padding, not an extra input depending on the still hidden question pair.

theorem conditioned_success_le_repeated_value_with_reference
    (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (observed : PositionOutside (zeroSet J gamma) → O × N)
    (positive : 0 < (FiniteDistribution.table (fun _ : P => μ)).probability
      (fun draw => decide (outsideRecord (zeroSet J gamma) g.name draw = observed)))
    (reference : RawObservationFibre J g.name gamma observed)
    (e : Fin (zeroSet J gamma).card ≃ PositionInside (zeroSet J gamma))
    (strategy : OuterStrategy (P := P) (R := R) (O := O) (N := N))
…

theorem OAI.UniqueGamesTheorem.Clean.UpperBound.conditioned_success_le_repeated_value line 110
theorem OAI.UniqueGamesTheorem.Clean.UpperBound.fixed_advice_success_le_repeated_value line 134
Source documentation
All outside observations are genuinely averaged with their actual weights. The result permits arbitrary repeated occurrence IDs and correlated local answers across the entire clean tuple.
```
theorem fixed_advice_success_le_repeated_value
    (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (strategy : OuterStrategy (P := P) (R := R) (O := O) (N := N))
…
```