OAI/Probability/InvariantIsing/Arrays/NSpinTensorRootVariance.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InvariantIsing.TensorGaussianSpace line 15
2. def OAI.InvariantIsing.tensorRootMark line 21

   Source documentation

   Reindex independent standard Euclidean coordinates, then apply the coordinate square roots of the prescribed root variances.

   def tensorRootMark {N m k : ℕ} (I : Fin m → Finset (Fin N))
       (degree : Fin k → Fin m → ℕ) (root : SpinTensorIndex I degree → ℝ≥0)
       (g : TensorGaussianSpace I degree) : SpinTensorIndex I degree → ℝ :=
   …

   Mentions: OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.TensorGaussianSpace

3. lemma OAI.InvariantIsing.measurable_tensorRootMark line 26
4. theorem OAI.InvariantIsing.tensorRootMark_measurePreserving line 32
5. def OAI.InvariantIsing.tensorRootCoefficient line 65
6. lemma OAI.InvariantIsing.spinTensorEnergy_tensorRootMark line 72
7. lemma OAI.InvariantIsing.tensorRootCoefficient_norm_sq_le line 89
8. theorem OAI.InvariantIsing.tensorCascade_shift_comparison line 109
9. lemma OAI.InvariantIsing.spinTensorEnergy_add line 141
10. theorem OAI.InvariantIsing.tensorCascadeValue_root_lipschitz line 150

    Source documentation

    The actual backward cascade recursion remains Lipschitz in the common root Gaussian mark, with the Euclidean coefficient bound of the model.

    theorem tensorCascadeValue_root_lipschitz {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)
        (z : SpinTensorIndex I degree → ℝ) :
        let B : ℝ≥0 := ⟨(site : ℝ) * N + ∑ j, (monomial j : ℝ) * amplitude j ^ 2,
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.IsingPerceptron.CascadeExponents

11. theorem OAI.InvariantIsing.tensorCascadeValue_root_variance_le line 195

    Source documentation

    Root Gaussian variance of the existing tensor recursion. This is conditional only on the explicitly cited finite Gaussian Poincaré input.

    theorem tensorCascadeValue_root_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) :
        variance (tensorCascadeValue eig U c I degree amplitude n b v)
          (tensorGaussianLaw I degree (tensorVarianceProfile I degree site monomial) :
            Measure (SpinTensorIndex I degree → ℝ)) ≤
          (site : ℝ) * N + ∑ j, (monomial j : ℝ) * amplitude j ^ 2 := by
    …

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

12. theorem OAI.InvariantIsing.normalized_tensorCascadeValue_root_variance_le line 218