OAI/MeasureTheory/Falconer/Estimates/FiniteClassFactors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Measurable endpoint factors from finite Borel classifications

The angular derivatives are taken on finite families of smooth symbols. Pulling the resulting factors back along measurable endpoint classifiers retains joint measurability, with no measurability assumption on a parameter-dependent derivative. Countable labels allow all scale-indexed finite families to be included before choosing the uniform constants.

  1. theorem OAI.Falconer.SymbolOrder.reindex line 26
  2. def OAI.Falconer.SmoothSeparation.reindex line 38
  3. theorem OAI.Falconer.SmoothSeparation.reindex_value line 47
  4. theorem OAI.Falconer.SmoothSeparation.HasOrder.reindex line 51
  5. theorem OAI.Falconer.finite_class_smooth_measurable line 60
  6. theorem OAI.Falconer.finite_class_inverse_factors line 68