OAI/Probability/InvariantIsing/Fields/FieldRadialBackward.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The terminal scale comparison propagated through the actual finite one-site Gaussian recursion.

  1. lemma OAI.InvariantIsing.gaussianOperator_fold_even line 15
  2. lemma OAI.InvariantIsing.gaussianOperator_fold_difference_monotone line 28
  3. theorem OAI.InvariantIsing.field_radial_backward_difference_monotone line 50

    Source documentation

    The exact scaled Ising terminal used in the radial covariance argument.

    theorem field_radial_backward_difference_monotone (L : List (ℝ × ℝ))
    (hL : ∀ av ∈ L, 0 < av.1 ∧ 0 ≤ av.2) {a b : ℝ}
    (ha : 0 ≤ a) (hab : a ≤ b) :
    MonotoneOn (fun z =>
      (L.foldr (fun av f => gaussianOperator av.1 av.2 f)
        (fun u => Real.log (Real.cosh (b * u)))) z -
      (L.foldr (fun av f => gaussianOperator av.1 av.2 f)
        (fun u => Real.log (Real.cosh (a * u)))) z) (Ici 0) := by
…

    Mentions: OAI.InvariantIsing.gaussianOperator