FiniteRelativeProductError.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Relative errors in the finite product of internal-prime averages

theorem OAI.Ostmann.finite_relative_product_error line 13

Source documentation

A common local majorant retains the full product scale in the error.

theorem finite_relative_product_error {ι : Type*} (S : Finset ι)
    (f g : ι → ℂ) (B K : ι → ℝ)
    (hB : ∀ i ∈ S, 0 ≤ B i) (hK : ∀ i ∈ S, 0 ≤ K i)
    (hf : ∀ i ∈ S, ‖f i‖ ≤ B i) (hg : ∀ i ∈ S, ‖g i‖ ≤ B i)
    (hdiff : ∀ i ∈ S, ‖f i - g i‖ ≤ K i * B i) :
    ‖(∏ i ∈ S, f i) - ∏ i ∈ S, g i‖ ≤
      (∑ i ∈ S, K i) * ∏ i ∈ S, B i := by
…