OAI/Probability/InvariantIsing/Fields/FieldMajorantFold.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.gaussianOperator_mono line 14
2. lemma OAI.InvariantIsing.linearGrowth_const_add line 42
3. lemma OAI.InvariantIsing.gaussianOperator_const_add line 48
4. lemma OAI.InvariantIsing.gaussianOperator_positive_growth line 54
5. lemma OAI.InvariantIsing.gaussianOperator_fold_growth line 62
6. lemma OAI.InvariantIsing.gaussianOperator_fold_majorant line 75

   Source documentation

   Only positive exponents occur in the non-root part of the recursion.

   lemma gaussianOperator_fold_majorant (L : List (ℝ × ℝ))
       (hL : ∀ av ∈ L, 0 < av.1 ∧ 0 ≤ av.2) {d : ℝ} (hd : 0 < d)
       (hd1 : d ≤ 1) (z : ℝ) :
       (L.foldr (fun av f => gaussianOperator av.1 av.2 f)
         (fun x => Real.log (Real.cosh x))) z ≤ fieldMajorant d z +
           (L.map (fun av => max av.1 d * av.2 / 2)).sum := by
   …

   Mentions: OAI.InvariantIsing.gaussianOperator, OAI.InvariantIsing.fieldMajorant

7. lemma OAI.InvariantIsing.fieldIncrement_nonneg line 105
8. lemma OAI.InvariantIsing.fieldIncrement_tail_positive line 115
9. lemma OAI.InvariantIsing.fieldValue_majorant_sum line 125

   Source documentation

   Iteration through the actual finite field, with the initial zero exponent handled by ordinary Gaussian expectation.

   lemma fieldValue_majorant_sum (h : FieldStep) {d : ℝ} (hd : 0 < d) (hd1 : d ≤ 1)
       (z : ℝ) :
       fieldValue h z ≤ fieldMajorant d z +
         ((List.ofFn (fieldIncrement h)).map (fun av => max av.1 d * av.2 / 2)).sum -
           h.height (Fin.last h.depth) / 2 := by
   …

   Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldValue, OAI.InvariantIsing.fieldMajorant, OAI.InvariantIsing.fieldIncrement