OAI/MeasureTheory/Falconer/Estimates/ConditionalPlanar.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFalconer.manuscript_main_of_published_radial line 13
2. theorem OAI.PlanarFalconer.mainTarget_of_published_radial line 53

   Source documentation

   The planar restriction of the main theorem, conditional on the published finite-energy radial estimate PublishedPlanarRadialMoment.

   theorem mainTarget_of_published_radial (hOrponen : PublishedPlanarRadialMoment) :
       MainTarget := manuscript_main_of_published_radial hOrponen
   …

   Mentions: OAI.PlanarFalconer.PublishedPlanarRadialMoment, OAI.PlanarFalconer.MainTarget, OAI.PlanarFalconer.manuscript_main_of_published_radial

3. theorem OAI.Falconer.planar_case_of_published_radial line 62

   Source documentation

   The two-dimensional instance of the main theorem.

   theorem planar_case_of_published_radial
       (hOrponen : PlanarFalconer.PublishedPlanarRadialMoment)
       (E : Set (Space 2)) (hE : IsCompact E) (hd : 1 < dimH E) :
       0 < volume (distanceSet E) :=
   …

   Mentions: OAI.PlanarFalconer.PublishedPlanarRadialMoment, OAI.Falconer.Space

4. theorem OAI.Falconer.positive_distance_of_planar_subset line 70

   Source documentation

   A planar compact subset with dimension above one suffices in any ambient Euclidean space, provided the inclusion preserves its original distances.

   theorem positive_distance_of_planar_subset
       (hOrponen : PlanarFalconer.PublishedPlanarRadialMoment)
       {d : ℕ} {E : Set (Space d)} {K : Set (Space 2)}
       (hK : IsCompact K) (hdim : 1 < dimH K)
       (i : Space 2 → Space d) (hi : Isometry i) (hsub : i '' K ⊆ E) :
       0 < volume (distanceSet E) :=
   …

   Mentions: OAI.PlanarFalconer.PublishedPlanarRadialMoment, OAI.Falconer.Space