FieldCapEstimate.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The rough field cap estimate used in the finite-dimensional upper comparison.

def OAI.InvariantIsing.fieldPartitionConstant line 14
Source documentation
The finite constant coming from the positive exponents of a fixed trial partition.
```
def fieldPartitionConstant (h : FieldStep) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
def OAI.InvariantIsing.gaussianAbsoluteMean line 17
lemma OAI.InvariantIsing.gaussianAbsoluteMean_nonneg line 19
lemma OAI.InvariantIsing.gaussianOperator_fold_abs line 22
lemma OAI.InvariantIsing.gaussianOperator_zero_abs line 55
lemma OAI.InvariantIsing.fieldValue_abs_sum line 60
lemma OAI.InvariantIsing.fieldValue_cap_estimate line 99
Source documentation
The field value has a linear negative cost in its integrated height and only a square-root positive cost at the root. This is sufficient to make the upper-comparison field cap inactive for a fixed trial partition.
```
lemma fieldValue_cap_estimate (h : FieldStep) :
    fieldValue h 0 ≤ -(∫ s, fieldFunction h s ∂pathMeasure) / 2 +
      Real.sqrt (h.height 0) * gaussianAbsoluteMean + fieldPartitionConstant h := by
…
```
Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldValue, OAI.InvariantIsing.fieldFunction, OAI.InvariantIsing.gaussianAbsoluteMean, OAI.InvariantIsing.fieldPartitionConstant
lemma OAI.InvariantIsing.integral_fieldFunction_ge_last line 124

lemma OAI.InvariantIsing.fieldValue_add_pairing_cap line 138

Source documentation

With a trial uniformly below one, the negative last-height term dominates all fields on that fixed partition.

lemma fieldValue_add_pairing_cap (p : OverlapPath) {d : ℝ} (hd : 0 ≤ d)
    (hp : ∀ᵐ s ∂pathMeasure, p s ≤ 1 - d) (h : FieldStep) :
    fieldValue h 0 + fieldPairing p h / 2 ≤
      -(d * (1 - h.cut (Fin.last h.depth).castSucc) / 2) *
          h.height (Fin.last h.depth) +
        gaussianAbsoluteMean * Real.sqrt (h.height (Fin.last h.depth)) +
        fieldPartitionConstant h := by
…

Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldValue, OAI.InvariantIsing.fieldPairing, OAI.InvariantIsing.gaussianAbsoluteMean, OAI.InvariantIsing.fieldPartitionConstant

lemma OAI.InvariantIsing.exists_linear_sqrt_cap line 155

Source documentation

The elementary square-root-versus-linear estimate needed to choose the field cap.

lemma exists_linear_sqrt_cap {e : ℝ} (he : 0 < e) (C K B : ℝ) :
    ∃ H : ℝ, 0 < H ∧ ∀ x : ℝ, H ≤ x → -e * x + C * Real.sqrt x + K ≤ B := by
…