OAI/MeasureTheory/Falconer/Recursion/ProfileBranchCounts.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact logarithmic coordinates for the retained block branching counts.

  1. theorem OAI.Falconer.Regularization.blockSlope_mul_gap line 9

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

  2. theorem OAI.Falconer.Regularization.regularizedProfile_node_difference line 24
  3. theorem OAI.Falconer.Regularization.blockProduct_real_rpow line 45
  4. theorem OAI.Falconer.Regularization.blockProduct_profile_difference line 55
  5. theorem OAI.Falconer.Regularization.blockProduct_ratio_profile line 63
  6. theorem OAI.Falconer.Regularization.blockProduct_inverse_ratio_profile line 74
  7. theorem OAI.Falconer.Regularization.regularizedProfile_lower_of_ratio_bound line 82