LipschitzRho

Theorem 2.3: rho is 1-Lipschitz

|rho(w) − rho(z)| ≤ ‖w − z‖ for all w, z : ℂ.

Proof:

|rho(w) − rho(z)|
  = | |‖1+w‖ − 1| − |‖1+z‖ − 1| |
  ≤ | ‖1+w‖ − ‖1+z‖ |              (reverse triangle ineq for |· − 1|)
  ≤ ‖(1+w) − (1+z)‖                (reverse triangle ineq for norm)
  = ‖w − z‖

Lean notes:

• abs_abs_sub_abs_le_abs_sub from Mathlib for |t − 1| Lipschitz.
• norm_sub_norm_le for the reverse triangle inequality on ℂ.
• LipschitzWith.comp from Mathlib can compose Lipschitz functions.

theorem FockSPR.rho_lipschitz : LipschitzWith 1 rho

Corollary 2.4: Pointwise comparison via Lipschitz

theorem FockSPR.rho_pointwise_upper (w z : ℂ) : rho w ≤ rho z + ‖w - z‖

rho(w) ≤ rho(z) + ‖w − z‖

theorem FockSPR.rho_pointwise_lower (w z : ℂ) : rho w ≥ rho z - ‖w - z‖

rho(w) ≥ rho(z) − ‖w − z‖

Corollary 2.5: rho(w) ≤ ‖w‖

Proof: Apply 2.4 with z = 0: rho(w) ≤ rho(0) + ‖w‖ = 0 + ‖w‖.

theorem FockSPR.rho_le_norm (w : ℂ) : rho w ≤ ‖w‖