OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandProducts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.mrt_euler_block_bound line 13
2. theorem OAI.TwoPointCorrelations.mrt_band_product_bound line 28
3. theorem OAI.TwoPointCorrelations.mrt_partitioned_euler_bound line 62

   Source documentation

   The complement and all disjoint bands partition the original finite Euler product, so the cost contains each prime exactly once.

   theorem mrt_partitioned_euler_bound {ι κ : Type*} [DecidableEq ι] [DecidableEq κ]
       (S : Finset ι) (J : Finset κ)
       (P : κ → Finset ι) (z : ι → ℂ)
       (hsub : ∀ j ∈ J, P j ⊆ S) (hdis : Set.PairwiseDisjoint (J : Set κ) P)
       (hz : ∀ i ∈ S, ‖z i‖ ≤ 1 / 2) :
       ‖(∏ i ∈ S \ J.biUnion P, (1 - z i)⁻¹) *
           ∏ j ∈ J, ((∏ i ∈ P j, (1 - z i)⁻¹) - 1)‖ ≤
         Real.sqrt ‖∏ i ∈ S, (1 - z i)⁻¹‖ *
           Real.exp ((∑ i ∈ S, (‖z i‖ + ‖z i‖ ^ 2)) / 2) := by
   …