OAI/Probability/InvariantIsing/Arrays/NSpinTensorFlatMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorFlatLog line 16
2. lemma OAI.InvariantIsing.measurable_tensorFlatLog line 23
3. lemma OAI.InvariantIsing.tensorLeafCoefficients_finite_bound line 44
4. lemma OAI.InvariantIsing.tensorFlat_base_exp_integrable line 67
5. lemma OAI.InvariantIsing.tensorFlat_base_log line 75
6. lemma OAI.InvariantIsing.random_cylinder_log_integrable line 89
7. theorem OAI.InvariantIsing.tensorFlatLog_integrable line 130

   Source documentation

   Joint integrability over the actual cascade branching and flat Gaussian coordinates, without a variance or pressure-limit hypothesis.

   theorem tensorFlatLog_integrable {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) :
       Integrable (tensorFlatLog eig U c I degree amplitude n v)
         ((labeledCascadeLaw n b : Measure (LabeledTree n)).prod gaussianCoordinates) := by
   …

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

8. theorem OAI.InvariantIsing.tensorFlatLog_mean line 151

   Source documentation

   The flat spin/leaf log partition has exactly the same mean as the root-averaged tensor cascade recursion.

   theorem tensorFlatLog_mean {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) :
       (∫ p, tensorFlatLog eig U c I degree amplitude n v p
         ∂(labeledCascadeLaw n b : Measure (LabeledTree n)).prod gaussianCoordinates) =
         ∫ z, tensorCascadeValue eig U c I degree amplitude n b (fun i => v (i + 1)) z
           ∂(tensorGaussianLaw I degree (v 0) : Measure (SpinTensorIndex I degree → ℝ)) := by
   …

   Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorFlatLog, OAI.InvariantIsing.tensorCascadeValue, OAI.InvariantIsing.tensorGaussianLaw

9. theorem OAI.InvariantIsing.tensorEnrichedPressure_eq_flat_mean line 199