OAI/NumberTheory/DukePrimeDegree/Entropy/ControlledCutObservation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite observations from controlled distance cuts

The observation records the membership bits of the selected distance balls. Equality of observations gives small relative lifts, while the dyadic estimates imply almost-sure avoidance of all finite cut boundaries.

  1. def OAI.DukePrimeDegree.distanceCutObservation line 19
  2. lemma OAI.DukePrimeDegree.distanceCutObservation_measurable line 22
  3. lemma OAI.DukePrimeDegree.distanceCutObservation_small_lifts line 34
  4. theorem OAI.DukePrimeDegree.ae_eventually_avoid_finite_dyadic_boundaries line 47