OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceRescaledImageVolume.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.rescaled_image_volume_lower_sequence line 22

   Source documentation

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

   theorem rescaled_image_volume_lower_sequence
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (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 : HasSubexponentialLowerBoundSeq scale (fun n => (volume (C n)).toReal)) :
       HasSubexponentialLowerBoundSeq scale (fun n =>
         ((Measure.map ((Exp ∘ e) ∘ b₀.equivFun.symm) volume)
           ((((Exp ∘ e) ∘ (exponentialRescaleBasis (WordBasisSelections.basis X words β)
   …

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