OAI/NumberTheory/DukePrimeDegree/Entropy/SummablePartitionBoundaries.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Choosing partition cuts with summable boundary returns

Almost every real cut of a measurable real-valued function has summable strip masses for any summable sequence of widths. Invariant dynamics therefore avoid those shrinking strips eventually almost everywhere. This supplies the boundary control for partitions subordinate to contracting root leaves.

  1. def OAI.DukePrimeDegree.realBoundaryStrip line 26
  2. lemma OAI.DukePrimeDegree.realBoundaryStrip_measurableSet line 29
  3. lemma OAI.DukePrimeDegree.measurable_realBoundaryStrip_mass line 35
  4. lemma OAI.DukePrimeDegree.lintegral_realBoundaryStrip_mass line 44
  5. theorem OAI.DukePrimeDegree.ae_summable_realBoundaryStrip_mass line 62
  6. lemma OAI.DukePrimeDegree.fiber_null_of_summable_realBoundaryStrip_mass line 72
  7. theorem OAI.DukePrimeDegree.ae_eventually_avoid_realBoundaryStrip line 88
  8. theorem OAI.DukePrimeDegree.exists_cut_with_summable_boundary_returns line 101