OAI/NumberTheory/Ostmann/Arithmetic/GlobalHistoryPairBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.historyPairBound line 13
2. theorem OAI.Ostmann.selected_global_history_pair_bound line 21
3. theorem OAI.Ostmann.global_history_pair_original_bound line 86

   Source documentation

   This is the full original-prior correlation estimate for the two constructed coefficients. Its only remaining loss is the displayed numerical bound, which is independent of the other sampled labels.

   theorem global_history_pair_original_bound {V : Type*} [Fintype V]
       (a b : V) (hab : a ≠ b) (D D' : HistoryCoefficientData V)
       (frequencies : List ℤ) (C : ℕ) (hC : 1 ≤ C)
       (hfreq : ∀ s ∈ frequencies, s ≠ 0)
       (hsteps : ∀ step ∈ D.steps, step.s ∈ frequencies)
       (hsteps' : ∀ step ∈ D'.steps, step.s ∈ frequencies)
       (hsize : ∀ step ∈ D.steps, step.left.length + step.right.length + 4 ≤ C)
       (hsize' : ∀ step ∈ D'.steps, step.left.length + step.right.length + 4 ≤ C)
       (hunits : ∀ i, (D.units i : ℤ) ∣ (historyFrequencyBase frequencies : ℤ))
       (hunits' : ∀ i, (D'.units i : ℤ) ∣ (historyFrequencyBase frequencies : ℤ))
       (χ : V → ∀ p : ℕ, DirichletCharacter ℂ p) (graph : V → V → ℤ)
       (unary : V → ℕ → ℂ) (hunary : ∀ i x, ‖unary i x‖ ≤ 1)
   …

   Mentions: OAI.Ostmann.HistoryCoefficientData, OAI.Ostmann.historyFrequencyBase