OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteSwitchEvents.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Successful switch events only use the prescribed finite list of sheets

  1. theorem OAI.PolycyclicRecognition.switchSuccessful_mono line 16
  2. theorem OAI.PolycyclicRecognition.switchSuccessful_congr line 27
  3. theorem OAI.PolycyclicRecognition.survivingSwitchProbability_congr line 39
  4. theorem OAI.PolycyclicRecognition.switchParameterLaw_success_finite line 56

    Source documentation

    No measurability conditions on unused sheets are needed.

    theorem switchParameterLaw_success_finite [MeasurableMul₂ G] [MeasurableInv G]
    (σ : ℕ → Measure G) [∀ j, IsProbabilityMeasure (σ j)]
    (S : ℕ → Set G) (n k : ℕ)
    (hS : ∀ j, n < j → j ≤ n + k → MeasurableSet (S j)) (x : G) :
    MeasurableSet {p : SwitchParameters G k | SwitchSuccessful S n k x p} ∧
      switchParameterLaw σ n k {p | SwitchSuccessful S n k x p} =
        survivingSwitchProbability σ S n k x := by
…

    Mentions: OAI.PolycyclicRecognition.SwitchParameters, OAI.PolycyclicRecognition.SwitchSuccessful, OAI.PolycyclicRecognition.switchParameterLaw, OAI.PolycyclicRecognition.survivingSwitchProbability