FirstSuccess.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

First-success law and finite-law error bounds

The bounded outer sampler repeats independent trials and uses a fixed feasible fallback. Its geometric output law has a stationary uniform-mixture specialization. Total-variation bounds are preserved by deterministic output maps.

def OAI.ContingencyTables.FirstSuccess.variation line 24
lemma OAI.ContingencyTables.FirstSuccess.variation_nonnegative line 27
lemma OAI.ContingencyTables.FirstSuccess.geometric_balance line 30
def OAI.ContingencyTables.FirstSuccess.outputMass line 39
Source documentation
The exact first-success-or-fallback mass from the manuscript.
```
def outputMass [DecidableEq α] (g : α → ℚ) (f : ℚ) (J : ℕ) (fallback z : α) : ℚ :=
…
```
lemma OAI.ContingencyTables.FirstSuccess.outputMass_nonnegative line 43
lemma OAI.ContingencyTables.FirstSuccess.outputMass_total line 50
def OAI.ContingencyTables.FirstSuccess.outputLaw line 59
def OAI.ContingencyTables.FirstSuccess.uniformLaw line 68
theorem OAI.ContingencyTables.FirstSuccess.stationary_output_mass line 77
Source documentation
Successful stationary pairs have equal mass; the repeated-trial law is exactly a uniform law mixed with the fallback, without conditioning on the implemented approximate trial's success.
```
theorem stationary_output_mass [DecidableEq α] (s : ℚ) (J : ℕ) (fallback z : α) :
    outputMass (fun _ => s * uniformMass (α := α)) (1 - s) J fallback z =
…
```
Mentions: OAI.ContingencyTables.FirstSuccess.outputMass
lemma OAI.ContingencyTables.FirstSuccess.point_mass_variation line 88
theorem OAI.ContingencyTables.FirstSuccess.stationary_variation line 104
Source documentation
The stationary repeated-trial error is at most the probability that all trials fail. No error term is divided by a success probability.
```
theorem stationary_variation [DecidableEq α] (s : ℚ) (_hs0 : 0 ≤ s) (hs1 : s ≤ 1)
    (J : ℕ) (fallback : α) :
    (∑ z, |outputMass (fun _ => s * uniformMass (α := α)) (1 - s) J fallback z -
…
```
Mentions: OAI.ContingencyTables.FirstSuccess.outputMass
def OAI.ContingencyTables.FirstSuccess.mapLaw line 127
theorem OAI.ContingencyTables.FirstSuccess.variation_map line 140
Source documentation
Deterministic postprocessing contracts total variation, as used for the map selecting the first successful trial and unpadding its table.
```
theorem variation_map [DecidableEq β] (p q : RationalLaw α) (f : α → β) :
    variation (mapLaw p f) (mapLaw q f) ≤ variation p q := by
…
```
Mentions: OAI.ContingencyTables.FirstSuccess.variation, OAI.ContingencyTables.FirstSuccess.mapLaw
def OAI.ContingencyTables.FirstSuccess.productLaw line 165
theorem OAI.ContingencyTables.FirstSuccess.variation_product line 174
Source documentation
Independent trials accumulate their errors additively, before the deterministic first-success map is applied.
```
theorem variation_product (p q : RationalLaw α) (r s : RationalLaw β) :
    variation (productLaw p r) (productLaw q s) ≤ variation p q + variation r s := by
…
```
Mentions: OAI.ContingencyTables.FirstSuccess.variation, OAI.ContingencyTables.FirstSuccess.productLaw