OAI/NumberTheory/DukePrimeDegree/Entropy/RootAdaptedObservations.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite generating observations with root neighborhoods in future atoms

  1. instance OAI.DukePrimeDegree.(instance at line 14) line 14
  2. def OAI.DukePrimeDegree.quotientCutEnumeration line 16
  3. lemma OAI.DukePrimeDegree.quotientCutEnumeration_surjective line 19
  4. def OAI.DukePrimeDegree.quotientCutBits line 22
  5. lemma OAI.DukePrimeDegree.quotientCutBits_measurable line 25
  6. lemma OAI.DukePrimeDegree.quotientCutBits_monotone line 29
  7. theorem OAI.DukePrimeDegree.quotientCutBits_generate line 37
  8. def OAI.DukePrimeDegree.quotientCutObservation line 64
  9. lemma OAI.DukePrimeDegree.quotientCutObservation_sigma line 68
  10. lemma OAI.DukePrimeDegree.quotientCutObservation_measurable line 73
  11. theorem OAI.DukePrimeDegree.quotientCutObservation_entropy line 77
  12. theorem OAI.DukePrimeDegree.exists_observations_with_root_neighborhoods line 96