TensorRotationCovariance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Rotation continuity of the concrete finite tensor perturbation marks.

lemma OAI.InvariantIsing.spinTensorFeature_increment_covariance line 14

theorem OAI.InvariantIsing.spinTensorFeature_increment_covariance_le line 39

Source documentation

Linear spin-field marks cancel in the rotation increment. Only the finite spectral tensor covariance contributes to the rotation modulus.

theorem spinTensorFeature_increment_covariance_le {N m k : ℕ} (hN : 0 < N)
    (U V W : SpecialOrthogonal N) (I : Fin m → Finset (Fin N))
    (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (site : ℝ≥0) (monomial : Fin k → ℝ≥0) (σ τ : Spin N) :
    |∑ i : SpinTensorIndex I degree, (tensorVarianceProfile I degree site monomial i : ℝ) *
      (spinTensorFeature (specialRotation U) I degree amplitude σ i -
        spinTensorFeature (specialRotation V) I degree amplitude σ i) *
          spinTensorFeature (specialRotation W) I degree amplitude τ i| ≤
      (∑ j, (monomial j : ℝ) * amplitude j ^ 2 * ∑ a, (degree j a : ℝ)) *
        frobeniusDistance U V := by
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorVarianceProfile, OAI.InvariantIsing.spinTensorFeature, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.frobeniusDistance