IndependentSwitchParameters.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The measurable event of successful independent switch parameters

abbrev OAI.PolycyclicRecognition.SwitchParameters line 17
Source documentation
Two independent samples per switch, in their prescribed order.
```
abbrev SwitchParameters (G : Type u) : ℕ → Type u
  | 0 => PUnit
  | k + 1 => G × G × SwitchParameters G k
```
instance OAI.PolycyclicRecognition.switchParametersMeasurableSpace line 21
def OAI.PolycyclicRecognition.switchParameterLaw line 30
instance OAI.PolycyclicRecognition.switchParameterLaw_isProbability line 35

def OAI.PolycyclicRecognition.SwitchSuccessful line 47

Source documentation

A parameter is successful precisely when every intermediate state belongs to the next retained set.

def SwitchSuccessful (S : ℕ → Set G) :
    (n k : ℕ) → G → SwitchParameters G k → Prop
  | _, 0, _, _ => True
  | n, k + 1, x, p =>
    x * p.1 * p.2.1⁻¹ ∈ S (n + 1) ∧
      SwitchSuccessful S (n + 1) k (x * p.1 * p.2.1⁻¹) p.2.2

Mentions: OAI.PolycyclicRecognition.SwitchParameters

theorem OAI.PolycyclicRecognition.measurableSet_switchSuccessful line 54
theorem OAI.PolycyclicRecognition.measurableSet_switchSuccessful_fixed line 66
theorem OAI.PolycyclicRecognition.switchParameterLaw_success line 73
Source documentation
The recursive survival integral equals the probability of the actual measurable successful-parameter event under the independent product law.
```
theorem switchParameterLaw_success [MeasurableMul₂ G] [MeasurableInv G]
    (σ : ℕ → Measure G) [∀ j, IsProbabilityMeasure (σ j)]
    (S : ℕ → Set G) (hS : ∀ j, MeasurableSet (S j)) (n k : ℕ) (x : G) :
    switchParameterLaw σ n k {p | SwitchSuccessful S n k x p} =
      survivingSwitchProbability σ S n k x := by
…
```
Mentions: OAI.PolycyclicRecognition.switchParameterLaw, OAI.PolycyclicRecognition.SwitchSuccessful, OAI.PolycyclicRecognition.survivingSwitchProbability