OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceSectionTileVolume.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.sequence_subexponential_exp_error line 14
2. theorem OAI.PolycyclicRecognition.sequence_section_tile_volume_exponent line 34

   Source documentation

   Arbitrary translations of the quotient do not alter its Haar multiplier. The ideal and quotient constraints give the exact P-minus-trace exponent.

   theorem sequence_section_tile_volume_exponent
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       (E : ℕ → Set N) (T : ℕ → Set Q) (B : ℕ → Set π.ker)
       (q₀ : ℕ → Q) (α : ℕ → Q ≃ Q)
       (P ell : ℝ) (ε U V : ℕ → ℝ)
       (hε : Tendsto ε atTop (𝓝 0))
       (hU : HasSubexponentialUpperBoundSeq scale U)
       (hV : HasSubexponentialUpperBoundSeq scale V)
       (hU0 : ∀ n, 0 ≤ U n) (hV0 : ∀ n, 0 ≤ V n)
       (hT : ∀ n, μQ (T n) ≠ ⊤) (hB : ∀ n, μI (B n) ≠ ⊤)
       (hα : ∀ n, μQ (α n '' T n) =
         ENNReal.ofReal (Real.exp (-ell * scale n + ε n * scale n)) * μQ (T n))
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq

3. theorem OAI.PolycyclicRecognition.sequence_section_tile_family_volume_exponent line 86

   Source documentation

   All tiles share one subexponential loss even though their quotient translations and automorphisms vary independently. This also proves the finiteness needed by the separated-cell packing inequality.

   theorem sequence_section_tile_family_volume_exponent
       (scale : ℕ → ℝ) (hscale : Tendsto scale atTop atTop)
       {J : ℕ → Type*} (E : ∀ n, J n → Set N) (T : ℕ → Set Q) (B : ℕ → Set π.ker)
       (q₀ : ∀ n, J n → Q) (α : ∀ n, J n → Q ≃ Q)
       (P ell : ℝ) (ε U V : ℕ → ℝ)
       (hε : Tendsto ε atTop (𝓝 0))
       (hU : HasSubexponentialUpperBoundSeq scale U)
       (hV : HasSubexponentialUpperBoundSeq scale V)
       (hU0 : ∀ n, 0 ≤ U n) (hV0 : ∀ n, 0 ≤ V n)
       (hT : ∀ n, μQ (T n) ≠ ⊤) (hB : ∀ n, μI (B n) ≠ ⊤)
       (hα : ∀ n j, μQ (α n j '' T n) ≤
         ENNReal.ofReal (Real.exp (-ell * scale n + ε n * scale n)) * μQ (T n))
   …

   Mentions: OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq