PathImageOccupation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The Hausdorff measure of a path image counts each point once; arclength occupation counts every traversal. Compact time sets and fine dyadic covers prove the resulting measure domination without an injectivity assumption.

lemma OAI.CircleDomainRigidity.eventually_dyadic_cells_inside_compact line 18
lemma OAI.CircleDomainRigidity.exists_small_dyadic_images_ge line 32
lemma OAI.CircleDomainRigidity.path_hausdorff_image_compact_le_open line 50
lemma OAI.CircleDomainRigidity.path_hausdorff_image_compact_le_length line 96
theorem OAI.CircleDomainRigidity.path_image_hausdorff_le_occupation line 105
Source documentation
A curve's occupation dominates Hausdorff measure on its image, even when the curve retraces itself.
```
theorem path_image_hausdorff_le_occupation (γ : RectifiablePath X) :
    (μH[1] : Measure X).restrict (range γ.val) ≤ pathOccupation γ := by
…
```
Mentions: OAI.CircleDomainRigidity.RectifiablePath, OAI.CircleDomainRigidity.pathOccupation