FieldLevelPath.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The bounded monotone representative on the field partition. Endpoint values are immaterial to integration; the representative is defined globally.

def OAI.InvariantIsing.fieldLevelIndex line 14
Source documentation
Last covariance interval whose lower endpoint has been passed.
```
def fieldLevelIndex (h : FieldStep) (s : ℝ) : Fin (h.depth + 1) :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
lemma OAI.InvariantIsing.fieldLevelIndex_monotone line 17
lemma OAI.InvariantIsing.fieldLevelIndex_on_cell line 29
def OAI.InvariantIsing.fieldLevelPath line 53
Source documentation
Monotone unit level values become an admissible overlap path on the same partition as the actual field.
```
def fieldLevelPath (h : FieldStep) (q : Fin (h.depth + 1) → ℝ)
    (hq : Monotone q) (hunit : ∀ i, q i ∈ Icc (0 : ℝ) 1) : OverlapPath where
…
```
Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.OverlapPath
lemma OAI.InvariantIsing.fieldLevelPath_on_cell line 60