OAI/NumberTheory/Ostmann/Arithmetic/MatchedPriorCorrelation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.counterpartRoleUnary line 12
2. theorem OAI.Ostmann.counterpartRoleUnary_norm line 16
3. theorem OAI.Ostmann.counterpartRole_finiteEdgeWeight line 25
4. theorem OAI.Ostmann.matched_harmonic_correlation_eq line 39

   Source documentation

   This equality factors out the harmonic normalizer and the reciprocal product scale before any external integer is summed.

   theorem matched_harmonic_correlation_eq {n : ℕ} (P : Finset ℕ)
       (Q : Fin n → Finset ℕ) (e : Equiv.Perm (Fin n))
       (μ : (Fin n → P) → ℝ) (G : (Fin n → P) → ℂ)
       (X : ℝ) (hX : X ≠ 0) :
       (∑ x, (μ x : ℂ) *
         (productPrior (fun i => primeSubsetPrior P (Q i)) (fun i => x (e i)) : ℂ) * G x) =
         (((∏ i, (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹) * X⁻¹ : ℝ) : ℂ) *
           ∑ x, (μ x : ℂ) * ((X / (∏ i, (x i : ℝ)) : ℝ) : ℂ) *
             ((∏ i, counterpartRoleFactor P Q e i (x i) : ℝ) : ℂ) * G x := by
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.counterpartRoleFactor

5. theorem OAI.Ostmann.matched_harmonic_correlation_bound line 63

   Source documentation

   The actual two-prior correlation has the already-extracted small factor. Its hypothesis is the normalized ratio bound supplied by FullPrimeRatioPair.

   theorem matched_harmonic_correlation_bound {n : ℕ} (P : Finset ℕ)
       (Q : Fin n → Finset ℕ) (e : Equiv.Perm (Fin n))
       (μ : (Fin n → P) → ℝ) (G : (Fin n → P) → ℂ)
       (X δ : ℝ) (hX : 0 < X)
       (hbound : ‖∑ x, (μ x : ℂ) * ((X / (∏ i, (x i : ℝ)) : ℝ) : ℂ) *
         ((∏ i, counterpartRoleFactor P Q e i (x i) : ℝ) : ℂ) * G x‖ ≤ δ) :
       ‖∑ x, (μ x : ℂ) *
         (productPrior (fun i => primeSubsetPrior P (Q i)) (fun i => x (e i)) : ℂ) * G x‖ ≤
         (∏ i, (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹) * X⁻¹ * δ := by
   …

   Mentions: OAI.Ostmann.counterpartRoleFactor, OAI.Ostmann.productPrior, OAI.Ostmann.primeSubsetPrior