OAI/MeasureTheory/FalconerCompletion/Angular/InverseEndpointCoefficientEq.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Angular cutoffs and derivative estimates.

  1. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.inverseEndpointCoefficientND_eq line 20
  2. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.inverseEndpointCoefficientND_paid_cost line 26
  3. def OAI.GraphLiteralSupport.Attempt4PrefixShell.paidSpatialCoefficientND line 47
  4. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.paidSpatialCoefficientND_measurable line 54
  5. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.paidSpatialCoefficientND_integrable line 60
  6. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.paidSpatialCoefficientND_norm_integral line 66
  7. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.paidSpatialCoefficientND_cost line 74
  8. def OAI.GraphLiteralSupport.Attempt4PrefixShell.fullInverseCoefficientCostND line 102
  9. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.fullInverseCoefficientCostND_nonneg line 107
  10. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.full_paidSpatialCoefficientND_cost line 114