OAI/Probability/InvariantIsing/Arrays/NSpinTensorFlatLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorFlatToNoise line 15
2. theorem OAI.InvariantIsing.tensorFlatToNoise_measurePreserving line 23
3. lemma OAI.InvariantIsing.spinTensorEnergy_labeled line 43
4. lemma OAI.InvariantIsing.tensorCoordinateLog_eq_terminal line 57
5. theorem OAI.InvariantIsing.tensorCoordinateLog_eq_noise line 91

   Source documentation

   On every good marked tree the coordinate partition is exactly the actual marked-cascade partition, uniformly in its rotation and root mark.

   theorem tensorCoordinateLog_eq_noise {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 → ℝ) (q : TensorCoordinateData I degree n)
       (hg : GoodNoiseTree (SpinTensorIndex I degree → ℝ) n
         (labeledNoiseJoin (SpinTensorIndex I degree → ℝ) n
           (q.1, markForestOfCoords (SpinTensorIndex I degree → ℝ) n q.2)))
       (ht : 0 < noiseTreeTotal (SpinTensorIndex I degree → ℝ) n
           (labeledNoiseJoin (SpinTensorIndex I degree → ℝ) n
             (q.1, markForestOfCoords (SpinTensorIndex I degree → ℝ) n q.2)) ∧
         noiseTreeTotal (SpinTensorIndex I degree → ℝ) n
           (labeledNoiseJoin (SpinTensorIndex I degree → ℝ) n
   …

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

6. theorem OAI.InvariantIsing.tensorFlatLog_eq_noise_ae line 122

   Source documentation

   The good-tree event is independent of the terminal energy, so this identity holds simultaneously for every rotation on one full-measure set.

   theorem tensorFlatLog_eq_noise_ae {N m k : ℕ} (eig 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) :
       ∀ᵐ p : LabeledTree n × (ℕ → ℝ)
         ∂(labeledCascadeLaw n b : Measure (LabeledTree n)).prod gaussianCoordinates,
         ∀ U : Rotation N, tensorFlatLog eig U c I degree amplitude n v p =
           tensorCascadeLog eig U c I degree amplitude n (tensorFlatToNoise I degree n v p).1
             (tensorFlatToNoise I degree n v p).2 := by
   …

   Mentions: OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.tensorFlatLog, OAI.InvariantIsing.tensorCascadeLog, OAI.InvariantIsing.tensorFlatToNoise

7. def OAI.InvariantIsing.tensorFlatToDisorder line 162
8. theorem OAI.InvariantIsing.tensorFlatToDisorder_measurePreserving line 168
9. theorem OAI.InvariantIsing.tensorFlatPressure_eq_disorder_ae line 183

   Source documentation

   Exact almost-everywhere pressure identification with the actual three-disorder model, suitable for transporting moments and variance.

   theorem tensorFlatPressure_eq_disorder_ae {N m k : ℕ}
       (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig 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) :
       (fun p : (SpecialOrthogonal N × LabeledTree n) × (ℕ → ℝ) =>
         (N : ℝ)⁻¹ * tensorFlatLog eig (specialRotation p.1.1) c I degree amplitude n v (p.1.2, p.2)) =ᵐ[
         (μ.prod (labeledCascadeLaw n b : Measure (LabeledTree n))).prod gaussianCoordinates]
       (tensorDisorderPressure eig c I degree amplitude n ∘ tensorFlatToDisorder I degree n v) := by
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorFlatLog, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.tensorDisorderPressure, OAI.InvariantIsing.tensorFlatToDisorder