OAI/MeasureTheory/Falconer/Estimates/NonstationaryScales.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Scale gain for the angular integration by parts

Depths are normalized by N, so 2^p = R^(p/N) is represented by R^p. The hypotheses and constants are those of graph:range and graph:ibp-ratio, without asymptotic notation.

  1. theorem OAI.Falconer.graph_nonstationary_ratio_bound line 15
  2. theorem OAI.Falconer.graph_radial_oscillation_size line 60