TensorFieldDerivativeMean.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual field-direction derivative used by the upper contact argument. All Gaussian insertions and actual model means are identified.

theorem OAI.InvariantIsing.tensorFieldInsertedLog_cgf_fold line 16
theorem OAI.InvariantIsing.tensorNamespacedMeanPressure_field_insert line 45

theorem OAI.InvariantIsing.tensorNamespacedMeanPressure_field_right_derivative line 86

Source documentation

A nonnegative monotone field direction is feasible even when base increments vanish or tie. The actual centered pressure has the stated right derivative, with no concentration or path-law input.

theorem tensorNamespacedMeanPressure_field_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 : ℕ → ℝ)
    (hh : Monotone h) (h0 : 0 ≤ h 0) (hg : Monotone g) (g0 : 0 ≤ g 0) :
    HasDerivWithinAt
      (fun a => tensorNamespacedMeanPressure μ eig c I degree amp n b treeDegree (fun i => h i + a * g i))
      (-tensorNamespacedReplicaAverage μ eig c I degree amp n b treeDegree h
        (fun _ => tensorFieldPairObservable g) / 2) (Ici 0) 0 := by
…

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