ResidueWordDependence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual attached-word residue tests depend only on their tuple singleton primes.

def OAI.TwoPointCorrelations.AttachedResiduePositiveWord line 14
Source documentation
Positivity for a word attached at a fixed displacement from the main origin.
```
def AttachedResiduePositiveWord {ι : Type*} (p : ι → ℕ) (h : ℕ)
    (w : List SignedStep) (attachment : ℤ) (B : ℕ) (x : ι → Fin B) : Prop :=
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep
lemma OAI.TwoPointCorrelations.divisor_prime_in_word_support line 21

lemma OAI.TwoPointCorrelations.attached_residue_test_depends line 32

Source documentation

Freeze all other coordinates, including every padding prime.

lemma attached_residue_test_depends {ι : Type*} [Fintype ι] [DecidableEq ι]
    (S : Finset ι) (p : ι → ℕ) (h B : ℕ) (w : List SignedStep) (attachment : ℤ)
    (hsq : ∀ t ∈ w, Squarefree t.tuple)
    (hprime : ∀ i ∈ S, (p i).Prime) (hpad : ∀ i ∈ S, ∀ t ∈ w, ¬p i ∣ t.padding)
    (outside : {i // i ∉ S} → Fin B) :
    DependsOn (wordCoordinateSupport (fun i : S => p i) w)
      (fun z : S → Fin B => decide (AttachedResiduePositiveWord p h w attachment B
        (joinCoordinates S z outside))) := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.DependsOn, OAI.TwoPointCorrelations.wordCoordinateSupport, OAI.TwoPointCorrelations.AttachedResiduePositiveWord, OAI.TwoPointCorrelations.joinCoordinates