SpinPriorFieldDerivativeMean.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.spinPriorFieldInsertedLog_cgf_fold line 16
theorem OAI.InvariantIsing.spinPriorMeanPressure_field_insert line 46

theorem OAI.InvariantIsing.spinPriorMeanPressure_field_right_derivative line 87

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 spinPriorMeanPressure_field_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 : ℕ → ℝ)
    (hh : Monotone h) (h0 : 0 ≤ h 0) (hg : Monotone g) (g0 : 0 ≤ g 0) :
    HasDerivWithinAt
      (fun a => spinPriorMeanPressure (n := n) μ π eig c I degree amp b treeDegree (fun i => h i + a * g i))
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.spinPriorMeanPressure