CrudeNumericalWordSum.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Complete reciprocal counting for actual numerical tuple and padding words.

lemma OAI.TwoPointCorrelations.split_assignment_reciprocal_sum line 14
lemma OAI.TwoPointCorrelations.primeWordEncoding_weight_sum line 27
theorem OAI.TwoPointCorrelations.primeWordEncoding_weight_le line 46
Source documentation
Both prime supplies may be enlarged, but distinct abstract classes continue to pay distinct reciprocal factors, including after collisions.
```
theorem primeWordEncoding_weight_le (R T : ℕ) (P Q : Finset ℕ) (U : ℝ)
    (hU : 1 ≤ U) (hP : primeHarmonicMass P ≤ U) (hQ : primeHarmonicMass Q ≤ U) :
    (∑ e : PrimeWordEncoding R T P Q, e.weight) ≤
      (∑ n : Fin (T + 1), (Fintype.card (CrudeWordCode R n.val R) : ℝ)) * U ^ T := by
…
```
Mentions: OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.PrimeWordEncoding, OAI.TwoPointCorrelations.CrudeWordCode

theorem OAI.TwoPointCorrelations.numerical_word_reciprocal_sum_le line 65

Source documentation

A bound for the original numerical words, before any equality-pattern or prime assignment is enlarged. This is the crude catalog estimate used by the many-unlit and witness cases.

theorem numerical_word_reciprocal_sum_le (R T : ℕ) (P Q : Finset ℕ)
    (F : Finset (Fin R → SignedStep)) (weight : List SignedStep → ℝ) (W U : ℝ)
    (hW : 0 ≤ W) (hU : 1 ≤ U)
    (hP : primeHarmonicMass P ≤ U) (hQ : primeHarmonicMass Q ≤ U)
    (hweight : ∀ w ∈ F, weight (List.ofFn w) ≤ W)
    (hT : ∀ w ∈ F, Fintype.card (ActualPrimeSlot w) ≤ T)
    (ht : ∀ w ∈ F, ∀ i, Squarefree (w i).tuple)
    (hq : ∀ w ∈ F, ∀ i, Squarefree (w i).padding)
    (htP : ∀ w ∈ F, ∀ i, (w i).tuple.primeFactors ⊆ P)
    (hqQ : ∀ w ∈ F, ∀ i, (w i).padding.primeFactors ⊆ Q)
    (hd : ∀ w ∈ F, ∀ i j, Disjoint (w i).tuple.primeFactors (w j).padding.primeFactors) :
    (∑ w ∈ F, weight (List.ofFn w) *
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.ActualPrimeSlot

theorem OAI.TwoPointCorrelations.crude_numerical_cost_exp_bound line 102

Source documentation

Explicit exponential form of the complete code and reciprocal cost.

theorem crude_numerical_cost_exp_bound (R T b : ℕ)
    (L C U : ℝ) (hR : 1 ≤ R) (hL : 0 < L) (hlog : 1 ≤ Real.log L)
    (hslots : (T : ℝ) ≤ C * R * Real.log L)
    (hT : (T : ℝ) + 1 ≤ L ^ (2 : ℕ)) (hRpoly : (R : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hU : 1 ≤ U) (hUP : U ≤ L ^ b) :
    (∑ n : Fin (T + 1), (Fintype.card (CrudeWordCode R n.val R) : ℝ)) * U ^ T ≤
      Real.exp ((3 + 5 * C + b * C) * R * (Real.log L) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.CrudeWordCode

theorem OAI.TwoPointCorrelations.primeWordEncoding_weight_exp_bound line 148

Source documentation

The numerical assignment sum inherits the explicit code-cost bound.

theorem primeWordEncoding_weight_exp_bound (R T b : ℕ) (P Q : Finset ℕ)
    (L C U : ℝ) (hR : 1 ≤ R) (hL : 0 < L) (hlog : 1 ≤ Real.log L)
    (hslots : (T : ℝ) ≤ C * R * Real.log L)
    (hT : (T : ℝ) + 1 ≤ L ^ (2 : ℕ)) (hRpoly : (R : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hU : 1 ≤ U) (hUP : U ≤ L ^ b)
    (hP : primeHarmonicMass P ≤ U) (hQ : primeHarmonicMass Q ≤ U) :
    (∑ e : PrimeWordEncoding R T P Q, e.weight) ≤
      Real.exp ((3 + 5 * C + b * C) * R * (Real.log L) ^ 2) :=
…

Mentions: OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.PrimeWordEncoding