OAI/MeasureTheory/Falconer/Measures/ProductSchurIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarFalconer.product_moment_integrable line 8
  2. theorem OAI.PlanarFalconer.circle_pair_schur_bound line 23
  3. theorem OAI.PlanarFalconer.original_product_schur_integral line 51