SpectralArcResolvents.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Continuous functions approximating the open arc spectral projection.

def OAI.KadisonSimilarity.spectralCutFunction line 14
Source documentation
The positive resolvent approximation to the open cut (c,∞).
```
def spectralCutFunction (c ε t : ℝ) : ℝ := (t - c)⁺ / ((t - c)⁺ + ε)
```
theorem OAI.KadisonSimilarity.spectralCutFunction_continuous line 16
theorem OAI.KadisonSimilarity.spectralCutFunction_nonneg line 23
theorem OAI.KadisonSimilarity.spectralCutFunction_le_one line 27
theorem OAI.KadisonSimilarity.spectralCutFunction_tendsto line 32
theorem OAI.KadisonSimilarity.positiveShift_cfc line 50
theorem OAI.KadisonSimilarity.supportResolvent_positiveShift_eq_cfc line 61
Source documentation
The actual operators in the strong support approximation are evaluations of the scalar continuous cut functions.
```
theorem supportResolvent_positiveShift_eq_cfc (a : H →L[ℂ] H)
    (ha : IsSelfAdjoint a) (c : ℝ) {ε : ℝ} (hε : 0 < ε) :
    supportResolvent (a - c • 1)⁺ ε = cfc (spectralCutFunction c ε) a := by
…
```
Mentions: OAI.KadisonSimilarity.supportResolvent, OAI.KadisonSimilarity.spectralCutFunction