NonrawReindex.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact numerical reindexing of all nonraw center-band terms.

lemma OAI.TwoPointCorrelations.primeSubset_product_one_lt_iff line 12

theorem OAI.TwoPointCorrelations.nonraw_prime_reindex line 24

Source documentation

A term is indexed uniquely by its retained integer and removed integer. The original divisor is their product, without multiplicity.

theorem nonraw_prime_reindex (S T : Finset ℕ)
    (hS : ∀ p ∈ S, Nat.Prime p) (hT : T ⊆ S)
    (H τ : ℝ) (θ : ℂ) (G : ℕ → ℕ → ℂ) :
    (∑ D ∈ S.powerset, ∑ W ∈ (D ∩ T).powerset,
      if W.Nonempty ∧ H < ((∏ p ∈ D, p : ℕ) : ℝ) ∧
          ((∏ p ∈ D, p : ℕ) : ℝ) ≤ τ * H
      then ((-θ) ^ W.card / ((∏ p ∈ W, p : ℕ) : ℂ)) *
        G (∏ p ∈ D \ W, p) (∏ p ∈ D, p)
      else 0) =
      ∑ u ∈ retainedPrimeDivisors S, ∑ w ∈ nonrawRoughSupport T H τ u,
        ((-θ) ^ w.primeFactors.card / (w : ℂ)) * G u (u * w) := by
…

Mentions: OAI.TwoPointCorrelations.retainedPrimeDivisors, OAI.TwoPointCorrelations.nonrawRoughSupport

def OAI.TwoPointCorrelations.centerDifference line 67

theorem OAI.TwoPointCorrelations.centerDifference_eq_nonraw_sum line 79

Source documentation

The literal partially centered-minus-raw sum is exactly the numerical u*w expansion, before estimating or using multiplicativity.

theorem centerDifference_eq_nonraw_sum (S T C : Finset ℕ)
    (hS : ∀ p ∈ S, Nat.Prime p) (hT : T ⊆ S) (hCT : Disjoint C T)
    (a : ℕ → ℂ) (A H τ : ℝ) (θ : ℂ) (x : ℕ) (F : ℕ → ℂ) :
    centerDifference S T C a A H τ θ x F =
      ∑ u ∈ retainedPrimeDivisors S, (A : ℂ) ^ (u.primeFactors ∩ C).card *
        ∑ w ∈ nonrawRoughSupport T H τ u,
          ((nonrawRoughData T H τ a θ u).coefficient w / (w : ℂ)) *
            F (u * w) * natDivisibilityIndicator u x := by
…

Mentions: OAI.TwoPointCorrelations.centerDifference, OAI.TwoPointCorrelations.retainedPrimeDivisors, OAI.TwoPointCorrelations.nonrawRoughSupport, OAI.TwoPointCorrelations.nonrawRoughData, OAI.TwoPointCorrelations.natDivisibilityIndicator