WitnessMetadataBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite metadata universe yields the actual union bound for singleton systems.

lemma OAI.TwoPointCorrelations.nonnegative_cover_sum line 13

theorem OAI.TwoPointCorrelations.witness_metadata_reciprocal_bound line 33

Source documentation

Count every bounded mode/label/endpoint record and impose only those support conditions needed for successive elimination. Thus this bound contains no assumed probability estimate or assumed number of systems.

theorem witness_metadata_reciprocal_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
    (n N K h : ℕ) (main : LabeledPrimeWord ι) (word : Fin n → LabeledPrimeWord ι)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hV : 1 ≤ primeHarmonicMass P)
    (H B : ℕ) (hH : 0 < H) (hB : 1 ≤ B)
    (hlo : ∀ p ∈ P, H ≤ p) (hhi : ∀ p ∈ P, p ≤ B)
    (hdelta : (H : ℝ)⁻¹ + (1 + Real.log B) / H ≤ 1) :
    (∑ x : ι → P, if ∃ d : WitnessSystemData n N ι,
      K ≤ d.chosen.card ∧ d.Triangular main word h ∧
        d.Holds main word h (integerPrimeAssignment Subtype.val x)
      then ∏ z, ((x z).val : ℝ)⁻¹ else 0) ≤
      (Fintype.card (WitnessSystemData n N ι) : ℝ) * primeHarmonicMass P ^ Fintype.card ι *
        ((H : ℝ)⁻¹ + (1 + Real.log B) / H) ^ K := by
…

Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.WitnessSystemData, OAI.TwoPointCorrelations.integerPrimeAssignment