Field.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The one-site Gaussian functional

These are the finite Gaussian recursion and extended-real optimization in (1.5)--(1.7) of the manuscript. The field supremum stays inside the path infimum.

def OAI.InvariantIsing.gaussianOperator line 21
Source documentation
Gaussian logarithmic integration, with ordinary expectation at exponent zero.
Also declared: ComparatorChallenges/InvariantIsing.lean:76 (same declaration text).
```
def gaussianOperator (a v : ℝ) (f : ℝ → ℝ) (z : ℝ) : ℝ :=
…
```
lemma OAI.InvariantIsing.gaussianOperator_zero_variance line 25
structure OAI.InvariantIsing.FieldStep line 33
Source documentation
Positive intervals partitioning the unit interval, with monotone covariance heights.
Also declared: ComparatorChallenges/InvariantIsing.lean:80 (same declaration text).
```
structure FieldStep where
…
```
def OAI.InvariantIsing.fieldFunction line 44
Source documentation
A finite covariance step path, with arbitrary values assigned at its cuts.
Also declared: ComparatorChallenges/InvariantIsing.lean:90 (same declaration text).
```
def fieldFunction (h : FieldStep) (s : ℝ) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
def OAI.InvariantIsing.fieldIncrement line 49
Source documentation
Exponent and covariance increment for one backward step.
Also declared: ComparatorChallenges/InvariantIsing.lean:94 (same declaration text).
```
def fieldIncrement (h : FieldStep) (i : Fin (h.depth + 1)) : ℝ × ℝ :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
def OAI.InvariantIsing.fieldValue line 54
Source documentation
The canonical one-site value at initial bias b, with the diagonal covariance subtraction.
Also declared: ComparatorChallenges/InvariantIsing.lean:98 (same declaration text).
```
def fieldValue (h : FieldStep) (b : ℝ) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
def OAI.InvariantIsing.fieldPairing line 60
Source documentation
The field-order-parameter pairing on (0,1).
Also declared: ComparatorChallenges/InvariantIsing.lean:103 (same declaration text).
```
def fieldPairing (p : OverlapPath) (h : FieldStep) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.FieldStep
def OAI.InvariantIsing.entropyFunctional line 64
Source documentation
Equation (1.6). Infinite suprema are retained as extended real values.
Also declared: ComparatorChallenges/InvariantIsing.lean:106 (same declaration text).
```
def entropyFunctional (p : OverlapPath) : EReal :=
…
```
Mentions: OAI.InvariantIsing.OverlapPath
def OAI.InvariantIsing.spectralFunctional line 68
Source documentation
Equation (1.7) at temperature parameter one.
Also declared: ComparatorChallenges/InvariantIsing.lean:109 (same declaration text).
```
def spectralFunctional (R : ℝ → ℝ) (p : OverlapPath) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.OverlapPath
def OAI.InvariantIsing.variationalFunctional line 72
Source documentation
Equation (1.8), with the infimum outside the field supremum.
Also declared: ComparatorChallenges/InvariantIsing.lean:112 (same declaration text).
```
def variationalFunctional (R : ℝ → ℝ) : EReal :=
…
```
def OAI.InvariantIsing.zeroField line 76
Source documentation
The admissible zero covariance field.
```
def zeroField : FieldStep where
…
```
Mentions: OAI.InvariantIsing.FieldStep
lemma OAI.InvariantIsing.fieldFunction_zero line 89
lemma OAI.InvariantIsing.fieldValue_zero line 93
lemma OAI.InvariantIsing.fieldPairing_zero line 96
lemma OAI.InvariantIsing.entropyFunctional_nonneg line 99
lemma OAI.InvariantIsing.fieldFunction_nonneg line 105
lemma OAI.InvariantIsing.spectralFunctional_constant line 112
lemma OAI.InvariantIsing.integrable_spectral_composition line 117

lemma OAI.InvariantIsing.abs_spectralFunctional_sub_le line 124

Source documentation

Section 6's uniform comparison of spectral functionals.

lemma abs_spectralFunctional_sub_le (R Q : ℝ → ℝ) (hR : Continuous R) (hQ : Continuous Q)
    (δ : ℝ) (hδ : ∀ x ∈ Set.Icc (0 : ℝ) 1, |R x - Q x| ≤ δ) (p : OverlapPath) :
    |spectralFunctional R p - spectralFunctional Q p| ≤ δ / 2 := by
…

Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.spectralFunctional

lemma OAI.InvariantIsing.variationalFunctional_le_add line 146

Source documentation

A common uniform spectral error passes through the path infimum without exchanging the field supremum and the path infimum.

lemma variationalFunctional_le_add (R Q : ℝ → ℝ) (hR : Continuous R) (hQ : Continuous Q)
    (δ : ℝ) (hδ : ∀ x ∈ Set.Icc (0 : ℝ) 1, |R x - Q x| ≤ δ) :
    variationalFunctional R ≤ variationalFunctional Q + ((δ / 2 : ℝ) : EReal) := by
…

Mentions: OAI.InvariantIsing.variationalFunctional