OAI/NumberTheory/DukePrimeDegree/Geometry/DyadicBoundaryCuts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Distance cuts with uniform quantitative boundary bounds

One cut controls all dyadic widths. The constant depends only on the length of the interval from which the cut is selected, not the observable or the probability measure.

  1. def OAI.DukePrimeDegree.dyadicBoundaryCost line 20
  2. lemma OAI.DukePrimeDegree.lintegral_dyadicBoundaryCost line 23
  3. theorem OAI.DukePrimeDegree.exists_dyadic_boundary_cut line 45