ResidualMixture.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Exact correction by a finite residual mixture

Finite probability arithmetic gives the residual correction used in exact sampling. The construction is that of Göbel, Liu, Manurangsi and Pappik, Perfect sampling from rapidly mixing Markov chains, arXiv:2410.00882v2 (2024), §3.1, Algorithm 1 and Theorem 6.

All probabilities are rational, as required for the finite fair-bit sampler.

structure OAI.ContingencyTables.ResidualMixture.RationalLaw line 28
Source documentation
A finite probability law with exactly represented rational masses.
```
structure RationalLaw (α : Type*) [Fintype α] where
…
```
lemma OAI.ContingencyTables.ResidualMixture.card_pos line 35
def OAI.ContingencyTables.ResidualMixture.uniformMass line 39
Source documentation
The uniform mass on a nonempty finite space.
```
def uniformMass : ℚ := 1 / Fintype.card α
```
lemma OAI.ContingencyTables.ResidualMixture.uniformMass_pos line 41
lemma OAI.ContingencyTables.ResidualMixture.uniformMass_total line 44
def OAI.ContingencyTables.ResidualMixture.residualMass line 49
Source documentation
The residual point mass used on the rare correction branch.
```
def residualMass (p : RationalLaw α) (δ : ℚ) (x : α) : ℚ :=
…
```
Mentions: OAI.ContingencyTables.ResidualMixture.RationalLaw
lemma OAI.ContingencyTables.ResidualMixture.approximate_domination line 54
Source documentation
The pointwise approximation and cardinality bound imply domination. This is the estimate immediately before the definition of r(z) in 200-01.
```
lemma approximate_domination (p : RationalLaw α) {δ : ℚ}
    (hδ : 0 < δ) (hδone : δ ≤ 1)
    (hcard : (Fintype.card α : ℚ) * δ ≤ 1)
    (happrox : ∀ x, p.mass x ≤ uniformMass (α := α) + δ ^ 2) (x : α) :
…
```
Mentions: OAI.ContingencyTables.ResidualMixture.RationalLaw, OAI.ContingencyTables.ResidualMixture.uniformMass
lemma OAI.ContingencyTables.ResidualMixture.residualMass_nonnegative line 71
lemma OAI.ContingencyTables.ResidualMixture.residualMass_total line 76
def OAI.ContingencyTables.ResidualMixture.residualLaw line 85
Source documentation
A residual law exists whenever the ordinary branch is pointwise dominated by the target law. No additional existence assumption is used.
```
def residualLaw (p : RationalLaw α) {δ : ℚ} (hδ : 0 < δ)
    (hdom : ∀ x, (1 - δ) * p.mass x ≤ uniformMass (α := α)) : RationalLaw α where
…
```
Mentions: OAI.ContingencyTables.ResidualMixture.RationalLaw, OAI.ContingencyTables.ResidualMixture.uniformMass
theorem OAI.ContingencyTables.ResidualMixture.mixture_exact line 93
Source documentation
The two branches combine to give exactly uniform point masses.
```
theorem mixture_exact (p : RationalLaw α) {δ : ℚ} (hδ : δ ≠ 0) (x : α) :
    (1 - δ) * p.mass x + δ * residualMass p δ x = uniformMass (α := α) := by
…
```
Mentions: OAI.ContingencyTables.ResidualMixture.RationalLaw, OAI.ContingencyTables.ResidualMixture.residualMass, OAI.ContingencyTables.ResidualMixture.uniformMass
theorem OAI.ContingencyTables.ResidualMixture.exact_correction line 101
Source documentation
The complete finite residual-mixture consequence of the pointwise approximation bound used by the manuscript.
```
theorem exact_correction (p : RationalLaw α) {δ : ℚ}
    (hδ : 0 < δ) (hδone : δ ≤ 1)
    (hcard : (Fintype.card α : ℚ) * δ ≤ 1)
    (happrox : ∀ x, p.mass x ≤ uniformMass (α := α) + δ ^ 2) :
…
```
Mentions: OAI.ContingencyTables.ResidualMixture.RationalLaw, OAI.ContingencyTables.ResidualMixture.uniformMass
def OAI.ContingencyTables.ResidualMixture.residualNumerator line 112
Source documentation
The integer numerator in equation eq:residual-integers of 200-01. Here Q = 2^R, T = 2^D, and a x is the tabulated dyadic numerator.
```
def residualNumerator (Q T : ℤ) (a : α → ℤ) (x : α) : ℤ :=
…
```
lemma OAI.ContingencyTables.ResidualMixture.residualNumerator_total line 117
Source documentation
The residual integer weights have the exact required total.
```
lemma residualNumerator_total (Q T : ℤ) (a : α → ℤ) (ha : ∑ x, a x = Q) :
    ∑ x, residualNumerator Q T a x = (Fintype.card α : ℤ) * Q := by
…
```
Mentions: OAI.ContingencyTables.ResidualMixture.residualNumerator
lemma OAI.ContingencyTables.ResidualMixture.residualNumerator_quotient line 124
Source documentation
The numerator realizes the residual law exactly as a rational quotient.
```
lemma residualNumerator_quotient (Q T : ℤ) (a : α → ℤ)
    (hQ : Q ≠ 0) (hT : T ≠ 0) (x : α) :
    (residualNumerator Q T a x : ℚ) /
        ((Fintype.card α : ℚ) * Q) =
      (uniformMass (α := α) - (1 - 1 / (T : ℚ)) * ((a x : ℚ) / Q)) /
…
```
Mentions: OAI.ContingencyTables.ResidualMixture.residualNumerator, OAI.ContingencyTables.ResidualMixture.uniformMass
lemma OAI.ContingencyTables.ResidualMixture.residualNumerator_nonnegative line 139
Source documentation
Pointwise domination makes the actual integer correction weights nonnegative, so their cumulative sums define a finite exact draw.
```
lemma residualNumerator_nonnegative {Q T : ℤ} (a : α → ℤ)
    (hQ : 0 < Q) (hT : 0 < T)
    (hdom : ∀ x, (1 - 1 / (T : ℚ)) * ((a x : ℚ) / Q) ≤
      uniformMass (α := α)) (x : α) :
…
```
Mentions: OAI.ContingencyTables.ResidualMixture.uniformMass
lemma OAI.ContingencyTables.ResidualMixture.integer_rejection_acceptance line 159
Source documentation
Acceptance of a dyadic proposal has probability greater than one half when the proposal range is less than twice the target range. This is the probability estimate for the manuscript's exact integer rejection draw.
```
lemma integer_rejection_acceptance {V Q : ℕ} (hV : 0 < V)
    (hcover : V ≤ Q) (hshort : Q < 2 * V) :
    (1 / 2 : ℚ) < (V : ℚ) / Q ∧ (V : ℚ) / Q ≤ 1 := by
…
```

lemma OAI.ContingencyTables.ResidualMixture.expected_cost_bound line 172

Source documentation

A branch with probability δ and conditional cost correction adds at most the permitted rare-branch allowance to the ordinary cost bound.

lemma expected_cost_bound {δ ordinary correction allowance : ℚ}
    (hδ : 0 ≤ δ) (hordinary : 0 ≤ ordinary)
    (hrare : δ * correction ≤ allowance) :
    (1 - δ) * ordinary + δ * correction ≤ ordinary + allowance := by
…