RestrictedFieldPublishedInput.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Panchenko--Talagrand (2007), Lemma 3.1 (8), p.655 and Corollary 3.2 (9), p.656, specialized to the actual finite constrained terminal. The hypothesis concerns only the marked endpoint law; no pressure, spin expectation, or limiting assertion is an input.

def OAI.InvariantIsing.restrictedFieldTiltedPairMean line 17
def OAI.InvariantIsing.RestrictedFieldAncestorPairLaw line 27
def OAI.InvariantIsing.PanchenkoTalagrandRestrictedFieldPairInput line 43
Source documentation
The same published marking theorem, with a nonempty finite spin constraint retained inside the terminal log partition.
```
def PanchenkoTalagrandRestrictedFieldPairInput : Prop :=
…
```

theorem OAI.InvariantIsing.restrictedFieldFinitePath_exp_integrable line 49

Source documentation

The constrained terminal satisfies the published exponential-moment condition on every finite Gaussian path, also for zero variances.

theorem restrictedFieldFinitePath_exp_integrable {N : ℕ} (hN : 0 < N)
    (S : Finset (Spin N)) (hS : S.Nonempty)
    (n : ℕ) (v : ℕ → ℝ≥0) (z : Fin N → ℝ) :
    Integrable (fun w : Fin n → Fin N → ℝ =>
      Real.exp (restrictedFieldTerminal S (z + ∑ i, w i)))
      (Measure.pi (fun i : Fin n => (vectorGaussianLaw N (v i) : Measure (Fin N → ℝ)))) := by
…

Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.restrictedFieldTerminal, OAI.InvariantIsing.vectorGaussianLaw