OAI/Probability/InvariantIsing/Arrays/NSpinTensorPairConditioning.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.spinLeafTerminal line 14
2. lemma OAI.InvariantIsing.exp_spinLeafTerminal line 17
3. lemma OAI.InvariantIsing.spinLeafPartition_eq line 22
4. lemma OAI.InvariantIsing.spinLeafTerminal_exp_integrable line 32
5. lemma OAI.InvariantIsing.spinLeafGibbs_singleton line 40
6. def OAI.InvariantIsing.spinLeafPairResidualKernel line 71
7. instance OAI.InvariantIsing.spinLeafPairResidualKernel_markov line 77
8. def OAI.InvariantIsing.spinLeafPairJoin line 81
9. lemma OAI.InvariantIsing.measurable_spinLeafPairJoin line 85
10. theorem OAI.InvariantIsing.spinLeafPairLaw line 92

    Source documentation

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

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

    Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.uniformSpinPrior, OAI.InvariantIsing.spinLeafTerminal, OAI.InvariantIsing.spinLeafPairResidualKernel, OAI.InvariantIsing.spinLeafPairJoin

11. theorem OAI.InvariantIsing.spinLeafPair_conditioning line 129
12. def OAI.InvariantIsing.tensorLeafSpinHamiltonian line 156
13. lemma OAI.InvariantIsing.tensorLeafSpinHamiltonian_eq_coordinates line 164
14. theorem OAI.InvariantIsing.tensorLeafSpin_exp_integrable_ae line 187
15. lemma OAI.InvariantIsing.spinLeafTerminal_tensorLeafSpinHamiltonian line 201
16. theorem OAI.InvariantIsing.tensorLeafSpinPair_conditioning line 212

    Source documentation

    Actual finite tensor Hamiltonian version of conditional spin sampling.

    theorem tensorLeafSpinPair_conditioning {N m k : ℕ}
        (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
        (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
        (n : ℕ) (z : SpinTensorIndex I degree → ℝ) (p : TensorCoordinateData I degree n)
        (he : Integrable (fun s => Real.exp (tensorLeafSpinHamiltonian eig U c I degree amplitude n z p s))
          ((uniformSpinPrior N : Measure (Spin N)).prod (labeledLeafLaw n p.1)))
        (D : (Fin 2 → Spin N × LabeledLeaf n) → ℝ)
        (hD : ∃ C : ℝ, ∀ x, |D x| ≤ C) :
        referenceReplicaMean ((uniformSpinPrior N : Measure (Spin N)).prod (labeledLeafLaw n p.1))
          (tensorLeafSpinHamiltonian eig U c I degree amplitude n z p) D =
          referenceReplicaMean (labeledLeafLaw n p.1)
            (fun α => spinTensorTerminal eig U c I degree amplitude
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.TensorCoordinateData, OAI.InvariantIsing.tensorLeafSpinHamiltonian, OAI.InvariantIsing.uniformSpinPrior, OAI.InvariantIsing.Spin, OAI.InvariantIsing.spinTensorTerminal

17. theorem OAI.InvariantIsing.tensorLeafSpinPair_conditioning_ae line 237

    Source documentation

    The actual Gaussian/cascade disorder satisfies the conditional pair factorization almost surely, on one event for every bounded pair test.

    theorem tensorLeafSpinPair_conditioning_ae {N m k : ℕ} (hN : 0 < N)
        (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
        (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
        (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
        (hb : CascadeExponents n b) (z : SpinTensorIndex I degree → ℝ) :
        ∀ᵐ p ∂tensorCoordinateLaw I degree n b v,
          ∀ D : (Fin 2 → Spin N × LabeledLeaf n) → ℝ,
            (∃ C : ℝ, ∀ x, |D x| ≤ C) →
            referenceReplicaMean ((uniformSpinPrior N : Measure (Spin N)).prod (labeledLeafLaw n p.1))
              (tensorLeafSpinHamiltonian eig U c I degree amplitude n z p) D =
              referenceReplicaMean (labeledLeafLaw n p.1)
                (fun α => spinTensorTerminal eig U c I degree amplitude
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorCoordinateLaw, OAI.InvariantIsing.Spin, OAI.InvariantIsing.uniformSpinPrior, OAI.InvariantIsing.tensorLeafSpinHamiltonian, OAI.InvariantIsing.spinTensorTerminal