OAI/MeasureTheory/Falconer/Incidence/WeightedLoomisStep.lean
3 declarations, 0 contain sorry, 0 declared as axioms
The finite weighted Loomis–Whitney induction step
- theorem
OAI.Falconer.finite_root_product_raiseline 11 - def
OAI.Falconer.FiniteWeightedLoomisline 23 - theorem
OAI.Falconer.finite_weighted_loomis_stepline 28