SampledHistoryRate.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Original-prior squared-history rate from integer reversals

theorem OAI.Ostmann.adaptivePivotData_history_frequencies line 13

theorem OAI.Ostmann.sampled_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 sampled_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),
      (∀ 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,
      (∀ t i, (D t).frequencies i = singleTreeNodeFrequencies S n t i.val) →
      ∀ T : TreeLeafIndex n → Finset ℕ, ∀ h J : TreeLeafIndex n → ℕ,
…

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