KaplanskyTransform.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

A bounded rational transform for Kaplansky approximation

The function 2t/(1+t²) maps the real line into the unit interval. Its operator difference is controlled on two fixed vectors without a bound on the approximating selfadjoint operators. This is the bounded-transform step in Kaplansky approximation.

def OAI.KadisonSimilarity.kaplanskyReciprocal line 21
def OAI.KadisonSimilarity.kaplanskyTransform line 24
theorem OAI.KadisonSimilarity.reciprocal_continuous line 27
theorem OAI.KadisonSimilarity.kaplanskyReciprocal_norm_le line 33
theorem OAI.KadisonSimilarity.kaplanskyReciprocal_mul_norm_le line 41
theorem OAI.KadisonSimilarity.kaplanskyTransform_norm_le line 57
theorem OAI.KadisonSimilarity.kaplanskyReciprocal_right_inverse line 62
theorem OAI.KadisonSimilarity.kaplanskyReciprocal_commute line 75
theorem OAI.KadisonSimilarity.kaplanskyReciprocal_left_inverse line 79
theorem OAI.KadisonSimilarity.kaplanskyReciprocal_difference line 92
Source documentation
The two error vectors are tested after fixed functions of B. No norm bound on A occurs in the resulting strong approximation argument.
```
theorem kaplanskyReciprocal_difference (A D : B)
    (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint D) :
    A * kaplanskyReciprocal A - D * kaplanskyReciprocal D =
      kaplanskyReciprocal A *
        ((A - D) - A * (A - D) * D) * kaplanskyReciprocal D := by
…
```
Mentions: OAI.KadisonSimilarity.kaplanskyReciprocal
def OAI.KadisonSimilarity.kaplanskyFunction line 109
Source documentation
The scalar transform used in bounded approximation.
```
def kaplanskyFunction (t : ℝ) : ℝ := 2 * (t * (1 + t ^ 2)⁻¹)
```
theorem OAI.KadisonSimilarity.kaplanskyFunction_continuous line 111
theorem OAI.KadisonSimilarity.kaplanskyTransform_eq_cfc line 114
def OAI.KadisonSimilarity.kaplanskyInverseFunction line 124
theorem OAI.KadisonSimilarity.kaplanskyInverseFunction_continuous line 127
theorem OAI.KadisonSimilarity.kaplanskyFunction_inverse line 134
def OAI.KadisonSimilarity.kaplanskyPreimage line 147
Source documentation
The bounded inverse branch, defined by functional calculus.
```
def kaplanskyPreimage (T : B) : B := cfc kaplanskyInverseFunction T
```
Mentions: OAI.KadisonSimilarity.kaplanskyInverseFunction
theorem OAI.KadisonSimilarity.kaplanskyPreimage_selfAdjoint line 149
theorem OAI.KadisonSimilarity.kaplanskyPreimage_mem line 152
theorem OAI.KadisonSimilarity.kaplanskyTransform_preimage line 159
Source documentation
Every selfadjoint contraction is a bounded transform of a selfadjoint member of its own generated C-star algebra.
```
theorem kaplanskyTransform_preimage (T : B) (hT : IsSelfAdjoint T)
    (hn : ‖T‖ ≤ 1) : kaplanskyTransform (kaplanskyPreimage T) = T := by
…
```
Mentions: OAI.KadisonSimilarity.kaplanskyTransform, OAI.KadisonSimilarity.kaplanskyPreimage
theorem OAI.KadisonSimilarity.map_kaplanskyTransform line 181
theorem OAI.KadisonSimilarity.kaplanskyReciprocal_difference_apply_le line 190