OAI/MeasureTheory/Falconer/Recursion/ProfileSuffixContact.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positive slopes of the future minimum occur at contact points

  1. theorem OAI.Falconer.profileSuffixMinimum_locally_constant_of_gap line 12
  2. theorem OAI.Falconer.profileSuffixMinimum_contact_of_pos_deriv line 48