FieldMajorant.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The entropy-domain majorant

The explicit majorant in Lemma fld:domain of Section 2 is unbounded but has linear growth. Its Gaussian bounds follow from exponential moments.

def OAI.InvariantIsing.fieldMajorant line 22
Source documentation
The function g_d used for the finite entropy-domain estimate.
```
def fieldMajorant (d z : ℝ) : ℝ :=
…
```
lemma OAI.InvariantIsing.exp_add_exp_neg_eq_two_cosh line 25
lemma OAI.InvariantIsing.fieldMajorant_eq_logcosh line 30
lemma OAI.InvariantIsing.fieldMajorant_zero line 39
lemma OAI.InvariantIsing.measurable_fieldMajorant line 44
lemma OAI.InvariantIsing.fieldMajorant_linearGrowth line 48
lemma OAI.InvariantIsing.logcosh_le_fieldMajorant line 62
Source documentation
The terminal Ising payoff lies below g_d when d ≤ 1.
```
lemma logcosh_le_fieldMajorant {d : ℝ} (hd : 0 < d) (hd1 : d ≤ 1) (z : ℝ) :
    Real.log (Real.cosh z) ≤ fieldMajorant d z := by
…
```
Mentions: OAI.InvariantIsing.fieldMajorant

lemma OAI.InvariantIsing.weighted_exp_log_sum_le line 86

Source documentation

A two-point convexity inequality. Its weights are the two terms of the partition function at the unshifted field.

lemma weighted_exp_log_sum_le {A B : ℝ} (hA : 0 < A) (hB : 0 < B)
    {p : ℝ} (hp : 1 ≤ p) (x : ℝ) :
    Real.exp (p * Real.log ((A * Real.exp x + B * Real.exp (-x)) / (A + B))) ≤
      (A / (A + B)) * Real.exp (p * x) +
        (B / (A + B)) * Real.exp (-p * x) := by
…

lemma OAI.InvariantIsing.fieldMajorant_increment_eq line 107

lemma OAI.InvariantIsing.fieldMajorant_increment_exp_le line 120

Source documentation

The sharp Gaussian exponential-moment bound in the branch a ≥ d.

lemma fieldMajorant_increment_exp_le {d a : ℝ} (hd : 0 < d) (hda : d ≤ a)
    (z q : ℝ) :
    Real.exp (a * (fieldMajorant d (z + q) - fieldMajorant d z)) ≤
      (Real.exp (d * z) / (Real.exp (d * z) + Real.exp (-d * z))) * Real.exp (a * q) +
      (Real.exp (-d * z) / (Real.exp (d * z) + Real.exp (-d * z))) * Real.exp (-a * q) := by
…

Mentions: OAI.InvariantIsing.fieldMajorant

lemma OAI.InvariantIsing.integrable_exp_fieldMajorant line 133
Source documentation
Exponential integrability of every shifted majorant, needed throughout the finite backward recursion.
```
lemma integrable_exp_fieldMajorant {d : ℝ} (hd : 0 < d) (z s a : ℝ) :
    Integrable (fun y : ℝ => Real.exp (a * fieldMajorant d (z + s * y)))
      (gaussianReal 0 1) :=
…
```
Mentions: OAI.InvariantIsing.fieldMajorant