FieldCoordinateDerivative.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Exact single-height derivatives of the finite Gaussian field value. An interior height changes its two adjacent covariance increments with opposite signs. The final height includes the diagonal subtraction.

def OAI.InvariantIsing.fieldFixedAffine line 16
lemma OAI.InvariantIsing.fieldFixedAffine_base line 19
lemma OAI.InvariantIsing.fieldFixedAffine_slope line 26
lemma OAI.InvariantIsing.fieldFixedAffine_increments line 32
def OAI.InvariantIsing.fieldAdjacentIncrements line 44
Source documentation
Actual increment list when a single nonterminal height is varied.
```
def fieldAdjacentIncrements (P S : List (ℝ × ℝ≥0)) (a b ζ η t : ℝ) :
    List (ℝ × ℝ≥0) :=
…
```
def OAI.InvariantIsing.fieldAdjacentLevel line 48
lemma OAI.InvariantIsing.adjacent_value line 53
lemma OAI.InvariantIsing.adjacent_inner_mean line 79

theorem OAI.InvariantIsing.hasDerivAt_fieldAdjacentValue line 106

Source documentation

The manuscript's finite interior-height gradient before the fixed normalizing diagonal term. The derivative is minus half the cell width multiplied by its actual conditional squared spin mean.

theorem hasDerivAt_fieldAdjacentValue
    (P S : List (ℝ × ℝ≥0))
    (hP : ∀ av ∈ P, 0 < (av.2 : ℝ))
    (hS : ∀ av ∈ S, 0 < (av.2 : ℝ))
    (a b ζ η t z : ℝ) (ht : t ∈ Ioo (-a) b) :
    HasDerivAt (fun q => fieldScalarValue (fieldAdjacentIncrements P S a b ζ η q)
      (fun y => Real.log (Real.cosh y)) z)
      (-(η - ζ) / 2 * fieldScalarSquares (fieldAdjacentIncrements P S a b ζ η t)
        (fun y => Real.log (Real.cosh y)) Real.tanh
        (fieldAdjacentLevel P S a b ζ η t) z) t := by
…

Mentions: OAI.InvariantIsing.fieldScalarValue, OAI.InvariantIsing.fieldAdjacentIncrements, OAI.InvariantIsing.fieldScalarSquares, OAI.InvariantIsing.fieldAdjacentLevel

def OAI.InvariantIsing.fieldTerminalIncrements line 190
Source documentation
The terminal height changes the final variance and the normalizing subtraction by the same amount.
```
def fieldTerminalIncrements (P : List (ℝ × ℝ≥0)) (a ζ t : ℝ) :
    List (ℝ × ℝ≥0) := P ++ [(ζ, Real.toNNReal (a + t))]
```
def OAI.InvariantIsing.fieldTerminalLevel line 193
theorem OAI.InvariantIsing.hasDerivAt_fieldTerminalValue line 197