FieldScalarSampling.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Common-prefix sampling of two scalar Ising spins. After the split the two tails are independent; before the split they use the same actual tilted Gaussian transition.

def OAI.InvariantIsing.fieldPairSpinKernel line 16
instance OAI.InvariantIsing.fieldPairSpinKernel_markov line 27
theorem OAI.InvariantIsing.fieldPairSpinKernel_mean line 42
def OAI.InvariantIsing.fieldLevelSpinPair line 67
Source documentation
The field's root is shared by the two replicas.
```
def fieldLevelSpinPair (h : FieldStep) (i : Fin (h.depth + 1)) : Measure (Bool × Bool) :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
instance OAI.InvariantIsing.fieldLevelSpinPair_probability line 72
theorem OAI.InvariantIsing.fieldLevelSpinPair_mean line 77
theorem OAI.InvariantIsing.fieldLevelSpinPair_test line 86
Source documentation
The common-level spin test in the evaluated cavity law.
```
theorem fieldLevelSpinPair_test (h : FieldStep) (q : OverlapPath) (Φ : ℝ → ℝ) :
    (∫ s, ∫ σ, Φ (q s) * (spinValue σ.1 * spinValue σ.2)
      ∂fieldLevelSpinPair h (fieldLevelIndex h s) ∂pathMeasure) =
      ∫ s, Φ (q s) * fieldMagnetizationPath h s ∂pathMeasure := by
…
```
Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.spinValue, OAI.InvariantIsing.fieldLevelSpinPair, OAI.InvariantIsing.fieldLevelIndex, OAI.InvariantIsing.fieldMagnetizationPath
theorem OAI.InvariantIsing.fieldLevelSpinPair_level_test line 96
Source documentation
Sampling the spin pair leaves every common-level observable unchanged.
```
theorem fieldLevelSpinPair_level_test (h : FieldStep) (q : OverlapPath) (Φ : ℝ → ℝ) :
    (∫ s, ∫ _σ, Φ (q s) ∂fieldLevelSpinPair h (fieldLevelIndex h s) ∂pathMeasure) =
      ∫ s, Φ (q s) ∂pathMeasure := by
…
```
Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.fieldLevelSpinPair, OAI.InvariantIsing.fieldLevelIndex