OAI/Probability/InvariantIsing/Arrays/OverlapBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Dimension-independent bounds for projected spectral overlap kernels.

  1. lemma OAI.InvariantIsing.projected_spin_sq_sum_le line 15
  2. lemma OAI.InvariantIsing.projectedOverlap_abs_le_one line 20
  3. lemma OAI.InvariantIsing.projectedOverlap_self_le_one line 38
  4. lemma OAI.InvariantIsing.abs_projected_cross_difference_sum_le line 42
  5. theorem OAI.InvariantIsing.abs_projectedOverlap_sub_rotation_le line 64

    Source documentation

    Every projected overlap has a uniform Frobenius Lipschitz constant. This controls the covariances of the Gaussian GG perturbations.

    theorem abs_projectedOverlap_sub_rotation_le {N : ℕ} (hN : 0 < N)
    (U V : SpecialOrthogonal N) (I : Finset (Fin N)) (σ τ : Spin N) :
    |projectedOverlap (specialRotation U) I σ τ - projectedOverlap (specialRotation V) I σ τ| ≤
      2 * frobeniusDistance U V := by
…

    Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.frobeniusDistance