OAI/MeasureTheory/Falconer/Estimates/OneInputMain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Falconer.mainTarget_of_planar_furstenberg line 9

   Source documentation

   Exact all-dimensional conclusion after independently proving the radial input.

   theorem mainTarget_of_planar_furstenberg
       (hFurstenberg : PublishedPlanarFurstenberg) : MainTarget :=
   …

   Mentions: OAI.Falconer.PublishedPlanarFurstenberg, OAI.Falconer.MainTarget