OAI/Analysis/FiniteFactor/Sampling/ProductError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sampling_product_error line 12

   Source documentation

   Telescoping products needs upper bounds only. In particular, a zero ideal coordinate moment causes no division or exceptional case.

   theorem sampling_product_error {ι : Type*} (S : Finset ι) (f g : ι → ℝ) (M ε : ℝ)
       (hM : 1 ≤ M) (hε : 0 ≤ ε)
       (hf : ∀ i ∈ S, 0 ≤ f i ∧ f i ≤ M) (hg : ∀ i ∈ S, 0 ≤ g i ∧ g i ≤ M)
       (he : ∀ i ∈ S, |f i-g i| ≤ ε) :
       |(∏ i ∈ S, f i)-(∏ i ∈ S, g i)| ≤ (S.card : ℝ)*ε*M^S.card := by
   …