OAI/NumberTheory/Ostmann/Construction/FiniteMatchedPrior.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.finite_enumeration_sum line 11
2. theorem OAI.Ostmann.finite_matched_harmonic_prior line 17
3. theorem OAI.Ostmann.finite_matched_harmonic_correlation_eq line 37

   Source documentation

   This keeps the reciprocal product scale outside the normalized pair correlation, before any sum over integer pivots.

   theorem finite_matched_harmonic_correlation_eq {H : Type*} [Fintype H]
       (P : Finset ℕ) (Q : H → Finset ℕ) (e : Equiv.Perm H)
       (μ : (H → P) → ℝ) (G : (H → P) → ℂ) (X : ℝ) (hX : X ≠ 0) :
       (∑ x, (μ x : ℂ) * (∏ i, primeSubsetPrior P (Q i) (x (e i)) : ℝ) * G x) =
         (((∏ i, (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹) * X⁻¹ : ℝ) : ℂ) *
           ∑ x, (μ x : ℂ) * ((X / (∏ i, (x i : ℝ)) : ℝ) : ℂ) *
             ((∏ i, if (x i : ℕ) ∈ Q (e.symm i) then (1 : ℝ) else 0) : ℂ) * G x := by
   …

   Mentions: OAI.Ostmann.primeSubsetPrior

4. theorem OAI.Ostmann.finite_matched_harmonic_correlation_bound line 58