OAI/Probability/InvariantIsing/Fields/FieldSpinSampling.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual spin sampling and Gaussian transitions for the scalar Ising recursion. The transition kernels remain probabilities at zero variance.

  1. def OAI.InvariantIsing.scalarSpinKernel line 16
  2. instance OAI.InvariantIsing.scalarSpinKernel_markov line 24
  3. lemma OAI.InvariantIsing.integral_uniformBool line 31
  4. theorem OAI.InvariantIsing.scalarSpinKernel_mean line 42
  5. def OAI.InvariantIsing.fieldTransitionKernel line 52
  6. instance OAI.InvariantIsing.fieldTransitionKernel_markov line 64
  7. lemma OAI.InvariantIsing.fieldTransitionKernel_eq_tilted line 69
  8. lemma OAI.InvariantIsing.fieldTransitionKernel_integral line 75
  9. def OAI.InvariantIsing.fieldTailSpinKernel line 84

    Source documentation

    Spin law at the end of the actual successive tilted Gaussian transitions, starting from the given scalar field.

    def fieldTailSpinKernel : (L : List (ℝ × ℝ≥0)) →
    (∀ av ∈ L, 0 < av.1) → Kernel ℝ Bool
  | [], _ => scalarSpinKernel
  | av :: L, hL =>
    let ht := fun bv hb => hL bv (List.mem_cons_of_mem av hb)
…

    Mentions: OAI.InvariantIsing.scalarSpinKernel

  10. instance OAI.InvariantIsing.fieldTailSpinKernel_markov line 93
  11. theorem OAI.InvariantIsing.fieldTailSpinKernel_mean line 103