OAI/Probability/InvariantIsing/Arrays/TensorDiagonalCGF.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InvariantIsing.TensorFlatDisorder line 16
2. def OAI.InvariantIsing.tensorNamespacedHamiltonian line 18
3. lemma OAI.InvariantIsing.measurable_tensorNamespacedHamiltonian line 26
4. def OAI.InvariantIsing.tensorNamespacedReference line 43
5. instance OAI.InvariantIsing.tensorNamespacedReference_probability line 50
6. lemma OAI.InvariantIsing.measurable_tensorNamespacedReference line 56
7. def OAI.InvariantIsing.tensorDiagonalCGF line 69
8. theorem OAI.InvariantIsing.tensorDiagonalCGF_eq_log_difference line 79

   Source documentation

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

   theorem tensorDiagonalCGF_eq_log_difference {N m k : ℕ} (hN : 0 < N)
       (μ : 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)
       (v : Fin m → ℝ) (t : ℝ) (a : Fin m) (w : ℝ) :
       tensorDiagonalCGF 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 => tensorNamespacedLog (diagonalPerturbedEigenvalues eig I (Function.update v a w) t)
           c I degree amplitude n r h p -
           tensorNamespacedLog (diagonalPerturbedEigenvalues eig I (Function.update v a 0) t)
             c I degree amplitude n r h p) := by
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorDiagonalCGF, OAI.InvariantIsing.tensorNamespacedLog, OAI.InvariantIsing.diagonalPerturbedEigenvalues

9. theorem OAI.InvariantIsing.tensorDiagonalCGF_statistics line 118

   Source documentation

   Actual full-disorder pressure moments give the diagonal CGF's mean and concentration at every bounded coordinate value.

   theorem tensorDiagonalCGF_statistics {N m k : ℕ} (hN : 0 < N)
       (μ : 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)
       (hb : CascadeExponents n b) (v : Fin m → ℝ) (t : ℝ) (a : Fin m) (w B : ℝ)
       (hF : ∀ q : ℝ, q = w ∨ q = 0 →
         MemLp (tensorDisorderPressure (diagonalPerturbedEigenvalues eig I (Function.update v a q) t)
           c I degree amplitude n) 2 (μ.prod (tensorRootTreeLaw I degree n b
             (fun i => tensorPathProfile I degree n r h (i + 1)) (tensorPathProfile I degree n r h 0))))
       (hv : ∀ q : ℝ, q = w ∨ q = 0 →
         variance (tensorDisorderPressure (diagonalPerturbedEigenvalues eig I (Function.update v a q) t)
           c I degree amplitude n) (μ.prod (tensorRootTreeLaw I degree n b
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorDisorderPressure, OAI.InvariantIsing.diagonalPerturbedEigenvalues, OAI.InvariantIsing.tensorRootTreeLaw, OAI.InvariantIsing.tensorPathProfile