OAI/Probability/InvariantIsing/Fields/FieldSpinEvaluation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual finite vector-spin common-depth test under the published marking input. Both the spin conditioning and exponential integrability are derived for this model.

  1. def OAI.InvariantIsing.fieldVectorSpinPairMean line 15
  2. theorem OAI.InvariantIsing.field_vector_spin_pair_reduce line 26
  3. theorem OAI.InvariantIsing.field_vector_spin_pair_evaluation line 40

    Source documentation

    The finite-cascade identity cav:spin-test, for the scalar field representation, conditional only on the published endpoint marking law.

    theorem field_vector_spin_pair_evaluation (hpub : PanchenkoTalagrandFieldPairInput)
    (N : ℕ) (hN : 0 < N) (h : FieldStep)
    (q : Fin (h.depth + 1) → ℝ) (Φ : ℝ → ℝ) (j : Fin N)
    {C : ℝ} (hΦ : ∀ x, |Φ x| ≤ C) :
    (∫ z, fieldVectorSpinPairMean N h z q Φ j
      ∂(vectorGaussianLaw N (NNReal.mk (h.height 0) (h.nonneg 0)) : Measure (Fin N → ℝ))) =
      ∫ s, Φ (q (fieldLevelIndex h s)) * fieldMagnetizationPath h s ∂pathMeasure := by
…

    Mentions: OAI.InvariantIsing.PanchenkoTalagrandFieldPairInput, OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldVectorSpinPairMean, OAI.InvariantIsing.vectorGaussianLaw, OAI.InvariantIsing.fieldLevelIndex, OAI.InvariantIsing.fieldMagnetizationPath