InitialSampledProductWindow.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The retained logarithmic window gives both Poisson cutoffs

theorem OAI.Ostmann.sampled_product_window_of_log_error line 9
theorem OAI.Ostmann.sampled_product_poisson_cutoff line 27

theorem OAI.Ostmann.initial_doubled_product_window line 40

Source documentation

The cutoff weights restrict the sampled product without changing any marginal prior. The only extra loss is the already bounded cell rounding.

theorem initial_doubled_product_window (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (b d r : ℕ) (μ₀ : P → ℝ) (μb : Fin b → P → ℝ)
    (μd : Fin d → P → ℝ) (μc : Fin r → P → ℝ) (G cb cd : ℝ) (center : Fin r → ℝ)
    (hG : ∀ q : P, μ₀ q ≠ 0 → |Real.log (q : ℝ) - G| ≤ 1)
    (hc : ∀ i (q : P), μc i q ≠ 0 → |Real.log (q : ℝ) - center i| ≤ 1)
    (X Δ E : ℝ) (hX : 0 < X)
    (htarget : |2 * (G + cb + cd + ∑ i, center i) - (Real.log X + Δ)| ≤ E)
    (x : Fin (((b + (d + r)) + 1) + ((b + (d + r)) + 1)) → P)
    (hprior : productPrior (Fin.append
      (Fin.cons μ₀ (Fin.append μb (Fin.append μd μc)))
      (Fin.cons μ₀ (Fin.append μb (Fin.append μd μc)))) x ≠ 0)
    (hw : doubledHalfWeight (fun y : Fin ((b + (d + r)) + 1) → P =>
…

Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.doubledHalfWeight