OAI/Analysis/LipschitzHilbert/Estimates/SelectedScaleDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The horizontal derivative bound for arbitrary selected scales above a lower length cutoff. It is independent of scale count and dimension.

  1. theorem OAI.LipschitzHilbert.selected_dyadic_reciprocals line 14
  2. theorem OAI.LipschitzHilbert.tile_weighted_vector_derivative_bound line 28
  3. theorem OAI.LipschitzHilbert.selected_scale_weighted_derivative_bound line 54