OAI/Probability/InvariantIsing/Fields/FieldPublishedPairInput.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite vector log-cosh specialization of Panchenko--Talagrand, C. R. Acad. Sci. Paris I 345 (2007), 653--656, Section 3, Lemma 3.1, equation (8), p.655, and Corollary 3.2, equation (9), p.656.

Only bounded measurable tests of the common depth and two endpoint fields are retained. The statement specifies their law under the actual terminal tilt, before any spins or overlap expectations are evaluated. The finite marking theorem supplies this hypothesis.

  1. def OAI.InvariantIsing.fieldStepVariance line 23
  2. def OAI.InvariantIsing.fieldVectorCoordinateLaw line 28
  3. def OAI.InvariantIsing.fieldVectorEndpoint line 35
  4. def OAI.InvariantIsing.fieldVectorTiltedPairMean line 40
  5. def OAI.InvariantIsing.FieldVectorAncestorPairLaw line 49
  6. def OAI.InvariantIsing.PanchenkoTalagrandFieldPairInput line 64

    Source documentation

    Same published marking result as PanchenkoTalagrandTensorPairInput, specialized to the separable vector terminal used after the cavity change of variables. No pressure, spin-moment, or limiting assertion is assumed.

    def PanchenkoTalagrandFieldPairInput : Prop :=
…
  7. lemma OAI.InvariantIsing.fieldVectorTerminal_linearGrowth line 67
  8. theorem OAI.InvariantIsing.fieldVectorFinitePath_exp_integrable line 83

    Source documentation

    The actual terminal meets the published theorem's exponential moment condition on every finite Gaussian path, including degenerate increments.

    theorem fieldVectorFinitePath_exp_integrable (N : ℕ) (hN : 0 < N)
    (n : ℕ) (v : ℕ → ℝ≥0) (z : Fin N → ℝ) :
    Integrable (fun w : Fin n → Fin N → ℝ =>
      Real.exp (∑ j, Real.log (Real.cosh ((z + ∑ i, w i) j))))
      (Measure.pi (fun i : Fin n => (vectorGaussianLaw N (v i) : Measure (Fin N → ℝ)))) := by
…

    Mentions: OAI.InvariantIsing.vectorGaussianLaw