SpinPriorReplicaAverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite replica averages under the actual namespaced tensor Gibbs law.

def OAI.InvariantIsing.spinPriorReplicaAverage line 15
lemma OAI.InvariantIsing.measurable_spinPriorReplicaMean line 25

theorem OAI.InvariantIsing.spinPriorFrozenGaussian_replicaAverage line 40

Source documentation

Gaussian insertion and actual full-model sampling give exactly the same bounded finite-replica averages, retaining the common Haar rotation.

theorem spinPriorFrozenGaussian_replicaAverage {N m k q : ℕ}
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ]
    (π : Measure (Spin 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 : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
    (j : Fin k) (t : ℝ)
    (D : SpecialOrthogonal N → (Fin q → Spin N × LabeledLeaf n) → ℝ)
    (hD : Measurable (Function.uncurry D)) :
    let U := fun ω : TensorFrozenData N n j => ω.1.1
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.TensorFrozenData