OAI/MeasureTheory/FalconerCompletion/Angular/TwoRpowNMul.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Angular cutoffs and derivative estimates.

  1. lemma OAI.GraphSourceScale.two_rpow_N_mul line 13
  2. lemma OAI.GraphSourceScale.length_scale line 17
  3. lemma OAI.GraphSourceScale.derivative_scale line 27
  4. lemma OAI.GraphSourceScale.inverse_cap_scale line 46
  5. lemma OAI.GraphSourceScale.cap_scale_bound line 58
  6. lemma OAI.GraphSourceScale.ratio_scale line 69
  7. lemma OAI.GraphSourceScale.source_error_scale line 103
  8. lemma OAI.GraphSourceScale.ratio_power_decay line 130