ExactSampling.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

Exact fair-bit sampling of the optimizer mixture

The finite-word rejection calculation follows Section 9. The random trial is encoded from actual Boolean bits. First-success trace probabilities determine the output law and expected number of trials.

def OAI.EditApproximation.binaryWord line 20

Source documentation

Little-endian encoding of a finite Boolean word.

def binaryWord : (B : ℕ) → (Fin B → Bool) → Fin (2 ^ B)
  | 0, _ => ⟨0, by norm_num⟩
  | B + 1, bits =>
    ⟨(if bits 0 then 1 else 0) + 2 * (binaryWord B (fun i => bits i.succ)).val, by
      have hword := (binaryWord B (fun i => bits i.succ)).isLt
…

theorem OAI.EditApproximation.binaryWord_injective line 28
theorem OAI.EditApproximation.binaryWord_bijective line 46

theorem OAI.EditApproximation.uniform_map_of_bijective line 51

Source documentation

A bijection carries the uniform finite law to the uniform finite law.

theorem uniform_map_of_bijective {α β : Type*} [Fintype α] [Fintype β]
    [Nonempty α] [Nonempty β] (f : α → β) (hf : Function.Bijective f) :
    (PMF.uniformOfFintype α).map f = PMF.uniformOfFintype β := by
…

theorem OAI.EditApproximation.binaryWord_uniform line 64
Source documentation
Independent fair Boolean words encode a uniform power-of-two range.
```
theorem binaryWord_uniform (B : ℕ) :
    (PMF.uniformOfFintype (Fin B → Bool)).map (binaryWord B) =
      PMF.uniformOfFintype (Fin (2 ^ B)) := by
…
```
Mentions: OAI.EditApproximation.binaryWord
theorem OAI.EditApproximation.rejectionWord_range line 72
Source documentation
Number of fair bits per rejection trial.
```
theorem rejectionWord_range (N : ℕ) (hN : 0 < N) :
    N ≤ 2 ^ rejectionBitCount N ∧ 2 ^ rejectionBitCount N < 2 * N := by
…
```
Mentions: OAI.EditApproximation.rejectionBitCount
def OAI.EditApproximation.rejectionTrial line 90
Source documentation
A trial accepts exactly the words lying in the requested range.
```
def rejectionTrial (N R : ℕ) (word : Fin R) : Option (Fin N) :=
…
```
def OAI.EditApproximation.rejectionPrefix line 95
Source documentation
Executable finite prefix of the rejection loop. Each failed trial is discarded before the next trial is examined.
```
def rejectionPrefix (N R : ℕ) : List (Fin R) → Option (Fin N)
  | [] => none
  | word :: words => match rejectionTrial N R word with
    | some accepted => some accepted
    | none => rejectionPrefix N R words
```
Mentions: OAI.EditApproximation.rejectionTrial
theorem OAI.EditApproximation.rejectionTrial_none_iff line 101
theorem OAI.EditApproximation.rejectionTrial_some_iff line 105
theorem OAI.EditApproximation.rejectionPrefix_none_iff line 113
theorem OAI.EditApproximation.rejectionPrefix_first_success line 127
def OAI.EditApproximation.firstSuccessEvent line 144
Source documentation
Finite traces with n failed words followed by the specified accepted integer.
```
def firstSuccessEvent (N R n : ℕ) (accepted : Fin N) :
    Set ((Fin n → Fin R) × Fin R) :=
…
```
def OAI.EditApproximation.firstSuccessEquiv line 150
Source documentation
Each failed word is represented uniquely by its offset above N; the final accepted word is fixed.
```
def firstSuccessEquiv (N R n : ℕ) (hNR : N ≤ R) (accepted : Fin N) :
    firstSuccessEvent N R n accepted ≃ (Fin n → Fin (R - N)) where
…
```
Mentions: OAI.EditApproximation.firstSuccessEvent
theorem OAI.EditApproximation.firstSuccessEvent_runs line 181
Source documentation
First-success events are actual terminating executions of the finite-prefix rejection program.
```
theorem firstSuccessEvent_runs (N R n : ℕ) (accepted : Fin N)
    (samples : (Fin n → Fin R) × Fin R) (hsamples : samples ∈ firstSuccessEvent N R n accepted) :
    rejectionPrefix N R (List.ofFn samples.1 ++ [samples.2]) = some accepted := by
…
```
Mentions: OAI.EditApproximation.firstSuccessEvent, OAI.EditApproximation.rejectionPrefix
theorem OAI.EditApproximation.firstSuccessEvent_probability line 191
Source documentation
Exact finite counting probability for n failures and then a specified accepted value, under independent uniform trial words.
```
theorem firstSuccessEvent_probability (N R n : ℕ) (hN : 0 < N) (hNR : N ≤ R)
    (accepted : Fin N) :
    let : NeZero R := ⟨by omega⟩
…
```
def OAI.EditApproximation.rejectionFailureProbability line 208
Source documentation
Rejection probability per trial.
```
noncomputable def rejectionFailureProbability (N R : ℕ) : ℝ := ((R - N : ℕ) : ℝ) / R
```
theorem OAI.EditApproximation.rejectionFailureProbability_range line 210
theorem OAI.EditApproximation.rejection_exact_output_mass line 223
Source documentation
The sum over all first-success times is exactly uniform on the requested range. This also establishes total terminating mass one.
```
theorem rejection_exact_output_mass (N R : ℕ) (hN : 0 < N) (hNR : N ≤ R) :
    HasSum (fun n : ℕ => ((R - N : ℕ) : ℝ) ^ n / ((R : ℝ) ^ n * R)) (1 / (N : ℝ)) := by
…
```
theorem OAI.EditApproximation.rejection_expected_trials line 242
Source documentation
The expected rejection-loop trial count is the sum of its failure tails, namely R/N.
```
theorem rejection_expected_trials (N R : ℕ) (hN : 0 < N) (hNR : N ≤ R) :
    HasSum (fun n : ℕ => rejectionFailureProbability N R ^ n) ((R : ℝ) / N) := by
…
```
Mentions: OAI.EditApproximation.rejectionFailureProbability
theorem OAI.EditApproximation.rejection_fair_bits_expected_trials_lt_two line 254
theorem OAI.EditApproximation.rejection_first_success_expected_trials line 263
Source documentation
The actual first-success trace law has expected trial count R/N; this identifies the tail-sum calculation with the terminating executions.
```
theorem rejection_first_success_expected_trials (N R : ℕ) (hN : 0 < N) (hNR : N ≤ R) :
    HasSum (fun n : ℕ => ((n : ℝ) + 1) * N *
      (((R - N : ℕ) : ℝ) ^ n / ((R : ℝ) ^ n * R))) ((R : ℝ) / N) := by
…
```
def OAI.EditApproximation.rejectionTransition line 296
Source documentation
A streaming rejection sampler only retains its current accepted value and the current bounded-width random word.
```
def rejectionTransition (N R : ℕ) (state : Option (Fin N)) (word : Fin R) : Option (Fin N) :=
…
```
theorem OAI.EditApproximation.rejectionTransition_absorbs line 301
theorem OAI.EditApproximation.rejection_fixed_state_space line 305
Source documentation
The sampler state space is independent of the number of failures.
```
theorem rejection_fixed_state_space (N R : ℕ) :
    Fintype.card (Option (Fin N)) = N + 1 ∧ Fintype.card (Fin R) = R := by
…
```
theorem OAI.EditApproximation.rejection_output_is_uniform line 311
Source documentation
Summing the first-success trace probabilities gives exactly the probability of each value in the uniform target distribution.
```
theorem rejection_output_is_uniform (N R : ℕ) (hN : 0 < N) (hNR : N ≤ R)
    (accepted : Fin N) :
    let : NeZero N := ⟨Nat.ne_of_gt hN⟩
…
```

theorem OAI.EditApproximation.rejection_terminating_mass line 321

Source documentation

Total mass of terminating rejection executions is one.

theorem rejection_terminating_mass (N R : ℕ) (hN : 0 < N) (hNR : N ≤ R) :
    (∑ _ : Fin N, ∑' n : ℕ, ((R - N : ℕ) : ℝ) ^ n / ((R : ℝ) ^ n * R)) = 1 := by
…

theorem OAI.EditApproximation.fair_bit_word_probability line 329

Source documentation

The finite fair-word law factors into the independent fair-bit laws.

theorem fair_bit_word_probability (B : ℕ) (bits : Fin B → Bool) :
    PMF.uniformOfFintype (Fin B → Bool) bits =
      ∏ i : Fin B, PMF.uniformOfFintype Bool (bits i) := by
…

theorem OAI.EditApproximation.rejection_fair_bits_failure_lt_half line 334
theorem OAI.EditApproximation.optimizerTriangularMass_monotone line 344
theorem OAI.EditApproximation.optimizerTriangularMass_positive line 350

theorem OAI.EditApproximation.triangularChoice_fiber line 361

Source documentation

The lookup assigns precisely the j+1 integers in block j.

theorem triangularChoice_fiber (K : ℕ) (integer : Fin (optimizerTriangularMass K))
    (j : ℕ) (hj : j < K) :
    (triangularChoice K integer).val = j ↔
      optimizerTriangularMass j ≤ integer.val ∧ integer.val < optimizerTriangularMass (j + 1) := by
…

Mentions: OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.triangularChoice

def OAI.EditApproximation.triangularChoiceFiberEquiv line 395
Source documentation
Each triangular lookup fiber is exactly a finite interval of the claimed integer length.
```
def triangularChoiceFiberEquiv (K j : ℕ) (hj : j < K) :
    {integer : Fin (optimizerTriangularMass K) // (triangularChoice K integer).val = j} ≃ Fin (j + 1) where
…
```
Mentions: OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.triangularChoice
theorem OAI.EditApproximation.triangularChoice_fiber_card line 424
theorem OAI.EditApproximation.triangularChoice_uniform_weights line 431
Source documentation
Uniform integer rejection followed by triangular lookup gives the stored exact optimizer weights.
```
theorem triangularChoice_uniform_weights (K : ℕ) (hK : 0 < K) (j : Fin K) :
    let : NeZero (optimizerTriangularMass K) := ⟨Nat.ne_of_gt (optimizerTriangularMass_positive K hK)⟩
…
```
Mentions: OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.optimizerTriangularMass_positive
theorem OAI.EditApproximation.triangularChoice_coordinate_mean line 454
Source documentation
Exact coordinate mean of the sampler, including repeated selected actions, equals the actual rational optimizer iterate.
```
theorem triangularChoice_coordinate_mean {ι : Type*} (initial : ι → ℚ)
    (selected : ℕ → ι → ℚ) (K : ℕ) (hK : 0 < K) (i : ι) :
    (∑ integer : Fin (optimizerTriangularMass K), selected (triangularChoice K integer).val i) /
        optimizerTriangularMass K = rationalOptimizerIterate initial selected K i := by
…
```
Mentions: OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.triangularChoice, OAI.EditApproximation.rationalOptimizerIterate

theorem OAI.EditApproximation.finiteRationalOptimizer_sampler_mean line 475

Source documentation

The exactly sampled action has the mean computed by the finite rational optimizer, with no distinction assumption on its selections.

theorem finiteRationalOptimizer_sampler_mean {ι : Type*} (coordinates : Finset ι)
    (vertices : List (ι → ℚ)) (linear : ι → ℚ) (G K : ℕ) (hK : 0 < K) (i : ι) :
    (∑ integer : Fin (optimizerTriangularMass K),
      finiteOptimizerSelection coordinates vertices linear G (triangularChoice K integer).val i) /
        optimizerTriangularMass K = finiteRationalOptimizer coordinates vertices linear G K i := by
…

Mentions: OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.finiteOptimizerSelection, OAI.EditApproximation.triangularChoice, OAI.EditApproximation.finiteRationalOptimizer