FiniteRepetition.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Independent complete rounds and the fixed finite repetition schedule

The product law retains both actual outcomes, including sampler exhaustion. Repetition draws fresh complete rounds and accepts if any round accepts.

def OAI.LowSpaceSubsetSum.FiniteLaw.prod line 26
Source documentation
Independent actual outcomes. A failure value in either coordinate does not prevent the other coordinate from being drawn.
```
def prod (μ : FiniteLaw Ω) (ν : FiniteLaw Ψ) : FiniteLaw (Ω × Ψ) where
…
```
Mentions: OAI.LowSpaceSubsetSum.FiniteLaw
theorem OAI.LowSpaceSubsetSum.FiniteLaw.prod_first_probability line 34
theorem OAI.LowSpaceSubsetSum.FiniteLaw.prod_second_probability line 44
theorem OAI.LowSpaceSubsetSum.FiniteLaw.prod_or_ge_left line 55
theorem OAI.LowSpaceSubsetSum.FiniteLaw.prod_or_ge_right line 61
def OAI.LowSpaceSubsetSum.FiniteLaw.pi line 68
Source documentation
Fresh independent draws, allowing a different finite law at each index.
```
def pi {I : Type*} [Fintype I] [DecidableEq I] (A : I → Type*) [∀ i, Fintype (A i)]
    (μ : ∀ i, FiniteLaw (A i)) : FiniteLaw (∀ i, A i) where
…
```
Mentions: OAI.LowSpaceSubsetSum.FiniteLaw
theorem OAI.LowSpaceSubsetSum.FiniteLaw.pi_forall_probability line 77
def OAI.LowSpaceSubsetSum.FiniteLaw.iid line 93
theorem OAI.LowSpaceSubsetSum.FiniteLaw.iid_forall_probability line 96
theorem OAI.LowSpaceSubsetSum.FiniteLaw.iid_exists_probability line 101
def OAI.LowSpaceSubsetSum.repeatAccept line 114
Source documentation
The executable finite OR of complete trial outcomes.
```
def repeatAccept {Ω : Type*} {k : ℕ} (test : Ω → Bool) (draws : Fin k → Ω) : Bool :=
…
```
theorem OAI.LowSpaceSubsetSum.repeatAccept_eq_true line 117
theorem OAI.LowSpaceSubsetSum.repeatAccept_sound line 122
theorem OAI.LowSpaceSubsetSum.repetition_acceptance_probability line 128
def OAI.LowSpaceSubsetSum.optionAccept line 142
Source documentation
Exhaustion is a rejecting actual outcome, without conditioning the law.
```
def optionAccept {α : Type*} (test : α → Bool) : Option α → Bool
  | none => false
  | some x => test x
```
theorem OAI.LowSpaceSubsetSum.optionAccept_eq_true line 146
theorem OAI.LowSpaceSubsetSum.bounded_repetition_acceptance_probability line 150