OAI/MeasureTheory/Falconer/Recursion/ProfileApplicationBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

One block width and one weak initial constant control all profile-cell estimates and every step of a bounded-length interval composition.

  1. theorem OAI.Falconer.profile_label_le_first_iterate line 10
  2. theorem OAI.Falconer.profile_sixth_power_le_label_square line 21
  3. theorem OAI.Falconer.exists_profile_application_budget line 33