OAI/MeasureTheory/FalconerCompletion/Estimates/OutgoingPower.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Quantitative estimates for the distance-set construction.

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