OAI/NumberTheory/TwoPoint/Bounds/CenterBandReindex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoPointCorrelations.centerBand_nonraw_expansion line 13
2. lemma OAI.TwoPointCorrelations.primeIndicator_union line 33
3. theorem OAI.TwoPointCorrelations.partialCenterBand_expansion line 48

   Source documentation

   Only the selected center band is centered. The untouched core factors combine with the retained center factors into the exact divisor D\W.

   theorem partialCenterBand_expansion (D T : Finset ℕ)
       (hD : ∀ p ∈ D, Nat.Prime p) (θ : ℂ) (n : ℕ) :
       natDivisibilityIndicator (∏ p ∈ D \ T, p) n *
           (∏ p ∈ D ∩ T, (natDivisibilityIndicator p n - θ / (p : ℂ))) =
         ∑ W ∈ (D ∩ T).powerset,
           ((-θ) ^ W.card / ((∏ p ∈ W, p : ℕ) : ℂ)) *
             natDivisibilityIndicator (∏ p ∈ D \ W, p) n := by
   …

   Mentions: OAI.TwoPointCorrelations.natDivisibilityIndicator

4. theorem OAI.TwoPointCorrelations.partialCenterBand_nonraw_expansion line 83
5. lemma OAI.TwoPointCorrelations.powerset_inter_filter line 104
6. lemma OAI.TwoPointCorrelations.sum_powerset_retained line 115
7. theorem OAI.TwoPointCorrelations.centerBand_reindex line 147

   Source documentation

   The removed-prime choice can be made first; the retained subset then runs through the complementary pool. No cardinal multiplicity is added.

   theorem centerBand_reindex (S T : Finset ℕ) (hT : T ⊆ S)
       (F : Finset ℕ → Finset ℕ → ℂ) :
       (∑ D ∈ S.powerset, ∑ W ∈ (D ∩ T).powerset, F (D \ W) W) =
         ∑ W ∈ T.powerset, ∑ U ∈ (S \ W).powerset, F U W := by
   …

8. lemma OAI.TwoPointCorrelations.powerset_sdiff_filter line 165
9. theorem OAI.TwoPointCorrelations.centerBand_reindex_retained line 178

   Source documentation

   The retained-prime product is the outer summation variable used in the analytic transfer. Removed and retained primes are disjoint exactly.

   theorem centerBand_reindex_retained (S T : Finset ℕ) (hT : T ⊆ S)
       (F : Finset ℕ → Finset ℕ → ℂ) :
       (∑ D ∈ S.powerset, ∑ W ∈ (D ∩ T).powerset, F (D \ W) W) =
         ∑ U ∈ S.powerset, ∑ W ∈ (T \ U).powerset, F U W := by
   …