OAI/NumberTheory/TwoPoint/Bounds/ResampledWitnesses.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.ResampledWitnessEvent line 16

   Source documentation

   Conditions on an actual numerical assignment, before enlarging its event into the finite union of symbolic relation systems.

   def ResampledWitnessEvent {n : ℕ} {ι : Type*} [DecidableEq ι]
       (main : LabeledPrimeWord ι) (word : Fin n → LabeledPrimeWord ι)
       (h s J : ℕ) (supply : ℕ → ℕ → Prop)
       (mark : Fin n → ι) (attachment position : Fin n → ℕ) (value : ι → ℕ) : Prop :=
   …

   Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord

2. lemma OAI.TwoPointCorrelations.resampled_witness_metadata line 34
3. theorem OAI.TwoPointCorrelations.resampled_witness_reciprocal_bound line 58

   Source documentation

   The actual witness event has the same prime-power saving as the metadata union. Coincident prime assignments are allowed in the enlarged union.

   theorem resampled_witness_reciprocal_bound {n K h s J N : ℕ} {supply : ℕ → ℕ → Prop}
       {ι : Type*} [Fintype ι] [DecidableEq ι]
       (main : LabeledPrimeWord ι) (word : Fin n → LabeledPrimeWord ι)
       (mark : Fin n → ι) (attachment position : Fin n → ℕ)
       (hsize : 8 * K ≤ n) (horder : Monotone attachment)
       (hbound : ∀ i, attachment i ≤ main.word.length)
       (hmainLength : main.word.length ≤ N) (hwordLength : ∀ i, (word i).word.length ≤ N)
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hV : 1 ≤ primeHarmonicMass P)
       (H B : ℕ) (hH : 0 < H) (hB : 1 ≤ B)
       (hlo : ∀ p ∈ P, H ≤ p) (hhi : ∀ p ∈ P, p ≤ B)
       (hdelta : (H : ℝ)⁻¹ + (1 + Real.log B) / H ≤ 1) :
       (∑ a : ι → P, if ResampledWitnessEvent main word h s J supply mark attachment position
   …

   Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.ResampledWitnessEvent