OAI/Probability/InvariantIsing/Arrays/TensorLeafCoefficients.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorLeafCoefficients line 17

   Source documentation

   Level zero is the common root mark. Positive levels encode the corresponding ancestor prefix of the labeled leaf.

   def tensorLeafCoefficients {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)
       (x : Spin N × LabeledLeaf n) : ℕ →₀ ℝ :=
   …

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

2. lemma OAI.InvariantIsing.tensorLeafCoefficients_cross line 25
3. lemma OAI.InvariantIsing.tensorLeafCoefficients_variance_le line 56
4. lemma OAI.InvariantIsing.cylinderCross_sub_left line 71
5. theorem OAI.InvariantIsing.tensorLeafCoefficients_increment_cross_le line 79

   Source documentation

   The full root/ancestor tensor increment has a uniform covariance modulus, independently of the pair of cascade leaves.

   theorem tensorLeafCoefficients_increment_cross_le {N m k : ℕ} (hN : 0 < N)
       (U V W : SpecialOrthogonal N)
       (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
       (n : ℕ) (site : Fin (n + 1) → ℝ≥0) (monomial : Fin (n + 1) → Fin k → ℝ≥0)
       (x y : Spin N × LabeledLeaf n) :
       let A := fun R => tensorLeafCoefficients (specialRotation R) I degree amplitude n
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorLeafCoefficients, OAI.InvariantIsing.specialRotation