OAI/MeasureTheory/Falconer/Recursion/ProfileGrid.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact logarithmic profile values at selected depths

  1. theorem OAI.Falconer.Regularization.intervalRamp_at_upper line 11
  2. theorem OAI.Falconer.Regularization.intervalRamp_at_lower line 14
  3. theorem OAI.Falconer.Regularization.intervalRamp_of_le line 17
  4. theorem OAI.Falconer.Regularization.intervalRamp_of_ge line 20
  5. theorem OAI.Falconer.Regularization.finiteRampProfile_block_difference line 23
  6. theorem OAI.Falconer.Regularization.finiteRampProfile_knots_telescope line 42
  7. theorem OAI.Falconer.Regularization.blockSlope_mul_gap line 53

    Distinct definitions of this name: OAI/MeasureTheory/Falconer/Recursion/ProfileBranchCounts.lean:9 (different declaration text). Qualify references as OAI.Falconer.Regularization.blockSlope_mul_gap@path.

  8. def OAI.Falconer.Regularization.blockLogProduct line 67
  9. theorem OAI.Falconer.Regularization.blockProduct_eq_pow line 72
  10. theorem OAI.Falconer.Regularization.regularizedProfile_grid line 77
  11. theorem OAI.Falconer.Regularization.regularizedProfile_reference_grid line 101