OAI/Probability/InvariantIsing/Fields/PriorSpinLeafConditioning.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Conditional independent spin sampling for a finite constrained prior. The prior is retained in both its terminal and its conditional spin kernels.

  1. def OAI.InvariantIsing.priorSpinLeafTerminal line 15
  2. lemma OAI.InvariantIsing.exp_priorSpinLeafTerminal line 18
  3. lemma OAI.InvariantIsing.priorSpinLeafPartition_eq line 23
  4. lemma OAI.InvariantIsing.priorSpinLeafTerminal_exp_integrable line 33
  5. lemma OAI.InvariantIsing.priorSpinLeafGibbs_singleton line 41
  6. def OAI.InvariantIsing.priorSpinLeafPairResidualKernel line 72
  7. instance OAI.InvariantIsing.priorSpinLeafPairResidualKernel_markov line 78
  8. def OAI.InvariantIsing.priorSpinLeafPairJoin line 82
  9. lemma OAI.InvariantIsing.measurable_priorSpinLeafPairJoin line 86
  10. theorem OAI.InvariantIsing.priorSpinLeafPairLaw line 93

    Source documentation

    Conditional on the two leaf labels, the spin residual draws are independent, including when the leaf labels coincide.

    theorem priorSpinLeafPairLaw {N n : ℕ} (μ : Measure (Spin N)) [IsProbabilityMeasure μ] (ν : Measure (LabeledLeaf n)) [IsProbabilityMeasure ν]
    (H : Spin N × LabeledLeaf n → ℝ)
    (he : Integrable (fun x => Real.exp (H x)) (μ.prod ν)) :
    ((Measure.pi (fun _ : Fin 2 => gibbsProbability ν (priorSpinLeafTerminal μ H))) ⊗ₘ
      priorSpinLeafPairResidualKernel μ H).map priorSpinLeafPairJoin =
      Measure.pi (fun _ : Fin 2 => gibbsProbability (μ.prod ν) H) := by
…

    Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.priorSpinLeafTerminal, OAI.InvariantIsing.priorSpinLeafPairResidualKernel, OAI.InvariantIsing.priorSpinLeafPairJoin

  11. theorem OAI.InvariantIsing.priorSpinLeafPair_conditioning line 130