KernelEnergy.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Positive rank-one kernel energy. Matrices are represented by their entries with the unnormalized Hilbert–Schmidt (Euclidean coefficient) norm.

def OAI.Dixmier.rankOneCoefficients line 17
theorem OAI.Dixmier.rankOneCoefficients_apply line 21
theorem OAI.Dixmier.rankOne_inner line 24
theorem OAI.Dixmier.rankOne_inner_re line 38
theorem OAI.Dixmier.rankOne_norm_sq line 43
def OAI.Dixmier.kernelCoefficients line 51
Source documentation
Collision blocks are sums of the rank-one matrices with that label value.
```
def kernelCoefficients (v : I → EuclideanSpace ℂ K) (s : I → G) (g : G) :
    EuclideanSpace ℂ (K × K) :=
…
```
theorem OAI.Dixmier.rankOne_sum_energy line 58
Source documentation
Positivity of every pairwise Hilbert–Schmidt inner product makes each block’s energy at least the number of its unit rank-one summands.
```
theorem rankOne_sum_energy (v : I → EuclideanSpace ℂ K) (hv : ∀ i, ‖v i‖ = 1)
    (J : Finset I) : (J.card : ℝ) ≤ ‖∑ i ∈ J, rankOneCoefficients (v i)‖^2 := by
…
```
Mentions: OAI.Dixmier.rankOneCoefficients
def OAI.Dixmier.coefficientMatrix line 76
theorem OAI.Dixmier.coefficient_norm_sq_eq_trace line 81
Source documentation
The coefficient norm is the unnormalized trace definition of Hilbert–Schmidt squared norm.
```
theorem coefficient_norm_sq_eq_trace (W : EuclideanSpace ℂ (K × K)) :
    ‖W‖^2 = (Matrix.trace (Matrix.conjTranspose (coefficientMatrix W) * coefficientMatrix W)).re := by
…
```
Mentions: OAI.Dixmier.coefficientMatrix
theorem OAI.Dixmier.kernelCoefficients_offsupport line 91
theorem OAI.Dixmier.kernel_energy_summable line 98

theorem OAI.Dixmier.kernel_energy_ge_card line 106

Source documentation

The kernel-energy lower bound preserves every colliding product label.

theorem kernel_energy_ge_card (v : I → EuclideanSpace ℂ K) (hv : ∀ i, ‖v i‖ = 1)
    (s : I → G) : (Fintype.card I : ℝ) ≤ ∑' g, ‖kernelCoefficients v s g‖^2 := by
…

Mentions: OAI.Dixmier.kernelCoefficients