OAI/MeasureTheory/Falconer/Estimates/ClassRecombination.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact recombination with the original class masses

  1. theorem OAI.Falconer.Regularization.classMeasure_eq_mass_smul line 13
  2. theorem OAI.Falconer.Regularization.retained_class_mass_sum_le_one line 21
  3. theorem OAI.Falconer.Regularization.retained_class_recombination line 30
  4. theorem OAI.Falconer.Regularization.class_original_pair_bad_mass line 50