OAI/Probability/InvariantIsing/Arrays/NSpinTensorFrozenCGF.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.tensorNamespacedCoefficients_variance_eq line 15
2. lemma OAI.InvariantIsing.tensorNamespacedPath_variance_le line 28
3. lemma OAI.InvariantIsing.measurable_tensorBaseEnergy line 38
4. lemma OAI.InvariantIsing.tensorBase_exp_integrable line 49
5. lemma OAI.InvariantIsing.measurable_namespacedPathField line 58
6. lemma OAI.InvariantIsing.measurable_frozenSelectedField line 75
7. theorem OAI.InvariantIsing.tensorNamespaced_exp_integrable_ae line 92

   Source documentation

   Exponentials of the tensor Hamiltonian are integrable for almost every joint rotation/tree/Gaussian disorder. No concentration or limiting-pressure hypothesis is used.

   theorem tensorNamespaced_exp_integrable_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 : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0) :
       ∀ᵐ p : (SpecialOrthogonal N × LabeledTree n) × (ℕ → ℝ)
         ∂(μ.prod (labeledCascadeLaw n b : Measure (LabeledTree n))).prod gaussianCoordinates,
         Integrable (fun x : Spin N × LabeledLeaf n => Real.exp
           (rotatedEnergy eig (specialRotation p.1.1) x.1 + fieldEnergy c x.1 +
             cylinderField (tensorNamespacedCoefficients (specialRotation p.1.1) I degree amplitude n
               (fun i => tensorPathProfile I degree n treeDegree h i) x) p.2))
           (labeledSpinReference n (uniformSpinPrior N : Measure (Spin N)) p.1.2) := by
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.rotatedEnergy, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.fieldEnergy, OAI.InvariantIsing.tensorNamespacedCoefficients, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.uniformSpinPrior

8. theorem OAI.InvariantIsing.tensorFrozenBase_exp_integrable_ae line 132

   Source documentation

   The frozen base energy is the actual Hamiltonian with the selected amplitude set to zero, and is exponentially integrable almost surely.

   theorem tensorFrozenBase_exp_integrable_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 : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
       (j : Fin k) :
       ∀ᵐ ω : TensorFrozenData N n j ∂tensorFrozenLaw μ n b j,
         Integrable (fun x => Real.exp (tensorFrozenBaseEnergy eig c I degree amplitude n treeDegree h j ω x))
           (labeledSpinReference n (uniformSpinPrior N : Measure (Spin N)) ω.1.2) := by
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.TensorFrozenData, OAI.InvariantIsing.tensorFrozenLaw, OAI.InvariantIsing.tensorFrozenBaseEnergy, OAI.InvariantIsing.uniformSpinPrior, OAI.InvariantIsing.Spin

9. def OAI.InvariantIsing.tensorNamespacedLog line 159
10. def OAI.InvariantIsing.tensorFrozenPartitionLog line 169
11. def OAI.InvariantIsing.tensorFrozenCGF line 176
12. lemma OAI.InvariantIsing.measurable_tensorFrozenCGF line 184
13. theorem OAI.InvariantIsing.tensorFrozenCGF_memLp_two line 200

    Source documentation

    The selected-field CGF is an actual square-integrable observable on the frozen external disorder and independent Gaussian factor.

    theorem tensorFrozenCGF_memLp_two {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 : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (j : Fin k) (t : ℝ) :
        MemLp (tensorFrozenCGF eig c I degree amplitude n treeDegree h j t) 2
          ((tensorFrozenLaw μ n b j).prod gaussianCoordinates) := by
    …

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

14. theorem OAI.InvariantIsing.tensorFrozenCGF_eq_log_difference line 221

    Source documentation

    The CGF is exactly the difference of the actual log partitions at selected amplitude t and selected amplitude zero, almost surely.

    theorem tensorFrozenCGF_eq_log_difference {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 : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
        (j : Fin k) (t : ℝ) :
        tensorFrozenCGF eig c I degree amplitude n treeDegree h j t =ᵐ[
          (tensorFrozenLaw μ n b j).prod gaussianCoordinates]
        (fun p => tensorFrozenPartitionLog eig c I degree amplitude n treeDegree h j t p -
          tensorFrozenPartitionLog eig c I degree amplitude n treeDegree h j 0 p) := by
    …

    Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorFrozenCGF, OAI.InvariantIsing.tensorFrozenLaw, OAI.InvariantIsing.tensorFrozenPartitionLog