OAI/GroupTheory/PolycyclicRecognition/Algebra/CoupledBundleStates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.innerContinuousMulEquiv line 17
2. theorem OAI.PolycyclicRecognition.innerContinuousMulEquiv_apply line 24
3. theorem OAI.PolycyclicRecognition.measurePreserving_innerContinuousMulEquiv line 29
4. def OAI.PolycyclicRecognition.bundleConjugator line 35
5. theorem OAI.PolycyclicRecognition.bundleConjugator_apply line 39
6. theorem OAI.PolycyclicRecognition.bundleConjugator_mem line 47
7. theorem OAI.PolycyclicRecognition.coupledRootIntervalSample_bundle line 57
8. theorem OAI.PolycyclicRecognition.good_coupled_source_bundle_image line 81

   Source documentation

   The second-sheet conjugations are the actual inner automorphisms. The joint lower volume is retained when passing to all successive states.

   theorem good_coupled_source_bundle_image {h m : ℕ}
       (lie : L₀ ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EN)) N)
       (Exp : GroupLieAlgebra (𝓘(ℝ, EN)) N → N) (hExp : IsGroupExponential Exp)
       (X : I₀ → L₀) (s : I₀ → ℝ) (letters : Fin m → I₀)
       (scale : ℕ → ℝ) (p : ℝ)
       (μ : Measure N) [SigmaFinite μ] [μ.IsMulLeftInvariant] [μ.IsMulRightInvariant]
       (k : ℕ → Fin h → N) (Good : ℕ → Set N) (x : ℕ → N)
       (hx : ∀ n, x n ∈ Good n) (C : ℕ → Set (Fin h → N))
       (hC : ∀ n, IsCompact (C n))
       (hvol : HasSubexponentialLowerBoundSeq scale (fun n =>
         ((Measure.pi fun _ : Fin h => μ) (C n)).toReal / Real.exp (scale n * p)))
       (ρ : ℝ)
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq