Transport.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Transport and correction of multiplication

These are the algebraic and norm estimates in the UCP criterion of §2 of Universal strong Kadison–Kastler stability (2026). No perturbation theorem is assumed here. If a linear equivalence correcting the transported product is supplied, its composition with the original map gives an actual algebra equivalence.

def OAI.KadisonKastler.transportedMul line 25
Source documentation
Multiplication on the source transported through a linear equivalence.
```
def transportedMul (F : A ≃ₗ[ℂ] B) (x y : A) : A := F.symm (F x * F y)
```
theorem OAI.KadisonKastler.map_transportedMul line 27
theorem OAI.KadisonKastler.transportedMul_assoc line 30
theorem OAI.KadisonKastler.transportedMul_add_left line 36
theorem OAI.KadisonKastler.transportedMul_add_right line 40
theorem OAI.KadisonKastler.transportedMul_smul_left line 44
theorem OAI.KadisonKastler.transportedMul_smul_right line 48
theorem OAI.KadisonKastler.transportedMul_one_left line 52
theorem OAI.KadisonKastler.transportedMul_one_right line 55
theorem OAI.KadisonKastler.transportedMul_sub_eq line 60
Source documentation
The transported product differs from the original product by applying the inverse equivalence to the original map's multiplicative defect.
```
theorem transportedMul_sub_eq (F : A ≃ₗ[ℂ] B) (x y : A) :
    transportedMul F x y - x * y = F.symm (F x * F y - F (x * y)) := by
…
```
Mentions: OAI.KadisonKastler.transportedMul

theorem OAI.KadisonKastler.norm_transportedMul_sub_le line 66

Source documentation

An inverse norm bound and a multiplicative-defect bound control the distance between transported and original multiplication.

theorem norm_transportedMul_sub_le (F : A ≃ₗ[ℂ] B) {K c : ℝ} (hK : 0 ≤ K)
    (hinv : ∀ y, ‖F.symm y‖ ≤ K * ‖y‖)
    (hdefect : ∀ x y, ‖F (x * y) - F x * F y‖ ≤ c * ‖x‖ * ‖y‖)
    (x y : A) : ‖transportedMul F x y - x * y‖ ≤ (K * c) * ‖x‖ * ‖y‖ := by
…

Mentions: OAI.KadisonKastler.transportedMul

theorem OAI.KadisonKastler.inverse_correction_mul line 80
Source documentation
A correction intertwines the transported product and the original one; its inverse intertwines them in the opposite direction.
```
theorem inverse_correction_mul (F : A ≃ₗ[ℂ] B) (L : A ≃ₗ[ℂ] A)
    (hL : ∀ x y, L (transportedMul F x y) = L x * L y) (x y : A) :
    L.symm (x * y) = transportedMul F (L.symm x) (L.symm y) := by
…
```
Mentions: OAI.KadisonKastler.transportedMul

theorem OAI.KadisonKastler.correctedMap_mul line 87

Source documentation

The map F ∘ L⁻¹ is multiplicative after correction.

theorem correctedMap_mul (F : A ≃ₗ[ℂ] B) (L : A ≃ₗ[ℂ] A)
    (hL : ∀ x y, L (transportedMul F x y) = L x * L y) (x y : A) :
    F (L.symm (x * y)) = F (L.symm x) * F (L.symm y) := by
…

Mentions: OAI.KadisonKastler.transportedMul

theorem OAI.KadisonKastler.correctedMap_one line 94
Source documentation
Bijective multiplicativity ensures the corrected map preserves the unit; unit preservation of the original linear maps need not be assumed.
```
theorem correctedMap_one (F : A ≃ₗ[ℂ] B) (L : A ≃ₗ[ℂ] A)
    (hL : ∀ x y, L (transportedMul F x y) = L x * L y) :
    F (L.symm 1) = 1 := by
…
```
Mentions: OAI.KadisonKastler.transportedMul
def OAI.KadisonKastler.correctedAlgEquiv line 104
Source documentation
The genuine algebra equivalence resulting from a correction of the transported product. Its underlying map is exactly F ∘ L⁻¹.
```
def correctedAlgEquiv (F : A ≃ₗ[ℂ] B) (L : A ≃ₗ[ℂ] A)
    (hL : ∀ x y, L (transportedMul F x y) = L x * L y) : A ≃ₐ[ℂ] B :=
…
```
Mentions: OAI.KadisonKastler.transportedMul
theorem OAI.KadisonKastler.correctedAlgEquiv_apply line 109