OAI/GroupTheory/PolycyclicRecognition/Geometry/RootIntervalSampling.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.rootIntervalDirection line 16

   Source documentation

   Extend a fixed finite word by zero directions for the unused indices.

   def rootIntervalDirection {m : ℕ} (letters : Fin m → I) (X : I → L)
       (s : I → ℝ) (r : ℝ) (j : ℕ) : L :=
   …

2. def OAI.PolycyclicRecognition.rootIntervalSample line 20
3. theorem OAI.PolycyclicRecognition.rootIntervalSample_letter line 25
4. theorem OAI.PolycyclicRecognition.rootIntervalSample_sub line 33

   Source documentation

   Two independent interval samples differ by the single intended root increment. There is no need to retain a profile at their intermediate product.

   theorem rootIntervalSample_sub (Exp : L → N)
       (hneg : ∀ v, Exp (-v) = (Exp v)⁻¹)
       (hadd : ∀ (v : L) (u t : ℝ), Exp ((u + t) • v) = Exp (u • v) * Exp (t • v))
       {m : ℕ} (letters : Fin m → I) (X : I → L) (s : I → ℝ) (r : ℝ) (j : ℕ) (u t : ℝ) :
       rootIntervalSample Exp letters X s r j u * (rootIntervalSample Exp letters X s r j t)⁻¹ =
         rootIntervalSample Exp letters X s r j (u - t) := by
   …

   Mentions: OAI.PolycyclicRecognition.rootIntervalSample

5. def OAI.PolycyclicRecognition.rootIntervalLaw line 44
6. theorem OAI.PolycyclicRecognition.measurePreserving_rootIntervalSample line 50

   Source documentation

   These are pushforward laws of the original independent uniform samples.

   theorem measurePreserving_rootIntervalSample [TopologicalSpace N] [BorelSpace N]
       (Exp : L → N)
       (hcont : ∀ v : L, Continuous (fun t : ℝ => Exp (t • v)))
       {m : ℕ} (letters : Fin m → I) (X : I → L) (s : I → ℝ) (r R : ℝ)
       (j : ℕ) :
       MeasurePreserving (rootIntervalSample Exp letters X s r j) (uniformIntervalLaw R)
         (rootIntervalLaw Exp letters X s r R j) := by
   …

   Mentions: OAI.PolycyclicRecognition.rootIntervalSample, OAI.PolycyclicRecognition.uniformIntervalLaw, OAI.PolycyclicRecognition.rootIntervalLaw

7. theorem OAI.PolycyclicRecognition.rootIntervalLaw_isProbability line 60