OAI/MeasureTheory/FalconerCompletion/Angular/NearAngularEnergyProfileBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Angular cutoffs and derivative estimates.

  1. theorem OAI.GraphLiteralSupport.Attempt4Near.nearAngularEnergyND_profile_bound line 19
  2. lemma OAI.GraphLiteralSupport.Attempt4Near.angular_four_term_integrableND line 93
  3. theorem OAI.GraphLiteralSupport.Attempt4Near.nearRetainedND_joint_integrable line 129
  4. theorem OAI.GraphLiteralSupport.Attempt4Near.nearRetainedND_integral_prod line 154
  5. def OAI.GraphLiteralSupport.Attempt4Near.farRetainedND line 183
  6. lemma OAI.GraphLiteralSupport.Attempt4Near.near_far_completeND line 189
  7. theorem OAI.GraphLiteralSupport.Attempt4Near.farRetainedND_joint_integrable line 203
  8. theorem OAI.GraphLiteralSupport.Attempt4Near.near_far_integral_identityND line 228
  9. theorem OAI.GraphLiteralSupport.Attempt4Near.sourceAngularHND_near_far_bound line 265