OAI/NumberTheory/TwoPoint/Bounds/EncodedWitnessProbability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The encoded witness union has its actual reciprocal-probability majorant.

  1. def OAI.TwoPointCorrelations.WitnessRecord.Realizes line 13
  2. def OAI.TwoPointCorrelations.EncodedWitnessHybridEvent line 20
  3. theorem OAI.TwoPointCorrelations.encoded_witness_hybrid_probability_le line 31