TensorMoment.lean`

61 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.CoordinateSweeps.PositiveTensor.trace_domination line 19
Source comment
Finite positive operators are dominated by their trace times identity.
```
theorem trace_domination (A : Matrix J J ℂ) (hA : A.PosSemidef) :
    (Matrix.trace A • (1 : Matrix J J ℂ) - A).PosSemidef := by
…
```
theorem OAI.CoordinateSweeps.PositiveTensor.projection_trace_domination line 46
Source comment
A positive operator supported on an orthogonal projection is dominated by the same trace times that projection, with no ambient-dimension loss.
```
theorem projection_trace_domination (A P : Matrix J J ℂ) (hA : A.PosSemidef)
    (hP : P.IsHermitian) (hP2 : P*P=P) (hPA : P*A=A) :
    (Matrix.trace A • P - A).PosSemidef := by
…
```
def OAI.CoordinateSweeps.PositiveTensor.outer line 58
theorem OAI.CoordinateSweeps.PositiveTensor.outer_sum_domination line 63
def OAI.CoordinateSweeps.PositiveTensor.partialTrace line 85
Source comment
The literal finite partial trace; it is a sum of positive submatrices.
```
def partialTrace (A : Matrix (J × K) (J × K) ℂ) : Matrix J J ℂ := fun i j => ∑ k, A (i,k) (j,k)
…
```
lemma OAI.CoordinateSweeps.PositiveTensor.partialTrace_posSemidef line 88
lemma OAI.CoordinateSweeps.PositiveTensor.partialTrace_outer_matrix line 97
def OAI.CoordinateSweeps.PositiveTensor.productMatrix line 105
lemma OAI.CoordinateSweeps.PositiveTensor.productMatrix_mul line 109
lemma OAI.CoordinateSweeps.PositiveTensor.productMatrix_star line 119
lemma OAI.CoordinateSweeps.PositiveTensor.productMatrix_smul line 125
lemma OAI.CoordinateSweeps.PositiveTensor.productMatrix_posSemidef line 130
lemma OAI.CoordinateSweeps.PositiveTensor.productMatrix_sum line 141
lemma OAI.CoordinateSweeps.PositiveTensor.productMatrix_mono line 147
lemma OAI.CoordinateSweeps.PositiveTensor.productMatrix_trace line 165
lemma OAI.CoordinateSweeps.PositiveTensor.pair_product_partialTrace line 173
def OAI.CoordinateSweeps.PositiveTensor.inclusion line 184
lemma OAI.CoordinateSweeps.PositiveTensor.inclusion_mulVec_image line 187
lemma OAI.CoordinateSweeps.PositiveTensor.inclusion_mulVec_notin line 192
lemma OAI.CoordinateSweeps.PositiveTensor.inclusion_isometry line 198
lemma OAI.CoordinateSweeps.PositiveTensor.mul_outer_mul_star line 208
lemma OAI.CoordinateSweeps.PositiveTensor.inclusion_trace_outer line 222
lemma OAI.CoordinateSweeps.PositiveTensor.partialTrace_sub line 230
lemma OAI.CoordinateSweeps.PositiveTensor.partialTrace_smul line 235
lemma OAI.CoordinateSweeps.PositiveTensor.partialTrace_sum line 240
lemma OAI.CoordinateSweeps.PositiveTensor.domination_pad line 249
lemma OAI.CoordinateSweeps.PositiveTensor.domination_trans line 255
def OAI.CoordinateSweeps.DependentTensor.tensor line 269
lemma OAI.CoordinateSweeps.DependentTensor.tensor_mul line 273
lemma OAI.CoordinateSweeps.DependentTensor.tensor_star line 283
lemma OAI.CoordinateSweeps.DependentTensor.tensor_trace line 289
lemma OAI.CoordinateSweeps.DependentTensor.tensor_one line 295
lemma OAI.CoordinateSweeps.DependentTensor.tensor_pow line 305
lemma OAI.CoordinateSweeps.DependentTensor.tensor_moment line 311
lemma OAI.CoordinateSweeps.DependentTensor.tensor_posSemidef line 317
lemma OAI.CoordinateSweeps.DependentTensor.tensor_smul line 325
lemma OAI.CoordinateSweeps.DependentTensor.tensor_sum line 331
lemma OAI.CoordinateSweeps.DependentTensor.tensor_mono line 339
Source comment
Tensor positivity is monotone in every factor simultaneously.
```
lemma tensor_mono (A B : ∀ i, Matrix (J i) (J i) ℂ)
    (hA : ∀ i, (A i).PosSemidef) (hAB : ∀ i, (B i-A i).PosSemidef) :
    (tensor B-tensor A).PosSemidef := by
…
```
Mentions: OAI.CoordinateSweeps.DependentTensor.tensor
lemma OAI.CoordinateSweeps.DependentTensor.tensor_mixture line 368
def OAI.CoordinateSweeps.TensorBoard.tensor line 383
lemma OAI.CoordinateSweeps.TensorBoard.tensor_mul line 387
lemma OAI.CoordinateSweeps.TensorBoard.tensor_star line 397
lemma OAI.CoordinateSweeps.TensorBoard.tensor_trace line 403
lemma OAI.CoordinateSweeps.TensorBoard.tensor_one line 409
lemma OAI.CoordinateSweeps.TensorBoard.tensor_posSemidef line 421
lemma OAI.CoordinateSweeps.TensorBoard.trace_mul_nonneg line 431
lemma OAI.CoordinateSweeps.TensorBoard.trace_mono_right line 437

lemma OAI.CoordinateSweeps.TensorBoard.free_product_le_exp line 445

Source comment

The source's deleted-site AMGM loss exp(h), using x≤exp(x−1). This avoids unnecessary equal-size/nonempty column cases.

lemma free_product_le_exp {T : Type*} [Fintype T] (F : Finset T) (x : T → ℝ)
    (hx : ∀ i, 0 ≤ x i) (hs : ∑ i, x i ≤ Fintype.card T) :
    ∏ i ∈ F, x i ≤ Real.exp (Fintype.card T-F.card) := by
…

lemma OAI.CoordinateSweeps.TensorBoard.free_tensor_trace line 461
lemma OAI.CoordinateSweeps.TensorBoard.average_regularization_posDef line 474
lemma OAI.CoordinateSweeps.TensorBoard.exists_whitening line 482
lemma OAI.CoordinateSweeps.TensorBoard.whitening_sum_bound line 491
lemma OAI.CoordinateSweeps.TensorBoard.trace_whitened_sum_le line 503
theorem OAI.CoordinateSweeps.TensorBoard.board_trace_le line 514
theorem OAI.CoordinateSweeps.norm_entry_le_matrix_norm line 559
theorem OAI.CoordinateSweeps.norm_trace_le line 571
theorem OAI.CoordinateSweeps.trace_moment_nonneg line 578
theorem OAI.CoordinateSweeps.trace_moment_le line 582
theorem OAI.CoordinateSweeps.matrix_unitary_norm_le line 591
theorem OAI.CoordinateSweeps.unitary_average_norm_le line 598
def OAI.CoordinateSweeps.schattenMoment line 614
Source comment
Ordinary, unnormalized even Schatten moment. For a matrix K this is Tr((K* K)^q), NOT divided by its dimension.
Also declared: ComparatorChallenges/CoordinateSweeps.lean:206 (same declaration text).
```
def schattenMoment {D : ℕ} (q : ℕ) (K : Matrix (Fin D) (Fin D) ℂ) : ℝ :=
…
```