OAI/Probability/InvariantIsing/Arrays/TensorArrayLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorNamespacedArrayLaw line 15
2. theorem OAI.InvariantIsing.tensorNamespacedArrayLaw_test line 27

   Source documentation

   Injection into the infinite replica sequence gives the exact actual finite-replica mean, while retaining its common rotation.

   theorem tensorNamespacedArrayLaw_test {N m k z : ℕ}
       (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig c : Fin N → ℝ)
       (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
       (n : ℕ) (b : ℕ → ℝ) (r : Fin k → ℕ) (h : ℕ → ℝ)
       (F : SpectralArray (m + 1) → ℝ) (hF : Continuous F)
       (D : SpecialOrthogonal N → (Fin z → Spin N × LabeledLeaf n) → ℝ)
       (ι : Fin z → ℕ) (hi : Function.Injective ι)
       (he : ∀ (U : SpecialOrthogonal N) (σ : ℕ → Spin N × LabeledLeaf n), F (fun ij : ℕ × ℕ =>
         spectralJointEntry (specialRotation U) I n (σ ij.1) (σ ij.2)) = D U (fun i => σ (ι i))) :
       (∫ x, F x ∂(tensorNamespacedArrayLaw μ eig c I degree amplitude n b r h :
         Measure (SpectralArray (m + 1)))) =
         tensorNamespacedReplicaAverage μ eig c I degree amplitude n b r h D := by
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.Spin, OAI.InvariantIsing.spectralJointEntry, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.tensorNamespacedArrayLaw, OAI.InvariantIsing.tensorNamespacedReplicaAverage

3. def OAI.InvariantIsing.finiteSpectralBlock line 56
4. lemma OAI.InvariantIsing.measurable_finiteReplicaBlock line 61
5. lemma OAI.InvariantIsing.measurable_finiteSpectralBlock line 76
6. def OAI.InvariantIsing.permutedSpectralBlockTest line 83
7. lemma OAI.InvariantIsing.measurable_permutedReplicaTest line 89
8. lemma OAI.InvariantIsing.measurable_permutedSpectralBlockTest line 98
9. lemma OAI.InvariantIsing.permutedSpectralBlockTest_embedding line 105