WitnessOrdering.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Private witnesses can be indexed by increasing attachment, including ties.

lemma OAI.TwoPointCorrelations.exists_monotone_enumeration line 12

theorem OAI.TwoPointCorrelations.ordered_numerical_witness_cover line 22

Source documentation

The cover is enumerated after selection, so sorting introduces no factor counting all covering subfamilies or possible hybrid choices.

theorem ordered_numerical_witness_cover {ι W A : Type*}
    [Fintype ι] [DecidableEq ι] [Fintype W] [DecidableEq W]
    (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 : 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 ι) :
    ∃ index : Fin T → W, Function.Injective index ∧
…

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