OAI/NumberTheory/TwoPoint/Bounds/NumericalWitnessEvent.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A numerical formulation of the witness event and its exact coded segments.

  1. def OAI.TwoPointCorrelations.NumericalWitnessEvent line 12

    Source documentation

    All conditions involve the original numerical main and witness words.

    def NumericalWitnessEvent {n : ℕ} {ι : Type*}
    (main : List SignedStep) (word : Fin n → List SignedStep) (value : ι → ℕ)
    (h s J : ℕ) (supply : ℕ → ℕ → Prop) : Prop :=
…

    Mentions: OAI.TwoPointCorrelations.SignedStep

  2. lemma OAI.TwoPointCorrelations.has_resampled_witnesses_iff line 28
  3. lemma OAI.TwoPointCorrelations.CrudeWordCode.segment_resample_word line 37