ActualProjectedTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The full selected-witness argument on the actual projected experiment. The variation comparison precedes all conditioning. Its visible event then pays the independent private decoder success on every selected datum.

def OAI.UniqueGamesTheorem.Decoder.ActualProjectedTransfer.slopeVariation line 29
theorem OAI.UniqueGamesTheorem.Decoder.ActualProjectedTransfer.visible_mass line 37
Source documentation
The actual complete-data event has positive mass depending only on the fixed inverse and alphabet parameters.
```
theorem visible_mass (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α g₀ β : ℝ) (hα : 0 < α) (hβ : 0 ≤ β) (hβ' : β ≤ 1)
    (hgood : g₀ ≤ ActualGoodRows.adviceMass S k s d r labeling α)
    (hvariation : slopeVariation k s d β ≤ ConstantSelection.variationBudget α g₀ s r) :
    ConstantSelection.visibleMass α g₀ s r ≤
      ((ActualSeedEvents.law S k s d r β hβ hβ').pushforward AdviceLaw.completeObserve).probability
        (VisibleTransfer.visibleWitness (ActualSeedEvents.law S k s d r β hβ hβ')
          AdviceLaw.completeObserve (ActualSeedEvents.slice S k s d r labeling α)
          (ActualSeedEvents.targetHit S k s d r labeling α) (α / 4)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.adviceMass, OAI.UniqueGamesTheorem.Decoder.ActualProjectedTransfer.slopeVariation, OAI.UniqueGamesTheorem.Decoder.ConstantSelection.variationBudget, OAI.UniqueGamesTheorem.Decoder.ConstantSelection.visibleMass, OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.law, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.completeObserve, OAI.UniqueGamesTheorem.Decoder.VisibleTransfer.visibleWitness, OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.slice, OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.targetHit

theorem OAI.UniqueGamesTheorem.Decoder.ActualProjectedTransfer.event_expectation_lower line 64

Source documentation

Integrating a pointwise lower bound over a genuine probability event.

theorem event_expectation_lower {Ω : Type*} [Fintype Ω]
    (μ : FiniteDistribution Ω) (event : Ω → Bool) (f : Ω → ℝ)
    (γ₁ γ₂ : ℝ) (hγ₂ : 0 ≤ γ₂) (hf : ∀ x, 0 ≤ f x)
    (hmass : γ₁ ≤ μ.probability event)
    (hpoint : ∀ x, event x = true → γ₂ ≤ f x) :
    γ₁ * γ₂ ≤ μ.expectation f := by
…

theorem OAI.UniqueGamesTheorem.Decoder.ActualProjectedTransfer.actual_success_lower line 84
Source documentation
End-to-end lower bound for actual local stochastic responses. No hidden matrix, selected witness, or opposing observation is passed to a prover.
```
theorem actual_success_lower (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (α g₀ β : ℝ) (hα : 0 < α)
    (hsmall : 1 / (2 : ℝ) ^ (s - r) < α / 8)
    (hβ : 0 ≤ β) (hβ' : β ≤ 1)
    (hgood : g₀ ≤ ActualGoodRows.adviceMass S k s d r labeling α)
    (hvariation : slopeVariation k s d β ≤ ConstantSelection.variationBudget α g₀ s r) :
    ConstantSelection.decodingMass α g₀ s r ≤
      (ActualSeedEvents.law S k s d r β hβ hβ').expectation
        (fun seed => VisiblePolicies.observedAgreement S labeling
          (SelectedPolicies.goodPredicate S labeling α hα hsmall)
          (AdviceLaw.seedToActualDraw seed.1.1 seed.1.2 seed.2)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Decoder.TableKeysGame.vertexCount, OAI.UniqueGamesTheorem.Decoder.ActualGoodRows.adviceMass, OAI.UniqueGamesTheorem.Decoder.ActualProjectedTransfer.slopeVariation, OAI.UniqueGamesTheorem.Decoder.ConstantSelection.variationBudget, OAI.UniqueGamesTheorem.Decoder.ConstantSelection.decodingMass, OAI.UniqueGamesTheorem.Decoder.ActualSeedEvents.law, OAI.UniqueGamesTheorem.Decoder.VisiblePolicies.observedAgreement, OAI.UniqueGamesTheorem.Decoder.SelectedPolicies.goodPredicate, OAI.UniqueGamesTheorem.Decoder.AdviceLaw.seedToActualDraw