MovingPatternGiantBounds.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Concrete logarithmic bounds for the original giant comparison

theorem OAI.Ostmann.giantProgressionCutoff_log_le line 13
theorem OAI.Ostmann.naturalProduct_exp_bound line 24
theorem OAI.Ostmann.naturalProduct_log_bound line 36

theorem OAI.Ostmann.naturalProduct_giant_log_range line 51

Source documentation

A list containing linearly many primes in the actual nongiant range satisfies the logarithmic budget used by the giant progression theorem.

theorem naturalProduct_giant_log_range (K : ℝ) (hK : 0 ≤ K) :
    ∀ᶠ L : ℝ in atTop, ∀ (σ : Type) (value : σ → ℕ) (slots : List σ),
      (∀ i, value i ≠ 0) → (slots.length : ℝ) ≤ K * L →
      (∀ i, (value i : ℝ) ≤ Real.exp (Real.exp ((11 / 1000 : ℝ) * L))) →
      Real.log (MovingSlotReversal.naturalProduct value slots : ℝ) ≤
        Real.exp ((12 / 1000 : ℝ) * L) := by
…

Mentions: OAI.Ostmann.MovingSlotReversal.naturalProduct

theorem OAI.Ostmann.movingPattern_regular_giant_log_range line 67
Source documentation
The common regular product of both histories uses only the original small and bulk leaves. Its logarithmic budget follows from their lengths.
```
theorem movingPattern_regular_giant_log_range (n r₀ k : ℕ) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…
```
Mentions: OAI.Ostmann.spectatorBulkCount

theorem OAI.Ostmann.frequencyModelModulus_exp_bound line 102

Source documentation

The frequency modulus used by the actual pair of histories has a fixed polynomial degree in the frequency cutoff.

theorem frequencyModelModulus_exp_bound (S : Finset ℤ) (N n : ℕ)
    (t : FrequencyTree (S × S) n) (A : ℝ)
    (hN : ∀ s ∈ S, s.natAbs ≤ N) (hA : (N : ℝ) ≤ Real.exp A) :
    ((frequencyModelBase S n t ^ (n - 1 + 2) : ℕ) : ℝ) ≤
      Real.exp ((2 * (2 ^ (n + 1) - 1) * (n - 1 + 2) : ℕ) * A) := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.frequencyModelBase

theorem OAI.Ostmann.movingPattern_actual_modulus_range line 116
Source documentation
The paired frequency modulus, the actual internal prime image, and the selected spectators all fit the giant cutoff at the manuscript scales.
```
theorem movingPattern_actual_modulus_range (n k : ℕ) (Cfreq : ℝ) (hCfreq : 0 ≤ Cfreq) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…
```
Mentions: OAI.Ostmann.spectatorBulkCount