OAI/NumberTheory/Ostmann/Arithmetic/CompensatedHistoryRate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.compensatedAdaptiveData_history_frequencies line 13
2. theorem OAI.Ostmann.compensated_history_square_rate line 31

   Source documentation

   This is the squared-history estimate with actual prime sampling and actual integer integrality/unit conditions. The adaptive-support event is constructed, and is not an additional hypothesis.

   theorem compensated_history_square_rate (n k : ℕ) (K C ε : ℝ) (hC : 0 ≤ C) (hε : 0 < ε) :
       ∀ᶠ m : ℝ in atTop, ∀ N V : ℕ, ∀ Δ : ℝ, ∀ P : Finset ℕ, ∀ S : Finset ℤ,
         (N : ℝ) ≤ Real.exp (C * m) →
         (V : ℝ) ≤ Real.exp (Δ + Real.sqrt m) →
         (∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N) →
         ∀ R : FrequencyTree S n → ℕ, ∀ [_hQ : ∀ t, NeZero (R t ^ (k + 2))],
         ∀ D : FrequencyTree S n → PivotDependencyScheme (2 ^ n - 1),
         ∀ U : FrequencyTree S n → Fin (2 ^ n - 1) → ℤ,
         (∀ t i, IsCoprime (U t i) (R t : ℤ)) →
         (∀ t i, (D t).depth i ≤ k) →
         ∀ _hs : ∀ t i, ((D t).frequencies i).root ≠ 0,
         ∀ _hsR : ∀ t i, ((D t).frequencies i).root.natAbs ∣ R t,
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.PivotDependencyScheme