JordanOrientation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Quantitative exclusion of the reversed Jordan orientation

The calculation in §5 of Universal strong Kadison–Kastler stability excludes an antihomomorphism that is sufficiently close to the inclusion. Closeness alone gives a 3e + e² estimate; contractivity improves it to 3e. The applications to Jordan maps keep the embeddings in the common ambient algebra explicit.

theorem OAI.KadisonKastler.commutator_norm_le_three_terms line 28

Source documentation

The three error terms controlling a commutator under an antimultiplicative map close to an isometric representation.

theorem commutator_norm_le_three_terms
    (ι : A →ₐ[ℂ] D) (F : A →ₗ[ℂ] D) {e : ℝ}
    (hι : ∀ x, ‖ι x‖ = ‖x‖)
    (hclose : ∀ x, ‖F x - ι x‖ ≤ e * ‖x‖)
    (hanti : ∀ x y, F (x * y) = F y * F x) (a b : A) :
    ‖a * b - b * a‖ ≤
      e * ‖a * b‖ + (e * ‖b‖) * ‖F a‖ + ‖b‖ * (e * ‖a‖) := by
…

theorem OAI.KadisonKastler.commutator_norm_le_of_close_antimultiplicative line 58

Source documentation

An antimultiplicative contraction close to an isometric representation forces every commutator to be small.

theorem commutator_norm_le_of_close_antimultiplicative
    (ι : A →ₐ[ℂ] D) (F : A →ₗ[ℂ] D) {e : ℝ} (he : 0 ≤ e)
    (hι : ∀ x, ‖ι x‖ = ‖x‖) (hF : ∀ x, ‖F x‖ ≤ ‖x‖)
    (hclose : ∀ x, ‖F x - ι x‖ ≤ e * ‖x‖)
    (hanti : ∀ x y, F (x * y) = F y * F x) (a b : A) :
    ‖a * b - b * a‖ ≤ 3 * e * ‖a‖ * ‖b‖ := by
…

theorem OAI.KadisonKastler.commutator_norm_le_of_close_antimultiplicative_without_contractivity line 76

Source documentation

Closeness alone controls an antimultiplicative map's commutators; contractivity is not assumed.

theorem commutator_norm_le_of_close_antimultiplicative_without_contractivity
    (ι : A →ₐ[ℂ] D) (F : A →ₗ[ℂ] D) {e : ℝ} (he : 0 ≤ e)
    (hι : ∀ x, ‖ι x‖ = ‖x‖)
    (hclose : ∀ x, ‖F x - ι x‖ ≤ e * ‖x‖)
    (hanti : ∀ x y, F (x * y) = F y * F x) (a b : A) :
    ‖a * b - b * a‖ ≤ (3 * e + e ^ 2) * ‖a‖ * ‖b‖ := by
…

theorem OAI.KadisonKastler.not_antimultiplicative_of_norm_two_commutator line 96

Source documentation

A norm-two commutator of contractions rules out the reversed orientation when 3 * e < 2.

theorem not_antimultiplicative_of_norm_two_commutator
    (ι : A →ₐ[ℂ] D) (F : A →ₗ[ℂ] D) {e : ℝ} (he : 0 ≤ e)
    (hι : ∀ x, ‖ι x‖ = ‖x‖) (hF : ∀ x, ‖F x‖ ≤ ‖x‖)
    (hclose : ∀ x, ‖F x - ι x‖ ≤ e * ‖x‖)
    (a b : A) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1)
    (hab : ‖a * b - b * a‖ = 2) (hsmall : 3 * e < 2) :
    ¬ ∀ x y, F (x * y) = F y * F x := by
…

theorem OAI.KadisonKastler.not_antimultiplicative_of_norm_two_commutator_without_contractivity line 110

Source documentation

A norm-two commutator excludes a close antihomomorphism without contractivity, using the slightly smaller tolerance 3e + e² < 2.

theorem not_antimultiplicative_of_norm_two_commutator_without_contractivity
    (ι : A →ₐ[ℂ] D) (F : A →ₗ[ℂ] D) {e : ℝ} (he : 0 ≤ e)
    (hι : ∀ x, ‖ι x‖ = ‖x‖)
    (hclose : ∀ x, ‖F x - ι x‖ ≤ e * ‖x‖)
    (a b : A) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1)
    (hab : ‖a * b - b * a‖ = 2) (hsmall : 3 * e + e ^ 2 < 2) :
    ¬ ∀ x y, F (x * y) = F y * F x := by
…

theorem OAI.KadisonKastler.PreservesJordan.multiplicative_of_close line 126

Source documentation

A sufficiently close surjective Jordan contraction into a prime algebra has the multiplicative orientation. Closeness is measured after representing the source and target in the same ambient normed algebra.

theorem PreservesJordan.multiplicative_of_close
    (θ : A →ₗ[ℂ] B) (ι : A →ₐ[ℂ] D) (κ : B →ₐ[ℂ] D) {e : ℝ}
    (hθ : PreservesJordan θ) (hsurj : Function.Surjective θ)
    (hprime : IsPrimeAlgebra B) (he : 0 ≤ e)
    (hι : ∀ x, ‖ι x‖ = ‖x‖) (hκ : ∀ x, ‖κ x‖ = ‖x‖)
    (hcontractive : ∀ x, ‖θ x‖ ≤ ‖x‖)
    (hclose : ∀ x, ‖κ (θ x) - ι x‖ ≤ e * ‖x‖)
    (a b : A) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1)
    (hab : ‖a * b - b * a‖ = 2) (hsmall : 3 * e < 2) :
    ∀ x y, θ (x * y) = θ x * θ y := by
…

Mentions: OAI.KadisonKastler.PreservesJordan, OAI.KadisonKastler.IsPrimeAlgebra

theorem OAI.KadisonKastler.PreservesJordan.multiplicative_of_close_without_contractivity line 147

Source documentation

The multiplicative orientation follows from closeness alone, with no contractivity assumption on the Jordan map.

theorem PreservesJordan.multiplicative_of_close_without_contractivity
    (θ : A →ₗ[ℂ] B) (ι : A →ₐ[ℂ] D) (κ : B →ₐ[ℂ] D) {e : ℝ}
    (hθ : PreservesJordan θ) (hsurj : Function.Surjective θ)
    (hprime : IsPrimeAlgebra B) (he : 0 ≤ e)
    (hι : ∀ x, ‖ι x‖ = ‖x‖)
    (hclose : ∀ x, ‖κ (θ x) - ι x‖ ≤ e * ‖x‖)
    (a b : A) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1)
    (hab : ‖a * b - b * a‖ = 2) (hsmall : 3 * e + e ^ 2 < 2) :
    ∀ x y, θ (x * y) = θ x * θ y := by
…

Mentions: OAI.KadisonKastler.PreservesJordan, OAI.KadisonKastler.IsPrimeAlgebra

theorem OAI.KadisonKastler.norm_commutator_of_anticommuting_unitaries line 171
Source documentation
Anticommuting unitaries have a commutator of norm two. In particular this applies to the selfadjoint anticommuting unitaries in a unital matrix algebra.
```
theorem norm_commutator_of_anticommuting_unitaries (a b : unitary A)
    (hab : (a : A) * (b : A) = -((b : A) * (a : A))) :
    ‖(a : A) * (b : A) - (b : A) * (a : A)‖ = 2 := by
…
```

theorem OAI.KadisonKastler.PreservesJordan.multiplicative_of_close_of_anticommuting_unitaries line 183

Source documentation

The form used in the finite-factor argument: a pair of anticommuting unitaries forces the nearby Jordan map to have multiplicative orientation.

theorem PreservesJordan.multiplicative_of_close_of_anticommuting_unitaries
    (θ : A →ₗ[ℂ] B) (ι : A →ₐ[ℂ] D) (κ : B →ₐ[ℂ] D) {e : ℝ}
    (hθ : PreservesJordan θ) (hsurj : Function.Surjective θ)
    (hprime : IsPrimeAlgebra B) (he : 0 ≤ e)
    (hι : ∀ x, ‖ι x‖ = ‖x‖) (hκ : ∀ x, ‖κ x‖ = ‖x‖)
    (hcontractive : ∀ x, ‖θ x‖ ≤ ‖x‖)
    (hclose : ∀ x, ‖κ (θ x) - ι x‖ ≤ e * ‖x‖)
    (a b : unitary A) (hab : (a : A) * (b : A) = -((b : A) * (a : A)))
    (hsmall : 3 * e < 2) : ∀ x y, θ (x * y) = θ x * θ y := by
…

Mentions: OAI.KadisonKastler.PreservesJordan, OAI.KadisonKastler.IsPrimeAlgebra

theorem OAI.KadisonKastler.PreservesJordan.multiplicative_of_close_of_anticommuting_unitaries_without_contractivity line 198

Source documentation

The finite-factor orientation step using only closeness and a pair of anticommuting unitaries, before any contractivity conclusion is available.

theorem PreservesJordan.multiplicative_of_close_of_anticommuting_unitaries_without_contractivity
    (θ : A →ₗ[ℂ] B) (ι : A →ₐ[ℂ] D) (κ : B →ₐ[ℂ] D) {e : ℝ}
    (hθ : PreservesJordan θ) (hsurj : Function.Surjective θ)
    (hprime : IsPrimeAlgebra B) (he : 0 ≤ e)
    (hι : ∀ x, ‖ι x‖ = ‖x‖)
    (hclose : ∀ x, ‖κ (θ x) - ι x‖ ≤ e * ‖x‖)
    (a b : unitary A) (hab : (a : A) * (b : A) = -((b : A) * (a : A)))
    (hsmall : 3 * e + e ^ 2 < 2) : ∀ x y, θ (x * y) = θ x * θ y := by
…

Mentions: OAI.KadisonKastler.PreservesJordan, OAI.KadisonKastler.IsPrimeAlgebra