SelectedWitnesses.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Apply the witness-cover argument only to the centered singleton coordinates.

lemma OAI.TwoPointCorrelations.word_dependsOn_restrict line 17
Source documentation
Freeze every coordinate outside the selected singleton set. Dependence on actual prime support restricts to the corresponding singleton support.
```
lemma word_dependsOn_restrict (S : Finset ι) (prime : ι → ℕ)
    (word : List SignedStep) (I : (ι → A) → Bool)
    (hI : DependsOn (wordCoordinateSupport prime word) I)
    (outside : {i // i ∉ S} → A) :
    DependsOn (wordCoordinateSupport (fun i : S => prime i) word)
      (fun z : S → A => I (joinCoordinates S z outside)) := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.DependsOn, OAI.TwoPointCorrelations.wordCoordinateSupport, OAI.TwoPointCorrelations.joinCoordinates

theorem OAI.TwoPointCorrelations.selected_ordered_numerical_witness_cover line 36

Source documentation

Nonzero selected centering yields a single hybrid containing the ordered family of witnesses. No extra choices of outside coordinates or independent hybrid draws are introduced.

theorem selected_ordered_numerical_witness_cover
    (S : Finset ι) (prime : ι → ℕ) (hinj : Function.Injective prime)
    (word : W → List SignedStep) (attachment : W → ℕ)
    (I : W → (ι → A) → Bool) (a x : ι → A)
    (hdepends : ∀ w, DependsOn (wordCoordinateSupport prime (word w)) (I w))
    (hnonzero : selectedMixedDifference S 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) < S.card) :
    ∃ index : Fin T → W, Function.Injective index ∧
      Monotone (fun i => attachment (index i)) ∧ ∃ H : Finset S,
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.DependsOn, OAI.TwoPointCorrelations.wordCoordinateSupport, OAI.TwoPointCorrelations.selectedMixedDifference, OAI.TwoPointCorrelations.witnessAvoidance