OAI/GroupTheory/PolycyclicRecognition/Algebra/SwitchParameterPullback.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.mapSwitchParameters line 14

   Source documentation

   Apply the prescribed sampling map in each of the two independent slots.

   def mapSwitchParameters {A B : Type*} (f : ℕ → A → B) :
       (n k : ℕ) → SwitchParameters A k → SwitchParameters B k
     | _, 0, _ => PUnit.unit
     | n, k + 1, p => (f n p.1, f n p.2.1, mapSwitchParameters f (n + 1) k p.2.2)

   Mentions: OAI.PolycyclicRecognition.SwitchParameters

2. theorem OAI.PolycyclicRecognition.measurePreserving_mapSwitchParameters line 19
3. theorem OAI.PolycyclicRecognition.pullback_switch_event line 34

   Source documentation

   The successful probability is unchanged by returning to the independent samples that defined the increment laws.

   theorem pullback_switch_event {A G : Type*} [MeasurableSpace A]
       [Group G] [MeasurableSpace G]
       (f : ℕ → A → G) (τ : ℕ → Measure A) (σ : ℕ → Measure G)
       [∀ j, IsProbabilityMeasure (τ j)] [∀ j, IsProbabilityMeasure (σ j)]
       (hf : ∀ j, MeasurePreserving (f j) (τ j) (σ j))
       (n k : ℕ) (E : Set (SwitchParameters G k)) (hE : MeasurableSet E) :
       MeasurableSet (mapSwitchParameters f n k ⁻¹' E) ∧
         switchParameterLaw τ n k (mapSwitchParameters f n k ⁻¹' E) =
           switchParameterLaw σ n k E := by
   …

   Mentions: OAI.PolycyclicRecognition.SwitchParameters, OAI.PolycyclicRecognition.mapSwitchParameters, OAI.PolycyclicRecognition.switchParameterLaw