SingletonFamily.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Sum the reciprocal savings of fixed singleton relation records.

theorem OAI.TwoPointCorrelations.singleton_family_bound line 17

Source documentation

The nonzero tests stay in every system event, so the estimate remains valid for all resampled prime assignments.

theorem singleton_family_bound (system : I → OrderedPrimeSystem ι) (K : ℕ)
    (hsize : ∀ i, K ≤ (system i).size)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hV : 1 ≤ primeHarmonicMass P)
    (H N : ℕ) (hH : 0 < H) (hN : 1 ≤ N)
    (hlo : ∀ p ∈ P, H ≤ p) (hhi : ∀ p ∈ P, p ≤ N)
    (hdelta : (H : ℝ)⁻¹ + (1 + Real.log N) / H ≤ 1)
    (weight : I → ℝ) (hw : ∀ i, 0 ≤ weight i) :
    (∑ i, weight i * ∑ x : ι → P,
      if (system i).Holds (integerPrimeAssignment Subtype.val x)
        then ∏ z, ((x z).val : ℝ)⁻¹ else 0) ≤
      (∑ i, weight i) * primeHarmonicMass P ^ Fintype.card ι *
        ((H : ℝ)⁻¹ + (1 + Real.log N) / H) ^ K := by
…

Mentions: OAI.TwoPointCorrelations.OrderedPrimeSystem, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.integerPrimeAssignment

theorem OAI.TwoPointCorrelations.outer_singleton_family_bound line 41

Source documentation

Outside numerical data is averaged separately from the finite combinatorial record, preserving the unrestricted reciprocal mass.

theorem outer_singleton_family_bound
    (Ξ : I → Type*) [∀ i, Fintype (Ξ i)]
    (system : ∀ i, Ξ i → OrderedPrimeSystem ι) (K : ℕ)
    (hsize : ∀ i x, K ≤ (system i x).size)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hV : 1 ≤ primeHarmonicMass P)
    (H N : ℕ) (hH : 0 < H) (hN : 1 ≤ N)
    (hlo : ∀ p ∈ P, H ≤ p) (hhi : ∀ p ∈ P, p ≤ N)
    (hdelta : (H : ℝ)⁻¹ + (1 + Real.log N) / H ≤ 1)
    (outerWeight : ∀ i, Ξ i → ℝ) (hout : ∀ i x, 0 ≤ outerWeight i x)
    (outerMass : ℝ) (hmass : ∀ i, ∑ x, outerWeight i x ≤ outerMass)
    (weight : I → ℝ) (hw : ∀ i, 0 ≤ weight i) :
    (∑ i, weight i * ∑ x, outerWeight i x * ∑ y : ι → P,
…

Mentions: OAI.TwoPointCorrelations.OrderedPrimeSystem, OAI.TwoPointCorrelations.primeHarmonicMass

theorem OAI.TwoPointCorrelations.singleton_record_weight_bound line 71

Source documentation

The exact finite code count bounds the total nonnegative record weight.

theorem singleton_record_weight_bound (R N D : ℕ)
    (encode : I → CrudeWordCode R N D) (hinj : Function.Injective encode)
    (weight : I → ℝ) (W : ℝ) (hW : 0 ≤ W) (hw : ∀ i, weight i ≤ W) :
    (∑ i, weight i) ≤ (Fintype.card (CrudeWordCode R N D) : ℝ) * W := by
…

Mentions: OAI.TwoPointCorrelations.CrudeWordCode