FieldSecondFamily.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Second-derivative data for the actual two-coordinate scalar recursion. The first coordinate is a finite covariance variation; the second is the scalar field. All bounds are local in the covariance coordinate.

structure OAI.InvariantIsing.FieldSecondFamily line 15
def OAI.InvariantIsing.fieldLogCoshSecondFamily line 28
Source documentation
The actual log-cosh terminal has zero covariance derivatives.
```
def fieldLogCoshSecondFamily (I : Set ℝ) : FieldSecondFamily I where
…
```
Mentions: OAI.InvariantIsing.FieldSecondFamily
def OAI.InvariantIsing.fieldAmplitudeSlope line 53
Source documentation
First derivative of the square-root amplitude.
```
def fieldAmplitudeSlope (a v t : ℝ) : ℝ := v / (2 * Real.sqrt (a + v * t))
```
def OAI.InvariantIsing.fieldAmplitudeCurvature line 56
Source documentation
Its second derivative, written in the chain-rule product form.
```
def fieldAmplitudeCurvature (a v t : ℝ) : ℝ :=
…
```
lemma OAI.InvariantIsing.fieldAmplitudeSlope_hasDerivAt line 59
def OAI.InvariantIsing.FieldSecondFamily.shiftedMean line 81
Source documentation
The affine-noise image of the physical spin mean.
```
def shiftedMean (a v u : ℝ) (p : ℝ × ℝ) : ℝ :=
…
```
def OAI.InvariantIsing.FieldSecondFamily.shiftedTangent line 85
Source documentation
The raw covariance tangent of the affine-noise image of the value.
```
def shiftedTangent (a v u : ℝ) (p : ℝ × ℝ) : ℝ :=
…
```
lemma OAI.InvariantIsing.FieldSecondFamily.shiftedMean_hasFDerivAt line 89
lemma OAI.InvariantIsing.FieldSecondFamily.shiftedTangent_hasFDerivAt line 99