CorrectionBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Bounds for correcting a transported multiplication

These are the inverse and composition estimates used in the UCP criterion of §2 of Universal strong Kadison–Kastler stability (2026). The estimates are formulated for an explicitly supplied correction map.

theorem OAI.KadisonKastler.norm_inverse_le_of_close_to_id line 21

Source documentation

The inverse norm estimate for a linear equivalence within η < 1 of the identity.

theorem norm_inverse_le_of_close_to_id (L : E ≃ₗ[ℂ] E) {η : ℝ} (hη : η < 1)
    (hclose : ∀ x, ‖L x - x‖ ≤ η * ‖x‖) (x : E) :
    ‖L.symm x‖ ≤ (1 - η)⁻¹ * ‖x‖ := by
…

theorem OAI.KadisonKastler.norm_inverse_sub_le_of_close_to_id line 33

Source documentation

The inverse displacement estimate corresponding to a near-identity linear equivalence.

theorem norm_inverse_sub_le_of_close_to_id (L : E ≃ₗ[ℂ] E) {η : ℝ}
    (hη₀ : 0 ≤ η) (hη : η < 1) (hclose : ∀ x, ‖L x - x‖ ≤ η * ‖x‖)
    (x : E) : ‖L.symm x - x‖ ≤ (η / (1 - η)) * ‖x‖ := by
…

theorem OAI.KadisonKastler.norm_correctedMap_sub_le line 46

Source documentation

Composing a contraction with an inverse correction adds at most the inverse displacement to the original comparison error.

theorem norm_correctedMap_sub_le (L : E ≃ₗ[ℂ] E) (F ρ : E →ₗ[ℂ] G)
    {η e : ℝ} (hη₀ : 0 ≤ η) (hη : η < 1)
    (hL : ∀ x, ‖L x - x‖ ≤ η * ‖x‖)
    (hF : ∀ x, ‖F x‖ ≤ ‖x‖) (hclose : ∀ x, ‖F x - ρ x‖ ≤ e * ‖x‖)
    (x : E) : ‖F (L.symm x) - ρ x‖ ≤ (e + η / (1 - η)) * ‖x‖ := by
…

theorem OAI.KadisonKastler.ucp_correction_parameter_bounds line 63
Source documentation
The correction parameter furnished by the multiplication estimate is small enough for inversion at the manuscript's UCP tolerance.
```
theorem ucp_correction_parameter_bounds {e : ℝ} (he : 0 ≤ e) (he₁ : e < 1 / 1000) :
    0 ≤ 30 * e / (1 - e) ∧ 30 * e / (1 - e) < 1 := by
…
```
theorem OAI.KadisonKastler.ucp_correction_constant_le line 73
Source documentation
The numerical estimate in the UCP criterion: e + η / (1 - η) ≤ 32e for η = 30e / (1 - e).
```
theorem ucp_correction_constant_le {e : ℝ} (he : 0 ≤ e) (he₁ : e < 1 / 1000) :
    e + (30 * e / (1 - e)) / (1 - 30 * e / (1 - e)) ≤ 32 * e := by
…
```

theorem OAI.KadisonKastler.norm_correctedMap_sub_le_thirty_two_mul line 93

Source documentation

The corrected map is within 32e of the comparison map under the explicit correction bound appearing in the UCP criterion.

theorem norm_correctedMap_sub_le_thirty_two_mul
    (L : E ≃ₗ[ℂ] E) (F ρ : E →ₗ[ℂ] G) {e : ℝ}
    (he : 0 ≤ e) (he₁ : e < 1 / 1000)
    (hL : ∀ x, ‖L x - x‖ ≤ (30 * e / (1 - e)) * ‖x‖)
    (hF : ∀ x, ‖F x‖ ≤ ‖x‖) (hclose : ∀ x, ‖F x - ρ x‖ ≤ e * ‖x‖)
    (x : E) : ‖F (L.symm x) - ρ x‖ ≤ (32 * e) * ‖x‖ := by
…