NSpinTensorFluctuation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Gaussian-root and cascade fluctuations for the finite tensor model.

lemma OAI.InvariantIsing.measurable_tensorCascadeLog_joint line 14
lemma OAI.InvariantIsing.tensorCascadeValue_root_memLp_two line 31

theorem OAI.InvariantIsing.tensorCascadeLog_root_tree_variance_le line 66

Source documentation

The actual log partition on the product of root marks and marked cascade trees has variance bounded by the sum of the two contributions.

theorem tensorCascadeLog_root_tree_variance_le (hpub : GaussianLipschitzVarianceInput)
    {N m k : ℕ} (hN : 0 < N) (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
    (hb : IsingPerceptron.CascadeExponents n b) (site : ℝ≥0) (monomial : Fin k → ℝ≥0) :
    let root := tensorGaussianLaw I degree (tensorVarianceProfile I degree site monomial)
…

Mentions: OAI.InvariantIsing.GaussianLipschitzVarianceInput, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.IsingPerceptron.CascadeExponents, OAI.InvariantIsing.tensorGaussianLaw, OAI.InvariantIsing.tensorVarianceProfile

theorem OAI.InvariantIsing.normalized_tensorCascadeLog_root_tree_variance_le line 97

Source documentation

For pressure, the Gaussian-root and cascade contributions scale by the square of the volume. The rotation remains fixed in this statement.

theorem normalized_tensorCascadeLog_root_tree_variance_le (hpub : GaussianLipschitzVarianceInput)
    {N m k : ℕ} (hN : 0 < N) (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
    (hb : IsingPerceptron.CascadeExponents n b) (site : ℝ≥0) (monomial : Fin k → ℝ≥0) :
    let root := tensorGaussianLaw I degree (tensorVarianceProfile I degree site monomial)
…