OAI/MeasureTheory/Falconer/Recursion/RoundedHighProfile.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

High-slope length survives inward rounding, with the same explicit endpoint loss as the total retained interval length.

  1. theorem OAI.Falconer.profileHighLength_eq_sum line 10
  2. theorem OAI.Falconer.rounded_profile_high_length_lower line 19