VisibleTransferLemmas.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.fiberEvent line 21
Source documentation
The part of an event in one actual visible-data fiber.
```
def fiberEvent (observe : Ω → D) (d : D) (event : Ω → Bool) : Ω → Bool := by
…
```
def OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.fiberMass line 25
theorem OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.fiberMass_nonnegative line 30
theorem OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.fiberMass_mono line 35
theorem OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.sum_fiberMass line 44
theorem OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.observation_weight line 54
def OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.visibleWitness line 62
Source documentation
Positive projected column-slice mass and sufficient conditional target agreement. Both quantities are computed after fixing actual visible data.
```
def visibleWitness (μ : FiniteDistribution Ω) (observe : Ω → D)
    (slice targetHit : Ω → Bool) (threshold : ℝ) (d : D) : Bool := by
…
```

theorem OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.witness_margin_le_visible_probability line 71

Source documentation

The positive part of the witness margin is paid for by the probability of the actual observed data, rather than by the larger hidden sample space.

theorem witness_margin_le_visible_probability
    (μ : FiniteDistribution Ω) (observe : Ω → D)
    (slice targetHit : Ω → Bool) (threshold : ℝ) (hthreshold : 0 ≤ threshold) :
    μ.probability (fun x => slice x && targetHit x) - threshold * μ.probability slice ≤
      (μ.pushforward observe).probability (visibleWitness μ observe slice targetHit threshold) := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.visibleWitness

theorem OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.visibleWitness_conditional line 114

Source documentation

On every selected datum the conditional distribution is defined on an actual nonempty positive-mass slice and has the promised target agreement.

theorem visibleWitness_conditional
    (μ : FiniteDistribution Ω) (observe : Ω → D)
    (slice targetHit : Ω → Bool) (threshold : ℝ) (d : D)
    (h : visibleWitness μ observe slice targetHit threshold d = true) :
    ∃ hpositive : 0 < μ.probability (fiberEvent observe d slice),
      threshold ≤ (μ.condition (fiberEvent observe d slice) hpositive).probability targetHit := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.visibleWitness, OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.fiberEvent

theorem OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.visibleWitness_good line 138

Source documentation

Goodness is inherited from any event whose membership requires good visible advice. Positivity supplies an actual supporting hidden sample.

theorem visibleWitness_good
    (μ : FiniteDistribution Ω) (observe : Ω → D)
    (slice targetHit : Ω → Bool) (threshold : ℝ)
    (good : D → Prop) (hslice : ∀ x, slice x = true → good (observe x))
    (d : D) (h : visibleWitness μ observe slice targetHit threshold d = true) :
    good d := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.visibleWitness

theorem OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.margin_transfer line 162

Source documentation

A pair of full-table event probabilities transfers with error (1 + threshold) * TV. This estimate precedes all conditioning.

theorem margin_transfer (μ ν : FiniteDistribution Ω)
    (slice targetHit : Ω → Bool) (threshold : ℝ) (hthreshold : 0 ≤ threshold) :
    μ.probability (fun x => slice x && targetHit x) - threshold * μ.probability slice -
        (1 + threshold) * μ.totalVariation ν ≤
      ν.probability (fun x => slice x && targetHit x) - threshold * ν.probability slice := by
…

theorem OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.wholeTable_transfer_to_visibleWitness line 175

Source documentation

The whole-table comparison and the exact finite disintegration combine without any assumption on conditional projection laws.

theorem wholeTable_transfer_to_visibleWitness
    {Γ : Type*} [Fintype Γ]
    (unrestricted : FiniteDistribution Ω) (actual : FiniteDistribution Γ)
    (pad : Γ → Ω) (observe : Γ → D) (slice targetHit : Ω → Bool)
    (threshold γ : ℝ) (hthreshold : 0 ≤ threshold)
    (hmargin : γ ≤
      unrestricted.probability (fun x => slice x && targetHit x) -
        threshold * unrestricted.probability slice -
        (1 + threshold) * unrestricted.totalVariation (actual.pushforward pad)) :
    γ ≤ (actual.pushforward observe).probability
      (visibleWitness actual observe (fun x => slice (pad x))
        (fun x => targetHit (pad x)) threshold) := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.visibleWitness

theorem OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.projected_witness_mass line 194
def OAI.UniqueGamesTheorem.Decoder.UniformFibers.selectedFiberEquiv line 228
theorem OAI.UniqueGamesTheorem.Decoder.UniformFibers.selectedFiberEquiv_point line 248

theorem OAI.UniqueGamesTheorem.Decoder.UniformFibers.conditional_probability line 256

Source documentation

Conditioning after fixing the complete datum and the selected column event leaves precisely the uniform restricted private fiber.

theorem conditional_probability [Fintype Ω] [Fintype Y]
    (μ : FiniteDistribution Ω) (observe : Ω → D) (d : D)
    (slice event : Ω → Bool)
    (positive : 0 < μ.probability (VisibleTransfer.fiberEvent observe d slice))
    (c : ℝ) (hconstant : ∀ x, observe x = d → μ.weight x = c)
    (e : Y ≃ {x : Ω // observe x = d}) :
    (μ.condition (VisibleTransfer.fiberEvent observe d slice) positive).probability event =
      𝔼 y : {y : Y // slice (e y).val = true},
        if event (e y.val).val then (1 : ℝ) else 0 := by
…

Mentions: OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.fiberEvent