OAI/Analysis/LipschitzHilbert/Trees/BoundaryDistanceAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single common translation is uniform at every angular scale. The folded fractional part has density two on [0,1/2]; no independent translations at distinct levels are introduced.

  1. theorem OAI.LipschitzHilbert.unitBoundaryDistance_integral line 14
  2. theorem OAI.LipschitzHilbert.unitBoundaryDistance_period_integral line 52