OAI/GroupTheory/PolycyclicRecognition/Analysis/RescaledImageVolume.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.continuous_exponential_basis line 23

   Source documentation

   Continuity is obtained from the supplied intrinsic exponential chart.

   theorem continuous_exponential_basis {n : ℕ}
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G)
       (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
       (b : Basis (Fin n) ℝ L) : Continuous (((Exp ∘ e) ∘ b.equivFun.symm) : (Fin n → ℝ) → G) := by
   …

2. theorem OAI.PolycyclicRecognition.rescaled_image_volume_lower line 42

   Source documentation

   The subexponential logarithmic image loss survives the rescaled exponential chart with exactly the selected word-basis exponent.

   theorem rescaled_image_volume_lower
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G)
       (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
       {I : Type*} (X : I → L) (words : Finset (FreeMagma I))
       (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (β : WordBasisSelections X words)
       (cost : words → ℝ) (C : ℝ → Set (Fin (finrank ℝ L) → ℝ))
       (hlower : HasSubexponentialLowerBound (fun r => (volume (C r)).toReal)) :
       HasSubexponentialLowerBound (fun r =>
         ((Measure.map ((Exp ∘ e) ∘ b₀.equivFun.symm) volume)
           ((((Exp ∘ e) ∘ (exponentialRescaleBasis (WordBasisSelections.basis X words β)
             (fun j => cost (β.val j)) r).equivFun.symm)) '' C r)).toReal /
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.HasSubexponentialLowerBound, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis