OAI/NumberTheory/TwoPoint/Walks/TupleColumnResampling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.wordPosition line 14
2. lemma OAI.TwoPointCorrelations.wordPosition_val line 17
3. def OAI.TwoPointCorrelations.resampledTupleColumnPattern line 22
4. lemma OAI.TwoPointCorrelations.resampledTupleColumnPattern_word line 32
5. theorem OAI.TwoPointCorrelations.tuple_column_high_rank_sum line 56

   Source documentation

   The reciprocal rank bound for an actual one-column fiber, with the other columns, signs and padding held fixed. The selected divisibilities are imposed on the original numerical tuple word after resampling.

   theorem tuple_column_high_rank_sum {J R : ℕ} {P : Fin J → Finset ℕ}
       {ρ : Type*} [Fintype ρ] [DecidableEq ρ]
       (w : ColumnPrimeAssignment J R P) (hR : 0 < R)
       (forward : Fin R → Bool) (padding : Fin R → ℕ) (j : Fin J)
       (F : Finset (Fin R → P j))
       (hpattern : ∀ v ∈ F, ∀ a b, v a = v b ↔ w j a = w j b)
       (h Q D B H : ℕ) (hP : ∀ p ∈ P j, p.Prime)
       (hV : 0 < primeHarmonicMass (P j)) (hH : 0 < H)
       (hlo : ∀ p ∈ P j, H ≤ p) (hbound : ∀ p ∈ P j, p ≤ B)
       (hq : ∀ i, padding i ≤ Q)
       (hd : ∀ i, (∏ l ∈ univ.erase j, (w l i).val) ≤ D)
       (left right : ρ → ℕ) (control : ρ → patternClasses (w j))
   …

   Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.patternClasses