OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandIdentity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.mrt_band_complement line 14
2. lemma OAI.TwoPointCorrelations.mrt_band_complement_disjoint line 43
3. theorem OAI.TwoPointCorrelations.mrt_band_complement_product line 52
4. theorem OAI.TwoPointCorrelations.mrt_euler_inclusion_exclusion line 66

   Source documentation

   The alternating masked Euler products factor exactly into one unrestricted complement and one nonempty factor for each band.

   theorem mrt_euler_inclusion_exclusion {ι κ : Type*} [DecidableEq ι] [DecidableEq κ]
       (S : Finset ι) (J : Finset κ)
       (P : κ → Finset ι) (a : ι → ℂ)
       (hsub : ∀ j ∈ J, P j ⊆ S) (hdis : Set.PairwiseDisjoint (J : Set κ) P) :
       (∑ I ∈ J.powerset, (-1 : ℂ) ^ I.card * ∏ p ∈ S \ I.biUnion P, a p) =
         (∏ p ∈ S \ J.biUnion P, a p) *
           ∏ j ∈ J, ((∏ p ∈ P j, a p) - 1) := by
   …