OAI/NumberTheory/DukePrimeDegree/Entropy/SubexponentialCoverAlphabet.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DukePrimeDegree.coverAlphabet line 14
2. lemma OAI.DukePrimeDegree.mem_coverAlphabet line 17
3. lemma OAI.DukePrimeDegree.coverAlphabet_card_le line 25
4. lemma OAI.DukePrimeDegree.coverAlphabet_log_card_le line 47
5. theorem OAI.DukePrimeDegree.ae_coverAlphabet_cost_tendsto_zero line 64

   Source documentation

   Encoding one height-bounded label anywhere in the word costs o(N). The same alphabet covers every time in the window.

   theorem ae_coverAlphabet_cost_tendsto_zero {Y : Type*} [MeasurableSpace Y]
       (μ : Measure Y) [IsFiniteMeasure μ] {T : Y → Y} (hT : MeasurePreserving T μ μ)
       (H Q : Y → ℕ) (hH : Measurable H) (hstep : ∀ x, H (T x) ≤ H x+1)
       (J : ℕ → ℕ) {K C : ℝ} (hK : 0 < K) (hC : 0 ≤ C)
       (hJ : ∀ m, (J m:ℝ) ≤ K*Real.exp (C*(m:ℝ)))
       (hcode : ∀ m, Q '' {x | H x=m} ⊆ (Nat.pair m) '' Set.Iio (J m)) :
       ∀ᵐ x ∂μ,
         (∀ N k, k ≤ N → Q (T^[k] x) ∈ coverAlphabet J (windowHeight T H N x)) ∧
         Tendsto (fun N : ℕ => Real.log (coverAlphabet J (windowHeight T H N x)).card / N)
           atTop (𝓝 0) := by
   …

   Mentions: OAI.DukePrimeDegree.coverAlphabet, OAI.DukePrimeDegree.windowHeight