OAI/MeasureTheory/Falconer/Incidence/WeightedLoomisBase.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Base and induction for the finite weighted projection inequality

  1. def OAI.Falconer.twoCoordinateEquiv line 11
  2. theorem OAI.Falconer.finite_weighted_loomis_one line 20
  3. theorem OAI.Falconer.finite_weighted_loomis_whitney line 37