OAI/Probability/InvariantIsing/Arrays/TensorReplicaAverageLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite replica averages under the tensor Gibbs law.

  1. lemma OAI.InvariantIsing.referenceReplicaMean_zero line 14
  2. def OAI.InvariantIsing.tensorNamespacedReplicaAverage line 21
  3. lemma OAI.InvariantIsing.measurable_tensorNamespacedReplicaMean line 31
  4. theorem OAI.InvariantIsing.tensorFrozenGaussian_replicaAverage line 45

    Source documentation

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

    theorem tensorFrozenGaussian_replicaAverage {N m k q : ℕ}
    (μ : 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 : ℕ → ℝ) (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