OAI/MeasureTheory/Falconer/Angular/GlobalCapBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Global ambient bounds for the actual normalized cap cutoffs

The packing argument works around every ambient point. The fixed smooth reciprocal also keeps the sum of all normalized caps between zero and one off the sphere. These are the bounds needed by the separated jet operators.

  1. theorem OAI.Falconer.separated_ambient_overlap line 16
  2. theorem OAI.Falconer.capDenominator_global_derivatives line 40
  3. theorem OAI.Falconer.capReciprocal_global_derivatives line 74
  4. theorem OAI.Falconer.normalizedCap_global_derivatives line 96
  5. theorem OAI.Falconer.capCutoffAmbient_global_derivatives line 129
  6. theorem OAI.Falconer.smoothReciprocal_nonneg line 168
  7. theorem OAI.Falconer.mul_smoothReciprocal_le_one line 173
  8. theorem OAI.Falconer.normalizedCap_global_nonneg line 183
  9. theorem OAI.Falconer.normalizedCap_global_sum_le_one line 190
  10. theorem OAI.Falconer.capCutoffAmbient_global_bounds line 196