ScalarPhase.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Stability of the removed scalar phase

The dominant-path comparison in §9 removes the scalar phase of its path weight. Relative motion of a nonzero complex weight gives controlled motion of that phase, and hence of the rotated off-path vector.

theorem OAI.LipschitzHilbert.normalize_motion line 29

Source documentation

Unit-vector normalization has a two-over-the-reference-norm bound.

theorem normalize_motion (x y : E) (hx : x ≠ 0) (hy : y ≠ 0) :
    ‖NormedSpace.normalize y - NormedSpace.normalize x‖ ≤ 2 * ‖y - x‖ / ‖x‖ := by
…

def OAI.LipschitzHilbert.scalarPhase line 52
Source documentation
The unit complex phase of a weight.
```
def scalarPhase (z : ℂ) : ℂ := NormedSpace.normalize z
```
theorem OAI.LipschitzHilbert.scalarPhase_eq_div line 54
theorem OAI.LipschitzHilbert.norm_scalarPhase line 58
theorem OAI.LipschitzHilbert.scalarPhase_ne_zero line 61
theorem OAI.LipschitzHilbert.scalarPhase_relative_motion line 69
Source documentation
A relative complex-weight perturbation less than one preserves its nonzero value and moves its unit phase by at most twice that perturbation.
```
theorem scalarPhase_relative_motion {z z' : ℂ} {ε : ℝ}
    (hz : z ≠ 0) (hε : ε < 1) (hmotion : ‖z' - z‖ ≤ ε * ‖z‖) :
    z' ≠ 0 ∧ ‖scalarPhase z' - scalarPhase z‖ ≤ 2 * ε := by
…
```
Mentions: OAI.LipschitzHilbert.scalarPhase
theorem OAI.LipschitzHilbert.scalarPhase_inverse_motion line 84

theorem OAI.LipschitzHilbert.rotated_off_path_motion line 99

Source documentation

Removing moving unit scalar phases costs only phase motion times the size of the off-path vector, in addition to its own motion.

theorem rotated_off_path_motion {z z' : ℂ} {ε K u : ℝ}
    (hz : z ≠ 0) (hε0 : 0 ≤ ε) (hε1 : ε < 1)
    (hweight : ‖z' - z‖ ≤ ε * ‖z‖) (X X' : E)
    (hX : ‖X‖ ≤ K * u) (hmove : ‖X' - X‖ ≤ ε * K * u) :
    ‖(scalarPhase z')⁻¹ • X' - (scalarPhase z)⁻¹ • X‖ ≤ 3 * ε * K * u := by
…

Mentions: OAI.LipschitzHilbert.scalarPhase