OAI/MeasureTheory/Falconer/Geometry/FixedChartBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite derivative bounds for fixed quadratic geometry

Only compact sets inside the smooth chart are used. The chart need not extend smoothly through its outer singularity.

  1. theorem OAI.Falconer.compact_iteratedFDeriv_bound_at line 19
  2. theorem OAI.Falconer.norm_iteratedFDeriv_mul_le_at line 34
  3. def OAI.Falconer.quadraticChartDensity line 55
  4. theorem OAI.Falconer.quadraticChartDensity_contDiffAt line 58
  5. theorem OAI.Falconer.fixed_quadratic_geometry_bounds line 66