ProtrusionProjection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A nontrivial continuum has positive transverse overlap with any nearby anchor ball after choosing a suitable direction.

def OAI.CircleDomainRigidity.unitOfNonzero line 16
theorem OAI.CircleDomainRigidity.one_add_im_ne_zero line 21
def OAI.CircleDomainRigidity.tiltedUnit line 26
theorem OAI.CircleDomainRigidity.continuous_tiltedUnit line 29
theorem OAI.CircleDomainRigidity.tiltedUnit_zero line 38
theorem OAI.CircleDomainRigidity.exists_transverse_rotation line 43
Source documentation
Make the projection of a nonzero displacement nonzero while keeping another displacement's projection as small as desired.
```
theorem exists_transverse_rotation {v : ℂ} (hv : v ≠ 0) (w : ℂ) {δ : ℝ} (hδ : 0 < δ) :
    ∃ a : Circle, (rotation a v).im ≠ 0 ∧ |(rotation a w).im| < δ := by
…
```

theorem OAI.CircleDomainRigidity.exists_transverse_interval line 97

Source documentation

A nontrivial continuum through x has a nondegenerate interval of transverse parameters strictly inside the projection of a prescribed anchor ball.

theorem exists_transverse_interval {Q : Set ℂ} (hQ : IsConnected Q) (hnt : Q.Nontrivial)
    {x : ℂ} (hx : x ∈ Q) (c : ℂ) {δ : ℝ} (hδ : 0 < δ) :
    ∃ (a : Circle) (s t : ℝ), s < t ∧
      Icc s t ⊆ (fun z => (rotation a z).im) '' Q ∩
        Ioo ((rotation a c).im - δ) ((rotation a c).im + δ) := by
…