ReturnMapEstimate.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual return map's two-point estimate

The two triangle-inequality comparisons retain the unprimed radius multiplying both direction differences. The sphere isometry connects the actual endpoints; no pairwise estimate for an arbitrary map is assumed.

theorem OAI.Tingley.norm_smul_sub_smul_le_first line 26
Source documentation
Changing both the scalar and a unit vector, retaining the first scalar in front of the direction difference.
```
theorem norm_smul_sub_smul_le_first (a b : ℝ) (ha : 0 ≤ a)
    (v w : UnitSphere X) :
    ‖a • (v : X) - b • (w : X)‖ ≤ a * ‖(v : X) - (w : X)‖ + |a - b| := by
…
```
Mentions: OAI.Tingley.UnitSphere
theorem OAI.Tingley.first_mul_norm_sub_le_smul_sub line 43
Source documentation
Recovering the direction difference from two differently scaled unit vectors, again retaining the first scalar.
```
theorem first_mul_norm_sub_le_smul_sub (a b : ℝ) (ha : 0 ≤ a)
    (v w : UnitSphere X) :
    a * ‖(v : X) - (w : X)‖ ≤ ‖a • (v : X) - b • (w : X)‖ + |a - b| := by
…
```
Mentions: OAI.Tingley.UnitSphere

theorem OAI.Tingley.return_pair_scalar_elimination line 61

Source documentation

The scalar elimination used after the two actual endpoint comparisons. Only the radii by which we divide require strict positivity.

theorem return_pair_scalar_elimination
    (r s u p A B Dg Dw Dv : ℝ) (hr : 0 < r) (hs : 0 < s) (hu : 0 ≤ u)
    (hg : r * Dg ≤ 2 * A + u * Dw)
    (hw : s * Dw ≤ 2 * B + p * Dv) :
    Dg ≤ (u * p / (r * s)) * Dv + 2 * A / r + 2 * u * B / (r * s) := by
…

theorem OAI.Tingley.returnSphere_pair_estimate line 82

Source documentation

The exact two-point estimate for the constructed return map on its actual extremal sphere set. Both endpoint comparisons use the original sphere isometry.

theorem returnSphere_pair_estimate
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (y : UnitSphere X)
    (t : ℝ) (ht : 0 < t ∧ t < 1) (M : ℝ) (hb : HasDefectBound f M)
    {v v' : UnitSphere X}
    (hv : v ∈ extremalSphere f y t ht M)
    (hv' : v' ∈ extremalSphere f y t ht M) :
    ‖(returnSphere f y t ht v : X) - (returnSphere f y t ht v' : X)‖ ≤
      (uRadius f y t ht v * pRadius f y t ht v /
        (rRadius f y t ht v * sRadius f y t ht v)) * ‖(v : X) - (v' : X)‖ +
      2 * |uRadius f y t ht v - uRadius f y t ht v'| / rRadius f y t ht v +
      2 * uRadius f y t ht v * |pRadius f y t ht v - pRadius f y t ht v'| /
        (rRadius f y t ht v * sRadius f y t ht v) := by
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound, OAI.Tingley.extremalSphere, OAI.Tingley.returnSphere, OAI.Tingley.uRadius, OAI.Tingley.pRadius, OAI.Tingley.rRadius, OAI.Tingley.sRadius

theorem OAI.Tingley.returnAmbient_pair_estimate line 170

Source documentation

The same estimate for the totalized ambient map. Membership in the actual extremal set ensures that every ambient function takes its sphere branch.

theorem returnAmbient_pair_estimate
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (y : UnitSphere X)
    (t : ℝ) (ht : 0 < t ∧ t < 1) (M : ℝ) (hb : HasDefectBound f M)
    {v v' : X} (hv : v ∈ extremalSet f y t ht M)
    (hv' : v' ∈ extremalSet f y t ht M) :
    ‖returnAmbient f y t ht v - returnAmbient f y t ht v'‖ ≤
      (uAmbient f y t ht v * pAmbient f y t ht v /
        (rAmbient f y t ht v * sAmbient f y t ht v)) * ‖v - v'‖ +
      2 * |uAmbient f y t ht v - uAmbient f y t ht v'| / rAmbient f y t ht v +
      2 * uAmbient f y t ht v * |pAmbient f y t ht v - pAmbient f y t ht v'| /
        (rAmbient f y t ht v * sAmbient f y t ht v) := by
…

Mentions: OAI.Tingley.UnitSphere, OAI.Tingley.HasDefectBound, OAI.Tingley.extremalSet, OAI.Tingley.returnAmbient, OAI.Tingley.uAmbient, OAI.Tingley.pAmbient, OAI.Tingley.rAmbient, OAI.Tingley.sAmbient

theorem OAI.Tingley.returnAmbient_pair_estimate_on line 188

Source documentation

Restriction to any subset of the actual extremal set, including the closed invariant convex set constructed from the positive schedule.

theorem returnAmbient_pair_estimate_on
    (f : UnitSphere X ≃ᵢ UnitSphere Y) (y : UnitSphere X)
    (t : ℝ) (ht : 0 < t ∧ t < 1) (M : ℝ) (hb : HasDefectBound f M)
    (C : Set X) (hC : C ⊆ extremalSet f y t ht M)
    {v v' : X} (hv : v ∈ C) (hv' : v' ∈ C) :
    ‖returnAmbient f y t ht v - returnAmbient f y t ht v'‖ ≤
      (uAmbient f y t ht v * pAmbient f y t ht v /
        (rAmbient f y t ht v * sAmbient f y t ht v)) * ‖v - v'‖ +
      2 * |uAmbient f y t ht v - uAmbient f y t ht v'| / rAmbient f y t ht v +
      2 * uAmbient f y t ht v * |pAmbient f y t ht v - pAmbient f y t ht v'| /
        (rAmbient f y t ht v * sAmbient f y t ht v) :=
…