OAI/Probability/InvariantIsing/Arrays/NSpinTensorRetained.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorCascadeBackward line 15
2. def OAI.InvariantIsing.tensorCascadeStopped line 22
3. def OAI.InvariantIsing.tensorCascadeMultiplier line 27
4. lemma OAI.InvariantIsing.measurable_tensorCascadeBackward line 35
5. lemma OAI.InvariantIsing.measurable_tensorCascadeStopped line 44
6. lemma OAI.InvariantIsing.measurable_tensorCascadeMultiplier line 49
7. lemma OAI.InvariantIsing.tensorCascadeMultiplier_pos line 58
8. lemma OAI.InvariantIsing.tensorCascadeMultiplier_moment line 67

   Source documentation

   Each transition is normalized at its own cascade exponent, for every ancestor state. The terminal is the actual finite Ising log partition.

   lemma tensorCascadeMultiplier_moment {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) (i : ℕ) (z : SpinTensorIndex I degree → ℝ) :
       (∫⁻ a, ENNReal.ofReal (tensorCascadeMultiplier eig U c I degree amplitude n b v i (z, a) ^ b i)
         ∂(tensorGaussianLaw I degree (v i) : Measure (SpinTensorIndex I degree → ℝ))) = 1 := by
   …

   Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorCascadeMultiplier, OAI.InvariantIsing.tensorGaussianLaw

9. lemma OAI.InvariantIsing.measurable_tensorAncestorMarkMeasure line 83
10. def OAI.InvariantIsing.tensorAncestorMarkKernel line 98

    Source documentation

    The ancestor-dependent mark transition, with density c_i(z,a)^b_i.

    def tensorAncestorMarkKernel {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 : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0) (i : ℕ) :
        Kernel (SpinTensorIndex I degree → ℝ) (SpinTensorIndex I degree → ℝ) :=
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex

11. theorem OAI.InvariantIsing.tensorAncestorMarkKernel_markov line 106
12. lemma OAI.InvariantIsing.tensorAncestorMarkKernel_density line 119
13. def OAI.InvariantIsing.tensorRetainedCascade line 135
14. lemma OAI.InvariantIsing.measurable_tensorRetainedCascade line 143
15. theorem OAI.InvariantIsing.tensorRetainedCascade_forget_law line 154

    Source documentation

    Forgetting the retained marks gives exactly the original raw cascade law.

    theorem tensorRetainedCascade_forget_law {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 → ℝ) :
        (tensorCascadeLaw I degree n b v).map
          (fun T => noiseTreeForget (SpinTensorIndex I degree → ℝ) n
            (tensorRetainedCascade eig U c I degree amplitude n b v z T)) = rawCascadeLaw n b := by
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorCascadeLaw, OAI.InvariantIsing.tensorRetainedCascade

16. theorem OAI.InvariantIsing.tensorRetainedCascade_law_succ line 180

    Source documentation

    The retained tree has the actual ancestor-dependent root mark kernel. The descendant is transformed at the updated ancestor state; it is not replaced by an independent level tilt.

    theorem tensorRetainedCascade_law_succ {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 + 1) b) (z : SpinTensorIndex I degree → ℝ) :
        letI := tensorAncestorMarkKernel_markov hN eig U c I degree amplitude (n + 1) b v hb 0
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorAncestorMarkKernel_markov

17. lemma OAI.InvariantIsing.tensorLeafTerminal_last line 217
18. def OAI.InvariantIsing.tensorTerminalLeafLaw line 233
19. lemma OAI.InvariantIsing.tensorTerminalLeafLaw_eq_backward line 242
20. theorem OAI.InvariantIsing.tensorTerminalLeafLaw_keep_ae line 265

    Source documentation

    Sampling after the actual terminal tilt is transported to ordinary sampling from the retained marked tree, with every mark kept.

    theorem tensorTerminalLeafLaw_keep_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 → ℝ) :
        ∀ᵐ T ∂tensorCascadeLaw I degree n b v,
          (tensorTerminalLeafLaw eig U c I degree amplitude n z T).map
            (noiseLeafKeep n (tensorCascadeMultiplier eig U c I degree amplitude n b v)
              (tensorCascadeStopped I degree n) z) =
            noiseLeafKernel (SpinTensorIndex I degree → ℝ) n
              (tensorRetainedCascade eig U c I degree amplitude n b v z T) := by
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorCascadeLaw, OAI.InvariantIsing.tensorTerminalLeafLaw, OAI.InvariantIsing.tensorCascadeMultiplier, OAI.InvariantIsing.tensorCascadeStopped, OAI.InvariantIsing.tensorRetainedCascade