OAI/MeasureTheory/Falconer/Estimates/ClassPairWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original class-pair weights have total mass at most one

  1. theorem OAI.Falconer.Regularization.retained_class_real_mass_sum_le_one line 12
  2. theorem OAI.Falconer.Regularization.retained_class_pair_real_mass_sum_le_one line 23