WitnessSupport.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Concrete prime supports of numerical witness words.

def OAI.TwoPointCorrelations.wordPrimeSupport line 13
Source documentation
The distinct prime factors of the whole tuples in a word.
```
def wordPrimeSupport : List SignedStep → Finset ℕ
  | [] => ∅
  | a :: w => a.tuple.primeFactors ∪ wordPrimeSupport w
```
Mentions: OAI.TwoPointCorrelations.SignedStep
lemma OAI.TwoPointCorrelations.mem_wordPrimeSupport line 17
lemma OAI.TwoPointCorrelations.mem_wordPrimeSupport_iff line 23
lemma OAI.TwoPointCorrelations.wordPrimeSupport_card_le line 36
def OAI.TwoPointCorrelations.wordCoordinateSupport line 51
Source documentation
Support restricted to the injectively numbered singleton coordinates.
```
def wordCoordinateSupport {ι : Type*} [Fintype ι] (prime : ι → ℕ) (w : List SignedStep) : Finset ι :=
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep
lemma OAI.TwoPointCorrelations.wordCoordinateSupport_card_le line 54

lemma OAI.TwoPointCorrelations.bounded_wordCoordinateSupport line 65

Source documentation

Numerical witness words of length at most s have at most s*J singleton coordinates in their support.

lemma bounded_wordCoordinateSupport {ι : Type*} [Fintype ι] [DecidableEq ι]
    (prime : ι → ℕ) (hinj : Function.Injective prime) (w : List SignedStep) (s J : ℕ)
    (hlen : w.length ≤ s) (hcard : ∀ a ∈ w, a.tuple.primeFactors.card ≤ J) :
    (wordCoordinateSupport prime w).card ≤ s * J :=
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordCoordinateSupport

theorem OAI.TwoPointCorrelations.numerical_witness_cover line 74

Source documentation

The witness-cover conclusion with actual numerical words and actual prime occurrences. Every selected word is positive in the same hybrid, and its marked prime occurs in no other selected word.

theorem numerical_witness_cover {ι W A : Type*} [Fintype ι] [DecidableEq ι]
    [Fintype W] [DecidableEq W] (prime : ι → ℕ) (hinj : Function.Injective prime)
    (word : W → List SignedStep) (I : W → (ι → A) → Bool) (a x : ι → A)
    (hdepends : ∀ w, DependsOn (wordCoordinateSupport prime (word w)) (I w))
    (hnonzero : mixedDifference a (witnessAvoidance I) x ≠ 0)
    (s J T : ℕ) (hlen : ∀ w, (word w).length ≤ s)
    (hsq : ∀ w t, t ∈ word w → Squarefree t.tuple)
    (hcard : ∀ w t, t ∈ word w → t.tuple.primeFactors.card ≤ J)
    (hT : T * (s * J) < Fintype.card ι) :
    ∃ R : Finset W, R.card = T ∧ ∃ H : Finset ι,
      (∀ w ∈ R, I w (forceCoordinates H a x) = true) ∧
      ∃ mark : R → ι, Function.Injective mark ∧
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.DependsOn, OAI.TwoPointCorrelations.wordCoordinateSupport, OAI.TwoPointCorrelations.mixedDifference, OAI.TwoPointCorrelations.witnessAvoidance, OAI.TwoPointCorrelations.forceCoordinates