OAI/MeasureTheory/Falconer/Geometry/ProjectionDilation.lean
5 declarations, 0 contain sorry, 0 declared as axioms
Positive dilations of the chosen auxiliary projections
- theorem
OAI.Falconer.map_smul_linearline 12 - theorem
OAI.Falconer.dilated_projected_frostmanline 20 - theorem
OAI.Falconer.exists_contractive_dilationline 27 - theorem
OAI.Falconer.compact_projected_supportline 34 - theorem
OAI.Falconer.projected_supports_disjointline 47