Distribution.lean`

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Spectral distributions, integrals, and scalar covariance.

theorem OAI.Kaplansky.cuntzCutoff_eq_zero_of_norm_le line 18
Source documentation
A positive cutoff vanishes above the actual spectral norm bound.
```
theorem cuntzCutoff_eq_zero_of_norm_le {a : A} (ha : 0 ≤ a) {ε : ℝ} (hε : ‖a‖ ≤ ε) :
    cuntzCutoff a ε = 0 := by
…
```
Mentions: OAI.Kaplansky.cuntzCutoff
theorem OAI.Kaplansky.cuntzCutoff_one_of_lt line 30
theorem OAI.Kaplansky.CuntzDimensionState.regularized_of_matrix_eq_zero line 38
def OAI.Kaplansky.CuntzDimensionState.distribution line 47
Source documentation
The regularized spectral distribution attached to an actual positive matrix.
```
def distribution (d : CuntzDimensionState A) (a : CuntzPositiveMatrix A) (t : ℝ) : ℝ :=
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix
theorem OAI.Kaplansky.CuntzDimensionState.distribution_antitone line 50
theorem OAI.Kaplansky.CuntzDimensionState.distribution_nonneg line 56
theorem OAI.Kaplansky.CuntzDimensionState.distribution_le_size line 59
theorem OAI.Kaplansky.CuntzDimensionState.distribution_eq_zero line 62
theorem OAI.Kaplansky.CuntzDimensionState.distribution_intervalIntegrable line 69
theorem OAI.Kaplansky.CuntzDimensionState.distribution_add line 73
def OAI.Kaplansky.CuntzDimensionState.spectralValue line 78
Source documentation
Finite layer-cake integral. This definition does not assert the quasitrace axioms.
```
def spectralValue (d : CuntzDimensionState A) (a : CuntzPositiveMatrix A) : ℝ :=
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix
theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_nonneg line 81
theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_le_norm_mul_size line 85
theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_eq_integral line 94
Source documentation
The layer-cake integral is independent of an upper endpoint past the norm.
```
theorem spectralValue_eq_integral (d : CuntzDimensionState A) (a : CuntzPositiveMatrix A)
    {R : ℝ} (hR : ‖CStarMatrix.ofMatrix a.matrix‖ ≤ R) :
    d.spectralValue a = ∫ t in (0 : ℝ)..R, d.distribution a t := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix
theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_add line 108
Source documentation
Block addition is preserved by the finite spectral integral.
```
theorem spectralValue_add (d : CuntzDimensionState A) (a b : CuntzPositiveMatrix A) :
    d.spectralValue (a.add b) = d.spectralValue a + d.spectralValue b := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix
theorem OAI.Kaplansky.CuntzDimensionState.nontrivial line 131
Source documentation
A normalized dimension state forces the underlying algebra to be nonzero.
```
theorem nontrivial (d : CuntzDimensionState A) : Nontrivial A := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
theorem OAI.Kaplansky.CuntzDimensionState.distribution_unit_of_lt line 139
theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_unit line 151
Source documentation
The finite spectral integral has exactly the required matrix-unit values.
```
theorem spectralValue_unit (d : CuntzDimensionState A) (n : ℕ) :
    d.spectralValue (.unit n) = (n : ℝ) := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState
theorem OAI.Kaplansky.cuntzCutoff_pos_smul line 173
Source documentation
Scaling the element rescales the spectral threshold.
```
theorem cuntzCutoff_pos_smul {a : A} (ha : 0 ≤ a) {r : ℝ} (hr : 0 < r) (t : ℝ) :
    cuntzCutoff (r • a) t = r • cuntzCutoff a (t/r) := by
…
```
Mentions: OAI.Kaplansky.cuntzCutoff
def OAI.Kaplansky.CuntzPositiveMatrix.scale line 184
Source documentation
Nonnegative scalar multiplication of a positive finite matrix.
```
def CuntzPositiveMatrix.scale (a : CuntzPositiveMatrix A) (r : ℝ) (hr : 0 ≤ r) :
    CuntzPositiveMatrix A :=
…
```
Mentions: OAI.Kaplansky.CuntzPositiveMatrix
theorem OAI.Kaplansky.CuntzDimensionState.distribution_pos_scale line 191
theorem OAI.Kaplansky.CuntzDimensionState.spectralValue_scale line 202
Source documentation
The integral scales with the positive scalar, including zero.
```
theorem spectralValue_scale (d : CuntzDimensionState A) (a : CuntzPositiveMatrix A)
    (r : ℝ) (hr : 0 ≤ r) :
    d.spectralValue (a.scale r hr) = r * d.spectralValue a := by
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.CuntzPositiveMatrix