RadialContact.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Contact of a ray from an interior point with the unit sphere

The contact radius exists by the intermediate value theorem on a real interval. A quantitative comparison proves both uniqueness and Lipschitz continuity. No compactness of the ambient unit ball or support functional is used.

theorem OAI.Tingley.contact_comparison_ordered line 25

Source documentation

Comparison of two contacts, with the radii in increasing order. The vectors need not be unit vectors for this estimate.

theorem contact_comparison_ordered (c v w : X) {r s : ℝ}
    (hr : 0 ≤ r) (hrs : r ≤ s)
    (hvr : ‖c + r • v‖ = 1) (hws : ‖c + s • w‖ = 1) :
    (1 - ‖c‖) * (s - r) ≤ (r * s) * ‖v - w‖ := by
…

theorem OAI.Tingley.contact_comparison line 53

Source documentation

A symmetric contact comparison, still independent of unit-norm assumptions on the two direction vectors.

theorem contact_comparison (c v w : X) {r s : ℝ}
    (hr : 0 ≤ r) (hs : 0 ≤ s)
    (hvr : ‖c + r • v‖ = 1) (hws : ‖c + s • w‖ = 1) :
    (1 - ‖c‖) * |r - s| ≤ (r * s) * ‖v - w‖ := by
…

theorem OAI.Tingley.contact_unique line 69

Source documentation

Nonnegative contacts in the same direction are unique when the center is strictly inside the unit ball.

theorem contact_unique (c : X) (hc : ‖c‖ < 1) (v : X) {r s : ℝ}
    (hr : 0 ≤ r) (hs : 0 ≤ s)
    (hvr : ‖c + r • v‖ = 1) (hvs : ‖c + s • v‖ = 1) : r = s := by
…

theorem OAI.Tingley.contact_bounds line 83
Source documentation
Every nonnegative contact in a unit direction has the exact radial bounds, independently of how the contact was obtained.
```
theorem contact_bounds (c : X) (v : UnitSphere X) {r : ℝ}
    (hr : 0 ≤ r) (hcontact : ‖c + r • (v : X)‖ = 1) :
    1 - ‖c‖ ≤ r ∧ r ≤ 1 + ‖c‖ := by
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.existsUnique_radialContact line 97
Source documentation
The genuine positive contact on each ray from an interior center. Existence uses only a compact real interval, never compactness of the ambient sphere.
```
theorem existsUnique_radialContact (c : X) (hc : ‖c‖ < 1)
    (v : UnitSphere X) : ∃! r : ℝ, 0 < r ∧ ‖c + r • (v : X)‖ = 1 := by
…
```
Mentions: OAI.Tingley.UnitSphere
def OAI.Tingley.radialRadius line 124
Source documentation
The radius is chosen from the proved existence theorem.
```
def radialRadius (c : X) (hc : ‖c‖ < 1) (v : UnitSphere X) : ℝ :=
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.radialRadius_spec line 127
theorem OAI.Tingley.radialRadius_pos line 131
theorem OAI.Tingley.norm_radialRadius line 134
theorem OAI.Tingley.radialRadius_bounds line 137
theorem OAI.Tingley.radialRadius_unique line 141

theorem OAI.Tingley.radialRadius_comparison line 148

Source documentation

The quantitative comparison for the chosen contact radii.

theorem radialRadius_comparison (c : X) (hc : ‖c‖ < 1) (v w : UnitSphere X) :
    (1 - ‖c‖) * |radialRadius c hc v - radialRadius c hc w| ≤
      (radialRadius c hc v * radialRadius c hc w) * ‖(v : X) - (w : X)‖ :=
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.radialRadius

theorem OAI.Tingley.radialRadius_sub_le line 155
theorem OAI.Tingley.lipschitz_radialRadius line 184
Source documentation
The radius is globally Lipschitz on the unit sphere for each fixed interior center, even in an infinite-dimensional normed space.
```
theorem lipschitz_radialRadius (c : X) (hc : ‖c‖ < 1) :
    LipschitzWith (Real.toNNReal ((1 + ‖c‖)^2 / (1 - ‖c‖))) (radialRadius c hc) := by
…
```
Mentions: OAI.Tingley.radialRadius
theorem OAI.Tingley.continuous_radialRadius line 190
def OAI.Tingley.radialContact line 194
Source documentation
The actual point of contact, retaining its unit-sphere subtype proof.
```
def radialContact (c : X) (hc : ‖c‖ < 1) (v : UnitSphere X) : UnitSphere X :=
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.radialContact_coe line 197
theorem OAI.Tingley.continuous_radialContact line 200