OAI/Probability/InvariantIsing/Fields/SpinPriorFieldDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The right derivative of an independent linear-field insertion in the actual namespaced tensor model. The variance-zero endpoint is included.

  1. def OAI.InvariantIsing.spinPriorFieldCGFMean line 18
  2. def OAI.InvariantIsing.spinPriorFieldInsertionMean line 28
  3. theorem OAI.InvariantIsing.spinPriorFieldCGFMean_right_derivative line 35
  4. theorem OAI.InvariantIsing.spinPriorFieldInsertionMean_right_derivative line 62

    Source documentation

    The diagonal Gaussian term is canceled by the actual -h(top)/2 normalization. This is the contact derivative, including zero and tied field increments, before identifying the inserted field with h+a*g.

    theorem spinPriorFieldInsertionMean_right_derivative {N m k : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ]
    (π : Measure (Spin N)) [IsProbabilityMeasure π] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amp : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h g : ℕ → ℝ)
    (hg : Monotone g) (g0 : 0 ≤ g 0) :
    HasDerivWithinAt (spinPriorFieldInsertionMean μ π eig c I degree amp n b treeDegree h g)
      (-spinPriorReplicaAverage μ π eig c I degree amp n b treeDegree h
        (fun _ => tensorFieldPairObservable g) / 2) (Ici 0) 0 := by
…

    Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.spinPriorFieldInsertionMean, OAI.InvariantIsing.spinPriorReplicaAverage, OAI.InvariantIsing.tensorFieldPairObservable