OAI/NumberTheory/TwoPoint/Bounds/ExistentialWitnesses.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Witness choices are eliminated by the existing relation metadata union.

  1. def OAI.TwoPointCorrelations.HasResampledWitnesses line 13

    Source documentation

    The marked labels and attachment positions may depend on the numerical sample.

    def HasResampledWitnesses {n : ℕ} {ι : Type*} [DecidableEq ι]
    (main : LabeledPrimeWord ι) (word : Fin n → LabeledPrimeWord ι)
    (h s J : ℕ) (supply : ℕ → ℕ → Prop) (value : ι → ℕ) : Prop :=
…

    Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord

  2. theorem OAI.TwoPointCorrelations.has_resampled_witnesses_reciprocal_bound line 20