SpinPriorDiagonalStatistics.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Diagonal CGF and pressure concentration for the actual constrained cascade model.

def OAI.InvariantIsing.spinPriorDiagonalCGF line 13

theorem OAI.InvariantIsing.spinPriorDiagonalCGF_eq_log_difference line 23

Source documentation

At its true coefficient N e_N w, a frozen diagonal tilt is exactly the actual perturbed partition difference.

theorem spinPriorDiagonalCGF_eq_log_difference {N m k : ℕ} (hN : 0 < N)
    (μ : 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)
    (v : Fin m → ℝ) (t : ℝ) (a : Fin m) (w : ℝ) :
    spinPriorDiagonalCGF π eig c I degree amplitude n r h v t a (N * perturbationScale N * w) =ᵐ[
      (μ.prod (labeledCascadeLaw n b : Measure (LabeledTree n))).prod gaussianCoordinates]
      (fun p => spinPriorNamespacedLog (n := n) π (diagonalPerturbedEigenvalues eig I (Function.update v a w) t)
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.spinPriorDiagonalCGF, OAI.InvariantIsing.spinPriorNamespacedLog, OAI.InvariantIsing.diagonalPerturbedEigenvalues

theorem OAI.InvariantIsing.spinPriorDiagonalCGF_statistics line 61