OAI/MeasureTheory/FalconerCompletion/Estimates/OutgoingPower2.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Quantitative estimates for the distance-set construction.

  1. def OAI.GraphLiteralSupport.Attempt4PrefixShell.outgoingPowerND line 16
  2. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.outgoingPowerND_hasDerivAt line 19
  3. def OAI.GraphLiteralSupport.Attempt4PrefixShell.outgoingProfileND line 31
  4. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.outgoingProfileND_hasDerivAt line 34
  5. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.outgoingProfileND_deriv line 45
  6. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.outgoingProfileND_deriv_hasDerivAt line 52
  7. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.radialHelmholtz_outgoingProfileND line 80
  8. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.nat_cast_le_inftyND line 110
  9. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.complex_coordinate_contDiffND line 113
  10. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.smooth_deriv_complexND line 116
  11. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.complex_coordinate_jetsND line 120
  12. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.iteratedDeriv_coordinate_mulND line 131
  13. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.iteratedDeriv_coordinate_derivND line 138
  14. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.iteratedDeriv_coordinate_sq_derivND line 148
  15. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.iteratedDeriv_eq_of_eqOn_positiveND line 163
  16. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.helmholtz_profile_jetsND line 171