TensorGaussianMean.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Gaussian mean rotation comparison on the concrete countable tensor model.

theorem OAI.InvariantIsing.tensorLeafGaussianMean_abs_sub_le line 19

Source documentation

The Gaussian part of the disorder-averaged leaf partition has a uniform rotation modulus for every countable probability leaf prior.

theorem tensorLeafGaussianMean_abs_sub_le {N m k : ℕ} (hN : 0 < N)
    (U V : SpecialOrthogonal N) (I : Fin m → Finset (Fin N))
    (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ) (n : ℕ)
    (site : Fin (n + 1) → ℝ≥0) (monomial : Fin (n + 1) → Fin k → ℝ≥0)
    (ν : Measure (Spin N × LabeledLeaf n)) [IsProbabilityMeasure ν]
    (H : Spin N × LabeledLeaf n → ℝ) (hH : Integrable (fun x => Real.exp (H x)) ν) :
    let A := fun R => tensorLeafCoefficients (specialRotation R) I degree amplitude n
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorLeafCoefficients, OAI.InvariantIsing.specialRotation

lemma OAI.InvariantIsing.finite_spin_base_exp_integrable line 41

theorem OAI.InvariantIsing.tensorLeafLogMean_abs_sub_le line 53

Source documentation

Both the deterministic quadratic term and the Gaussian tensor marks have uniform rotation moduli for the actual countable leaf partition.

theorem tensorLeafLogMean_abs_sub_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 : ℕ) (site : Fin (n + 1) → ℝ≥0) (monomial : Fin (n + 1) → Fin k → ℝ≥0)
    (ν : Measure (Spin N × LabeledLeaf n)) [IsProbabilityMeasure ν] :
    let H := fun R (x : Spin N × LabeledLeaf n) =>
…

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