LocalCrossingGeometry.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Local crossing segments from a buffered anchor ball to an inner target region.

theorem OAI.CircleDomainRigidity.continuous_rotatedLine line 14
theorem OAI.CircleDomainRigidity.convex_rotatedLine_preimage line 17
theorem OAI.CircleDomainRigidity.middle_chord_dist line 33
theorem OAI.CircleDomainRigidity.exists_rotated_frontier_parameter line 48
Source documentation
A connected line segment joining the exterior of a closed region to its interior meets the frontier at a parameter different from the exterior endpoint.
```
theorem exists_rotated_frontier_parameter (a : Circle) (y : ℝ)
    {U : Set ℂ} (hU : IsOpen U) {s t : ℝ}
    (hs : rotatedLine a y s ∉ closure U) (ht : rotatedLine a y t ∈ U) :
    ∃ b ∈ uIcc s t, b ≠ s ∧ rotatedLine a y b ∈ frontier U := by
…
```
Mentions: OAI.CircleDomainRigidity.rotatedLine

theorem OAI.CircleDomainRigidity.localized_frontier_crossings line 82

Source documentation

The compact transverse overlap supplies local segments starting strictly in the anchor ball and ending on the inner frontier. The entire paid segment stays in the chosen convex region.

theorem localized_frontier_crossings (a : Circle)
    {U Q W : Set ℂ} (hU : IsOpen U) (hQU : Q ⊆ U) (hQW : Q ⊆ W)
    (hW : Convex ℝ W) {c : ℂ} {δ : ℝ}
    (hball : ball c δ ⊆ (closure U)ᶜ ∩ W) {J : Set ℝ}
    (hJ : J ⊆ (fun z => ((rotation a).symm z).im) '' Q ∩
      Ioo (((rotation a).symm c).im - δ) (((rotation a).symm c).im + δ)) :
    ∀ y ∈ J, ∃ s t : ℝ, s ≠ t ∧
      rotatedLine a y s ∈ ball c δ ∧ rotatedLine a y t ∈ frontier U ∧
      ∀ x ∈ uIcc s t, rotatedLine a y x ∈ W := by
…

Mentions: OAI.CircleDomainRigidity.rotatedLine