OAI/MeasureTheory/Falconer/Estimates/MixedMaskBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mixed derivative bounds for the actual buffered angular masks

  1. theorem OAI.Falconer.normalizedCap_ambient_derivative_zero line 12
  2. theorem OAI.Falconer.capCutoffAmbient_ambient_derivatives line 25