OAI/MeasureTheory/Falconer/Geometry/NormalizedDescriptorFamily.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One normalized descriptor inverse family for every large scale

The operator, its finite index set, and all constants are chosen before the scale label. Every original descriptor remains in the support condition.

  1. theorem OAI.Falconer.equal_scale_product_derivatives line 18
  2. theorem OAI.Falconer.normalized_descriptor_inverse_family line 47