SpectralClipping.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Norm clipping with preserved support and quotient image

The cutoff multiplies an element on the right by a continuous function of its absolute value. Both the clipped part and the discarded part have star squares bounded by the original star square.

def OAI.KadisonKastler.clippingFunction line 23
theorem OAI.KadisonKastler.clippingFunction_continuous line 25
theorem OAI.KadisonKastler.clippingFunction_nonneg line 30
theorem OAI.KadisonKastler.clippingFunction_le_one line 34
theorem OAI.KadisonKastler.mul_clippingFunction line 38
theorem OAI.KadisonKastler.clippingFunction_square_le line 47
theorem OAI.KadisonKastler.clippingFunction_square_le_bound line 55
theorem OAI.KadisonKastler.discardedFunction_square_le line 62
def OAI.KadisonKastler.spectralClip line 72

theorem OAI.KadisonKastler.star_mul_cfc_abs line 76

Source documentation

A scalar functional-calculus identity for any continuous right multiplier.

theorem star_mul_cfc_abs (x : A) (f : ℝ → ℝ) (hf : Continuous f) :
    star (x * cfc f (CFC.abs x)) * (x * cfc f (CFC.abs x)) =
      cfc (fun t => (t * f t) ^ 2) (CFC.abs x) := by
…

theorem OAI.KadisonKastler.spectralClip_star_mul_self line 94
theorem OAI.KadisonKastler.spectralClip_star_mul_self_le line 100
Source documentation
Clipping does not increase the star square.
```
theorem spectralClip_star_mul_self_le {β : ℝ} (hβ : 0 < β) (x : A) :
    star (spectralClip β x) * spectralClip β x ≤ star x * x := by
…
```
Mentions: OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.spectralClip_discard_star_mul_self_le line 110
Source documentation
The discarded part also has star square bounded by the original.
```
theorem spectralClip_discard_star_mul_self_le {β : ℝ} (hβ : 0 < β) (x : A) :
    star (x - spectralClip β x) * (x - spectralClip β x) ≤ star x * x := by
…
```
Mentions: OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.spectralClip_norm_le line 126
theorem OAI.KadisonKastler.mul_right_eq_of_star_mul_self_le line 137
Source documentation
Star-square domination preserves every right support identity.
```
theorem mul_right_eq_of_star_mul_self_le (x y p : A)
    (hxy : star y * y ≤ star x * x) (hxp : x * p = x) : y * p = y := by
…
```
theorem OAI.KadisonKastler.spectralClip_mul_right_eq line 151
theorem OAI.KadisonKastler.spectralClip_eq_self line 155
theorem OAI.KadisonKastler.starAlgHom_map_abs line 171
theorem OAI.KadisonKastler.map_spectralClip line 183
Source documentation
The cutoff is natural for star homomorphisms, including quotient maps.
```
theorem map_spectralClip (π : A →⋆ₐ[ℂ] B) {β : ℝ} (hβ : 0 < β) (x : A) :
    π (spectralClip β x) = spectralClip β (π x) := by
…
```
Mentions: OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.map_spectralClip_eq line 191
Source documentation
If the image is already in the target ball, clipping changes the element only by an element of the homomorphism's kernel.
```
theorem map_spectralClip_eq {β : ℝ} (π : A →⋆ₐ[ℂ] B) (hβ : 0 < β) (x : A)
    (hx : ‖π x‖ ≤ β) : π (spectralClip β x) = π x := by
…
```
Mentions: OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.map_sub_spectralClip_eq_zero line 195