PriorArrayLaw.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual spectral array generated by a constrained spin/leaf prior.

def OAI.InvariantIsing.priorNamespacedArrayLaw line 12

theorem OAI.InvariantIsing.priorNamespacedArrayLaw_test line 25

Source documentation

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

theorem priorNamespacedArrayLaw_test {N m k n z : ℕ}
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ]
    (ν₀ : Measure (Spin N × LabeledLeaf n)) [IsProbabilityMeasure ν₀] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (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 ∂(priorNamespacedArrayLaw μ ν₀ eig c I degree amplitude r h :
      Measure (SpectralArray (m + 1)))) =
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.spectralJointEntry, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.priorNamespacedArrayLaw