FieldHeightUpdate.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Identification of the finite covariance charts with literal updates of a field height. The formula is defined without choosing proofs of the order constraints; whenever the updated heights are admissible it is the original fieldValue of that field.

def OAI.InvariantIsing.fieldHeightIncrement line 16
lemma OAI.InvariantIsing.fieldHeightIncrement_eq line 19
lemma OAI.InvariantIsing.fieldHeightIncrement_update line 22
lemma OAI.InvariantIsing.list_set_two line 56
def OAI.InvariantIsing.fieldHeightCoordinateValue line 75
Source documentation
The literal single-coordinate value, using exactly the Gaussian recursion of fieldValue with the updated height vector.
```
def fieldHeightCoordinateValue (h : FieldStep) (i : Fin (h.depth + 1))
    (t z : ℝ) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
lemma OAI.InvariantIsing.gaussianOperator_toNNReal line 82
def OAI.InvariantIsing.fieldWithHeights line 88
Source documentation
The original partition with an admissible updated height vector.
```
def fieldWithHeights (h : FieldStep) (r : Fin (h.depth + 1) → ℝ)
    (hr0 : ∀ i, 0 ≤ r i) (hrmono : Monotone r) : FieldStep :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
lemma OAI.InvariantIsing.fieldHeightCoordinateValue_eq_fieldValue line 92
lemma OAI.InvariantIsing.updated_increments_interior line 115
lemma OAI.InvariantIsing.fieldHeightCoordinateValue_interior line 161
lemma OAI.InvariantIsing.hasDerivAt_fieldHeightCoordinate_interior line 172
lemma OAI.InvariantIsing.updated_increments_final line 184
lemma OAI.InvariantIsing.fieldHeightCoordinateValue_final line 224
lemma OAI.InvariantIsing.hasDerivAt_fieldHeightCoordinate line 231
Source documentation
Exact finite-coordinate gradient of the actual field functional, including the zero root exponent and the final diagonal subtraction.
```
lemma hasDerivAt_fieldHeightCoordinate (h : FieldStep) (i : Fin (h.depth + 1))
    (hstrict : ∀ j, 0 < (fieldIncrement h j).2) :
    HasDerivAt (fun t => fieldHeightCoordinateValue h i t 0)
      (-(h.cut i.succ - h.cut i.castSucc) / 2 * fieldMagnetizationLevel h i) 0 := by
…
```
Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldIncrement, OAI.InvariantIsing.fieldHeightCoordinateValue, OAI.InvariantIsing.fieldMagnetizationLevel