OAI/Probability/GammaPassage/RecordScales.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.CrossingBridge.exists_strict_record_after line 16

   Source documentation

   A positive null sequence has a strict record minimum after every index.

   theorem exists_strict_record_after (a : ℕ → ℝ) (hpos : ∀ k, 0 < a k)
       (hlim : Tendsto a atTop (𝓝 0)) (N : ℕ) :
       ∃ k, N < k ∧ ∀ i < k, a k < a i := by
   …

2. theorem OAI.GammaFPP.CrossingBridge.infinite_strict_records line 32
3. theorem OAI.GammaFPP.CrossingBridge.normalized_lengths_tendsto line 41

   Source documentation

   Normalizing the characteristic lengths by 16^k makes them a null sequence.

   theorem normalized_lengths_tendsto (L : ℕ → ℝ)
       (hpos : ∀ k, 0 < L k) (hbound : ∀ k, L k ≤ (2 : ℝ) ^ (3 * k)) :
       Tendsto (fun k => L k * (1 / 16 : ℝ) ^ k) atTop (𝓝 0) := by
   …

4. theorem OAI.GammaFPP.CrossingBridge.record_scales line 57

   Source documentation

   Record-scale comparison in denominator-free form: L_k ≤ 16^(k-i) L_i for every previous index i.

   theorem record_scales (L : ℕ → ℝ) (hpos : ∀ k, 0 < L k)
       (hbound : ∀ k, L k ≤ (2 : ℝ) ^ (3 * k)) :
       ∀ N, ∃ k, N < k ∧ ∀ i ≤ k, L k ≤ (16 : ℝ) ^ (k - i) * L i := by
   …

5. theorem OAI.GammaFPP.CrossingBridge.record_scales_from line 86

   Source documentation

   Record-scale comparison from an initial index k₀, using k-j and requiring no bound below k₀.

   theorem record_scales_from (L : ℕ → ℝ) (k₀ : ℕ)
       (hpos : ∀ k, k₀ ≤ k → 0 < L k)
       (hbound : ∀ k, k₀ ≤ k → L k ≤ (2 : ℝ) ^ (3 * k)) :
       ∀ N, ∃ k, N < k ∧ k₀ ≤ k ∧
         ∀ j, j ≤ k - k₀ → (1 / 16 : ℝ) ^ j * L k ≤ L (k - j) := by
   …