OAI/MeasureTheory/Falconer/Recursion/ProfileCellFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Invariants for the finite profile-merging recursion. The original equal width cells are retained as witnesses when their active prefixes are shortened.

  1. structure OAI.Falconer.ProfileCellFamily line 11
  2. structure OAI.Falconer.StructuredProfilePieces line 16
  3. theorem OAI.Falconer.ProfileCellFamily.actual_ordered line 25
  4. theorem OAI.Falconer.ProfileCellFamily.clip line 32
  5. theorem OAI.Falconer.ProfileCellFamily.active_linear line 46
  6. theorem OAI.Falconer.StructuredProfilePieces.nil line 55
  7. theorem OAI.Falconer.StructuredProfilePieces.append_interval line 59