OAI/Probability/InvariantIsing/Arrays/NSpinTensorGaussianLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorNodeTag line 15
2. lemma OAI.InvariantIsing.tensorNodeTag_injective line 20
3. lemma OAI.InvariantIsing.tensorNodeTag_nodeAt line 29
4. def OAI.InvariantIsing.tensorStandardGaussianNodes line 36
5. lemma OAI.InvariantIsing.measurable_tensorStandardGaussianNodes line 41
6. theorem OAI.InvariantIsing.tensorStandardGaussianNodes_law line 46
7. theorem OAI.InvariantIsing.tensorMarkScale_measurePreserving line 60
8. def OAI.InvariantIsing.tensorGaussianNodes line 77
9. lemma OAI.InvariantIsing.measurable_tensorGaussianNodes line 82
10. theorem OAI.InvariantIsing.tensorGaussianNodes_measurePreserving line 88
11. theorem OAI.InvariantIsing.tensorGaussianRootForest_measurePreserving line 114

    Source documentation

    The root and all forest coordinates have their independent prescribed Gaussian laws, including zero variances.

    theorem tensorGaussianRootForest_measurePreserving {N m k : ℕ}
        (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ)
        (n : ℕ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0) :
        MeasurePreserving (fun g => (tensorGaussianNodes I degree n v g none,
          fun w => tensorGaussianNodes I degree n v g (some w))) gaussianCoordinates
          ((tensorGaussianLaw I degree (v 0) : Measure (SpinTensorIndex I degree → ℝ)).prod
            (Measure.infinitePi (fun w : ForestVertex n =>
              (tensorGaussianLaw I degree (v (forestVertexDepth n w + 1)) :
                Measure (SpinTensorIndex I degree → ℝ))))) := by
    …

    Mentions: OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorGaussianNodes, OAI.InvariantIsing.tensorGaussianLaw

12. lemma OAI.InvariantIsing.cylinderField_tensorLeaf_nodes line 144
13. def OAI.InvariantIsing.tensorFlatToCoordinates line 168
14. theorem OAI.InvariantIsing.tensorFlatToCoordinates_measurePreserving line 175
15. def OAI.InvariantIsing.tensorFlatToLabeled line 194
16. theorem OAI.InvariantIsing.tensorFlatToLabeled_measurePreserving line 203

    Source documentation

    The flat Gaussian spin/leaf model is exactly the independent Gaussian root and tensor-energy forest model used by the cascade recursion.

    theorem tensorFlatToLabeled_measurePreserving {N m k : ℕ} (U : Rotation N)
        (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
        (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0) :
        MeasurePreserving (tensorFlatToLabeled U I degree amplitude n v)
          ((labeledCascadeLaw n b : Measure (LabeledTree n)).prod gaussianCoordinates)
          ((tensorGaussianLaw I degree (v 0) : Measure (SpinTensorIndex I degree → ℝ)).prod
            (tensorLabeledLaw U I degree amplitude n b (fun i => v (i + 1)))) := by
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorFlatToLabeled, OAI.InvariantIsing.tensorGaussianLaw, OAI.InvariantIsing.tensorLabeledLaw

17. theorem OAI.InvariantIsing.tensorLabeledEnergy_flat_eq line 217