OAI/NumberTheory/Ostmann/Construction/WordProductWindow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.wordCopy_log_product line 12
2. theorem OAI.Ostmann.harmonic_word_log_error line 28
3. theorem OAI.Ostmann.word_event_log_product line 42

   Source documentation

   Both sampled word copies have the selected bin. Both cell copies retain exactly their original supports; the full formal product has bounded log error.

   theorem word_event_log_product (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       {B : Type*} {k m : ℕ} (Q : Fin k → Finset ℕ) (R : Fin m → Finset ℕ)
       (bin : (Fin k → P) → B) (b : B) (J W : ℝ) (T e : Fin m → ℝ)
       (hbin : ∀ w, productPrior (fun i => primeSubsetPrior P (Q i)) w ≠ 0 →
         bin w = b → |(∑ i, Real.log (w i : ℝ)) - J| ≤ W)
       (hcells : ∀ i p, p ∈ R i → |Real.log (p : ℝ) - T i| ≤ e i)
       (x : Fin ((k + m) + (k + m)) → P)
       (hx : x ∈ wordCharacterEvent (fun i => primeSubsetPrior P (Q i))
         (fun j => primeSubsetPrior P (R j)) bin b) :
       |Real.log (∏ i, (x i : ℝ)) - (2 * J + 2 * ∑ i, T i)| ≤
         2 * W + 2 * ∑ i, e i := by
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.wordCharacterEvent

4. theorem OAI.Ostmann.product_window_of_log_error line 80
5. theorem OAI.Ostmann.wordLogBin_log_error line 91

   Source documentation

   The clipped finite bin has the ordinary floor error on its valid support.

   theorem wordLogBin_log_error {m : ℕ} (τ : ℝ) (ℓ : Fin (m + 1) → ℝ)
       (hlo : 0 ≤ ∑ i, ℓ i) (hhi : (∑ i, ℓ i) ≤ 4 * τ) :
       |(∑ i, ℓ i) - (wordLogBin τ ℓ).val| ≤ 1 := by
   …

   Mentions: OAI.Ostmann.wordLogBin

6. theorem OAI.Ostmann.word_event_product_window line 100