OAI/MeasureTheory/Falconer/Recursion/ProfileBetweenNodes.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Propagating the discrete profile bounds across each actual interpolation block.

  1. theorem OAI.Falconer.Regularization.finiteRampProfile_affine_on_block line 8
  2. theorem OAI.Falconer.Regularization.exists_profile_block line 45
  3. theorem OAI.Falconer.Regularization.finiteRampProfile_lower_between_nodes line 57