OAI/Probability/InvariantIsing/Arrays/NSpinTensorPairPaths.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InvariantIsing.TensorPairPathData line 15
2. def OAI.InvariantIsing.tensorPairPathState line 20
3. lemma OAI.InvariantIsing.measurable_tensorPairPathState line 25
4. lemma OAI.InvariantIsing.measurable_tensorPairSpinMeasures line 35
5. def OAI.InvariantIsing.tensorPairPathSpinKernel line 74
6. instance OAI.InvariantIsing.tensorPairPathSpinKernel_markov line 83
7. def OAI.InvariantIsing.tensorPairPathSpinMean line 89
8. lemma OAI.InvariantIsing.measurable_tensorPairPathSpinMean line 95
9. lemma OAI.InvariantIsing.tensorPairPathSpinMean_abs_le line 105
10. def OAI.InvariantIsing.tensorPairSpinPathPayoff line 113
11. lemma OAI.InvariantIsing.measurable_tensorPairSpinPathPayoff line 121
12. lemma OAI.InvariantIsing.tensorPairSpinPathPayoff_abs_le line 130
13. lemma OAI.InvariantIsing.tensorPairPathState_edges line 142
14. lemma OAI.InvariantIsing.tensorPairPathSpinKernel_edges line 153
15. def OAI.InvariantIsing.tensorSpinPairAverage line 167
16. theorem OAI.InvariantIsing.tensorSpinPairAverage_eq_tiltedPath line 179
17. theorem OAI.InvariantIsing.tensorSpinPair_markov_identity line 208

    Source documentation

    The actual spin/leaf pair expectation is a Markov ancestor-path expectation conditional only on the precise published cascade input.

    theorem tensorSpinPair_markov_identity (hpub : PanchenkoTalagrandTensorPairInput)
        {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 : CascadeExponents n b) (z : SpinTensorIndex I degree → ℝ)
        (ψ : ℕ → ℝ) (D : (Fin 2 → Spin N) → ℝ)
        {B C : ℝ} (hB : 0 ≤ B) (hψ : ∀ d, |ψ d| ≤ B) (hD : ∀ σ, |D σ| ≤ C) :
        tensorSpinPairAverage eig U c I degree amplitude n b v z ψ D =
          ∫ α : ℕ → LabeledLeaf n,
            tensorAncestorPairPathMean eig U c I degree amplitude n b v
              (labeledCommonDepth n (α 0) (α 1)) n 0 z z
    …

    Mentions: OAI.InvariantIsing.PanchenkoTalagrandTensorPairInput, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorSpinPairAverage, OAI.InvariantIsing.tensorAncestorPairPathMean

18. theorem OAI.InvariantIsing.tensorProjectedOverlap_markov_identity line 229
19. theorem OAI.InvariantIsing.tensorRootedSpinPair_markov_identity line 250

    Source documentation

    The root Gaussian retains its original law and is averaged after the conditional spin/ancestor-path identity.

    theorem tensorRootedSpinPair_markov_identity (hpub : PanchenkoTalagrandTensorPairInput)
        {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 : CascadeExponents n b) (ψ : ℕ → ℝ) (D : (Fin 2 → Spin N) → ℝ)
        {B C : ℝ} (hB : 0 ≤ B) (hψ : ∀ d, |ψ d| ≤ B) (hD : ∀ σ, |D σ| ≤ C) :
        (∫ z, tensorSpinPairAverage eig U c I degree amplitude n b (fun i => v (i + 1)) z ψ D
          ∂(tensorGaussianLaw I degree (v 0) : Measure (SpinTensorIndex I degree → ℝ))) =
          ∫ z, ∫ α : ℕ → LabeledLeaf n,
            tensorAncestorPairPathMean eig U c I degree amplitude n b (fun i => v (i + 1))
              (labeledCommonDepth n (α 0) (α 1)) n 0 z z
    …

    Mentions: OAI.InvariantIsing.PanchenkoTalagrandTensorPairInput, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorSpinPairAverage, OAI.InvariantIsing.tensorGaussianLaw, OAI.InvariantIsing.tensorAncestorPairPathMean