OAI/Probability/InvariantIsing/Arrays/TensorFieldDerivative.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.randomReplicaAverage_zero_reference line 16
2. def OAI.InvariantIsing.tensorNamespacedMeanPressure line 27
3. def OAI.InvariantIsing.tensorFieldCGFMean line 34
4. def OAI.InvariantIsing.tensorFieldInsertionMean line 44
5. def OAI.InvariantIsing.tensorFieldPairObservable line 51
6. lemma OAI.InvariantIsing.tensorLinearCoefficients_cross line 56
7. lemma OAI.InvariantIsing.tensorLinearCoefficients_variance line 62
8. lemma OAI.InvariantIsing.tensorLinearCoefficients_cross_normalized line 72

   Source documentation

   The Gaussian covariance derivative is exactly the actual spin overlap times the field direction at the common ancestor level.

   lemma tensorLinearCoefficients_cross_normalized {N : ℕ} (hN : 0 < N) (n : ℕ)
       (g : ℕ → ℝ) (hg : Monotone g) (g0 : 0 ≤ g 0)
       (σ : Fin 2 → Spin N × LabeledLeaf n) :
       cylinderCross (tensorLinearCoefficients n g (σ 1))
         (tensorLinearCoefficients n g (σ 0)) = N * tensorFieldPairObservable g σ := by
   …

   Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorLinearCoefficients, OAI.InvariantIsing.tensorFieldPairObservable

9. theorem OAI.InvariantIsing.tensorFieldCGFMean_right_derivative line 82
10. theorem OAI.InvariantIsing.tensorFieldInsertionMean_right_derivative line 108

    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 tensorFieldInsertionMean_right_derivative {N m k : ℕ} (hN : 0 < N)
        (μ : Measure (SpecialOrthogonal 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 (tensorFieldInsertionMean μ eig c I degree amp n b treeDegree h g)
          (-tensorNamespacedReplicaAverage μ eig c I degree amp n b treeDegree h
            (fun _ => tensorFieldPairObservable g) / 2) (Ici 0) 0 := by
    …

    Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorFieldInsertionMean, OAI.InvariantIsing.tensorNamespacedReplicaAverage, OAI.InvariantIsing.tensorFieldPairObservable