OAI/Probability/InvariantIsing/Arrays/NSpinTensorComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.measurable_tensorEnrichedPressure line 16
2. theorem OAI.InvariantIsing.abs_tensorEnrichedPressure_sub_rotation_le line 26

   Source documentation

   Gaussian covariance comparison transfers through the exact flat-model mean identity to the backward recursion pressure itself.

   theorem abs_tensorEnrichedPressure_sub_rotation_le {N m k : ℕ} (hN : 0 < N)
       (eig c : Fin N → ℝ) (U V : SpecialOrthogonal N)
       (K : ℝ) (hK : 0 ≤ K) (heig : ∀ i, |eig i| ≤ K)
       (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
       (n : ℕ) (b : ℕ → ℝ) (hb : CascadeExponents n b)
       (site : ℕ → ℝ≥0) (monomial : ℕ → Fin k → ℝ≥0) :
       let v := fun i => tensorVarianceProfile I degree (site i) (monomial i)
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorVarianceProfile

3. theorem OAI.InvariantIsing.abs_tensorPathPressure_sub_rotation_le line 66

   Source documentation

   For the manuscript's tree power increments, the rotation modulus depends on the perturbation amplitudes and degrees, not the cascade depth.

   theorem abs_tensorPathPressure_sub_rotation_le {N m k : ℕ} (hN : 0 < N)
       (eig c : Fin N → ℝ) (U V : SpecialOrthogonal N)
       (K : ℝ) (hK : 0 ≤ K) (heig : ∀ i, |eig i| ≤ K)
       (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
       (n : ℕ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ)
       (b : ℕ → ℝ) (hb : CascadeExponents n b) :
       let v := tensorPathProfile I degree n treeDegree h
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorPathProfile