OAI/GroupTheory/PolycyclicRecognition/Analysis/SampledSuccessfulVolume.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.sampledSwitchParameters line 14
2. theorem OAI.PolycyclicRecognition.measurePreserving_sampledSwitchParameters line 18
3. theorem OAI.PolycyclicRecognition.exists_sampled_success_volume line 28

   Source documentation

   The compact cube is fixed before restricting to successful parameters.

   theorem exists_sampled_success_volume {G : Type*} [Group G] [MeasurableSpace G]
       {R : ℝ} (hR : 0 < R) (m : ℕ)
       (f : ℝ → ℕ → ℝ → G) (σ : ℝ → ℕ → Measure G)
       [∀ r j, IsProbabilityMeasure (σ r j)]
       (hf : ∀ r j, MeasurePreserving (f r j) (uniformIntervalLaw R) (σ r j))
       (x : ℝ → G) (A : ℝ → Set G) (E : ℝ → Set (SwitchParameters G m))
       (hE : ∀ r, MeasurableSet (E r))
       (hprob : HasSubexponentialLowerBound (fun r => (switchParameterLaw (σ r) 0 m (E r)).toReal))
       (hsuccess : ∀ r p, p ∈ E r → SwitchSuccessful (fun _ => A r) 0 m (x r) p) :
       ∃ F : ℝ → Set (Fin (m + m) → ℝ),
         (∀ r, MeasurableSet (F r)) ∧ (∀ r, F r ⊆ closedBall 0 R) ∧
         HasSubexponentialLowerBound (fun r => (volume (F r)).toReal) ∧
   …

   Mentions: OAI.PolycyclicRecognition.uniformIntervalLaw, OAI.PolycyclicRecognition.SwitchParameters, OAI.PolycyclicRecognition.HasSubexponentialLowerBound, OAI.PolycyclicRecognition.switchParameterLaw, OAI.PolycyclicRecognition.SwitchSuccessful