OAI/Probability/InvariantIsing/Core/MixedSpectralFeatures.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.mixedProjectedOverlap line 13
2. lemma OAI.InvariantIsing.mixedProjectedOverlap_abs_le_one line 17
3. lemma OAI.InvariantIsing.mixedProjectedOverlap_sub_first_le line 35
4. lemma OAI.InvariantIsing.spectralSpinFeature_mixed_cross line 53
5. lemma OAI.InvariantIsing.spectralMonomialFeature_mixed_cross line 64
6. theorem OAI.InvariantIsing.spectralMonomialFeature_increment_cross_le line 77

   Source documentation

   The cross covariance of a tensor increment with any rotated tensor has a dimension-independent rotation modulus.

   theorem spectralMonomialFeature_increment_cross_le {N m : ℕ} (hN : 0 < N)
       (U V W : SpecialOrthogonal N) (I : Fin m → Finset (Fin N)) (d : Fin m → ℕ)
       (σ τ : Spin N) :
       |∑ v : SpectralTensorIndex I d,
         (spectralMonomialFeature (specialRotation U) I d σ v -
           spectralMonomialFeature (specialRotation V) I d σ v) *
             spectralMonomialFeature (specialRotation W) I d τ v| ≤
         (∑ a, (d a : ℝ)) * frobeniusDistance U V := by
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.SpectralTensorIndex, OAI.InvariantIsing.spectralMonomialFeature, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.frobeniusDistance