FiniteSamplerCoupling.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Explicit finite couplings for dependent bounded samplers

The source retains fresh candidate tuples and independent backup choices. The backup is used only by the ideal completion of an exhausted call; the bounded output is none at that point. No law is conditioned on every call succeeding.

def OAI.LowSpaceSubsetSum.FiniteLaw.map line 25
def OAI.LowSpaceSubsetSum.FiniteLaw.expectation line 34
theorem OAI.LowSpaceSubsetSum.FiniteLaw.map_expectation line 36
theorem OAI.LowSpaceSubsetSum.FiniteLaw.probability_eq_expectation line 45
theorem OAI.LowSpaceSubsetSum.FiniteLaw.map_probability line 50
theorem OAI.LowSpaceSubsetSum.FiniteLaw.probability_or_le line 55
structure OAI.LowSpaceSubsetSum.SamplerCoupling line 67
Source documentation
An explicit common probability space for an ideal result and a bounded result. Every nonfailure agrees exactly; failure remains part of the law.
```
structure SamplerCoupling (α : Type*) [Fintype α] where
…
```
instance OAI.LowSpaceSubsetSum.SamplerCoupling.(instance at line 79) line 79
def OAI.LowSpaceSubsetSum.SamplerCoupling.idealLaw line 81
def OAI.LowSpaceSubsetSum.SamplerCoupling.boundedLaw line 83
def OAI.LowSpaceSubsetSum.SamplerCoupling.failure line 85
def OAI.LowSpaceSubsetSum.SamplerCoupling.pure line 87
def OAI.LowSpaceSubsetSum.SamplerCoupling.bind line 95

theorem OAI.LowSpaceSubsetSum.SamplerCoupling.bind_ideal_probability line 112

Source documentation

The ideal marginal follows the exact prescribed conditional laws.

theorem bind_ideal_probability (S : SamplerCoupling α) (β : α → Type)
    [∀ a, Fintype (β a)] (T : ∀ a, SamplerCoupling (β a))
    (P : (Σ a, β a) → Prop) :
    (S.bind β T).idealLaw.probability P =
      (S.idealLaw.bind β (fun a => (T a).idealLaw)).probability P := by
…

Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling, OAI.LowSpaceSubsetSum.SamplerCoupling.idealLaw

theorem OAI.LowSpaceSubsetSum.SamplerCoupling.bind_failure_le line 135
Source documentation
The probability of first divergence is at most the previous loss plus the uniform conditional bound for the next call.
```
theorem bind_failure_le (S : SamplerCoupling α) (β : α → Type)
    [∀ a, Fintype (β a)] (T : ∀ a, SamplerCoupling (β a))
    (δ : ℝ) (hT : ∀ a, (T a).failure ≤ δ) :
    (S.bind β T).failure ≤ S.failure + δ := by
…
```
Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling, OAI.LowSpaceSubsetSum.SamplerCoupling.failure
theorem OAI.LowSpaceSubsetSum.SamplerCoupling.event_lower line 165
Source documentation
Every ideal event loses at most the unconditional coupling failure.
```
theorem event_lower (S : SamplerCoupling α) (P : α → Prop) :
    S.idealLaw.probability P - S.failure ≤
      S.boundedLaw.probability (fun x => ∃ a, x = some a ∧ P a) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling