NSpinTensorFrozen.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

A selected actual spectral/tree monomial as an independent Gaussian factor.

abbrev OAI.InvariantIsing.TensorGaussianKey line 17
def OAI.InvariantIsing.tensorNamespaceTag line 22
Source documentation
Namespace zero contains the linear field; namespace j+1 contains precisely the jth spectral tensor at all ancestor levels.
```
def tensorNamespaceTag {N m k : ℕ} (I : Fin m → Finset (Fin N))
    (degree : Fin k → Fin m → ℕ) (q : TensorGaussianKey I degree) : ℕ :=
…
```
Mentions: OAI.InvariantIsing.TensorGaussianKey
lemma OAI.InvariantIsing.tensorNamespaceTag_injective line 28
def OAI.InvariantIsing.tensorNamespacedCoefficients line 56

theorem OAI.InvariantIsing.tensorNamespacedFields_law line 66

Source documentation

Injective Gaussian reindexing identifies the entire countable spin/leaf field law with the flat tensor model.

theorem tensorNamespacedFields_law {N m k : ℕ} (U : Rotation N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (v : Fin (n + 1) → SpinTensorIndex I degree → ℝ≥0) :
    gaussianCoordinates.map (fun g x => cylinderField (tensorLeafCoefficients U I degree amplitude n v x) g) =
      gaussianCoordinates.map (fun g x => cylinderField (tensorNamespacedCoefficients U I degree amplitude n v x) g) := by
…

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

lemma OAI.InvariantIsing.sqrt_varianceIncrement line 97
def OAI.InvariantIsing.tensorLinearCoefficients line 102

theorem OAI.InvariantIsing.tensorNamespacedField_expand line 108

Source documentation

The reindexed field is exactly the sum of the linear enrichment and the displayed independent spectral/tree Gaussian monomials.

theorem tensorNamespacedField_expand {N m k : ℕ} (U : Rotation N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
    (x : Spin N × LabeledLeaf n) (g : ℕ → ℝ) :
    cylinderField (tensorNamespacedCoefficients U I degree amplitude n
      (fun i => tensorPathProfile I degree n treeDegree h i) x) g =
      cylinderField (tensorLinearCoefficients n h x) (fun i => g (Nat.pair 0 i)) +
        ∑ j, amplitude j * cylinderField
          (jointSpectralMonomialCoefficients U I (degree j) n (treeDegree j) x)
          (fun i => g (Nat.pair (j + 1) i)) := by
…

Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorNamespacedCoefficients, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.tensorLinearCoefficients, OAI.InvariantIsing.jointSpectralMonomialCoefficients

lemma OAI.InvariantIsing.tensorNamespacedField_frozen line 140

theorem OAI.InvariantIsing.tensorNamespacedField_insert line 172

Source documentation

Inserting the selected standard Gaussian family adds exactly its actual amplitude times jointSpectralMonomialCoefficients.

theorem tensorNamespacedField_insert {N m k : ℕ} (U : Rotation N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
    (j : Fin k) (x : Spin N × LabeledLeaf n) (z : ℕ → ℝ) (g : OtherNamespaces (j + 1)) :
    cylinderField (tensorNamespacedCoefficients U I degree amplitude n
      (fun i => tensorPathProfile I degree n treeDegree h i) x)
      (gaussianNamespaceJoin (j + 1) (z, g)) =
    cylinderField (tensorNamespacedCoefficients U I degree (Function.update amplitude j 0) n
      (fun i => tensorPathProfile I degree n treeDegree h i) x)
      (gaussianNamespaceJoin (j + 1) (0, g)) +
        amplitude j * cylinderField (jointSpectralMonomialCoefficients U I (degree j) n (treeDegree j) x) z := by
…

lemma OAI.InvariantIsing.measurable_tensorNamespacedFields_joint line 204

theorem OAI.InvariantIsing.tensorNamespacedGibbs_law line 218

Source documentation

The full finite-volume Gibbs-law distribution is preserved by the Gaussian namespace reindexing, for each actual rotation and cascade prior.

theorem tensorNamespacedGibbs_law {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 : ℕ) (v : Fin (n + 1) → SpinTensorIndex I degree → ℝ≥0) (T : LabeledTree n) :
    let ν := labeledSpinReference n (uniformSpinPrior N : Measure (Spin N)) T
…

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

abbrev OAI.InvariantIsing.TensorFrozenData line 248
def OAI.InvariantIsing.tensorFrozenLaw line 250
instance OAI.InvariantIsing.tensorFrozenLaw_probability line 254
def OAI.InvariantIsing.tensorFrozenBaseEnergy line 259
def OAI.InvariantIsing.tensorFrozenReference line 268
instance OAI.InvariantIsing.tensorFrozenReference_probability line 275
lemma OAI.InvariantIsing.measurable_tensorFrozenBaseEnergy line 281
lemma OAI.InvariantIsing.measurable_tensorFrozenReference line 315
theorem OAI.InvariantIsing.tensorFrozenEnergy_insert line 329

theorem OAI.InvariantIsing.tensorFrozenInsertion_measurePreserving line 345

Source documentation

The selected field is a genuinely independent Gaussian product factor; all remaining marks, the rotation, and the tree form external disorder.

theorem tensorFrozenInsertion_measurePreserving {N : ℕ} (μ : Measure (SpecialOrthogonal N))
    [IsProbabilityMeasure μ] (n : ℕ) (b : ℕ → ℝ) (j : ℕ) :
    MeasurePreserving (fun p : TensorFrozenData N n j × (ℕ → ℝ) =>
      (p.1.1, gaussianNamespaceJoin (j + 1) (p.2, p.1.2)))
      ((tensorFrozenLaw μ n b j).prod gaussianCoordinates)
      ((μ.prod (labeledCascadeLaw n b : Measure (LabeledTree n))).prod gaussianCoordinates) :=
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.TensorFrozenData, OAI.InvariantIsing.tensorFrozenLaw