TensorProfiles.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's linear enrichment and monomial tree variance increments.

def OAI.InvariantIsing.varianceIncrement line 14
lemma OAI.InvariantIsing.varianceIncrement_coe line 16
lemma OAI.InvariantIsing.varianceIncrement_sum line 20
def OAI.InvariantIsing.tensorPathProfile line 27
Source documentation
The root has variance h 0; each child adds the next field increment. For a tree monomial of degree zero the entire variance is at the root.
```
def tensorPathProfile {N m k : ℕ} (I : Fin m → Finset (Fin N))
    (degree : Fin k → Fin m → ℕ) (n : ℕ) (treeDegree : Fin k → ℕ)
    (h : ℕ → ℝ) (i : ℕ) : SpinTensorIndex I degree → ℝ≥0 :=
…
```
Mentions: OAI.InvariantIsing.SpinTensorIndex
lemma OAI.InvariantIsing.prefixPath_weighted_sum line 33
lemma OAI.InvariantIsing.prefixPath_linear_monomials line 43

theorem OAI.InvariantIsing.tensorPathProfile_covariance line 63

Source documentation

The tensor mark model with these increments has exactly the paper's linear field covariance plus the displayed joint spectral/tree monomials.

theorem tensorPathProfile_covariance {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 y : Spin N × LabeledLeaf n) :
    cylinderCross (tensorLeafCoefficients U I degree amplitude n
      (fun i => tensorPathProfile I degree n treeDegree h i) x)
      (tensorLeafCoefficients U I degree amplitude n
        (fun i => tensorPathProfile I degree n treeDegree h i) y) =
      h (labeledCommonDepth n x.2 y.2) * (∑ a, spinValue (x.1 a) * spinValue (y.1 a)) +
        ∑ j, amplitude j ^ 2 * (∏ a, projectedOverlap U (I a) x.1 y.1 ^ degree j a) *
          treeOverlap n x.2 y.2 ^ treeDegree j := by
…

Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorLeafCoefficients, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.spinValue, OAI.InvariantIsing.projectedOverlap

lemma OAI.InvariantIsing.monomialVarianceIncrement_sum_le line 89
lemma OAI.InvariantIsing.tensorPathProfile_variance_cap line 94

lemma OAI.InvariantIsing.tensorPathProfile_rotation_cap line 116

Source documentation

The sum over all tree levels contributes no extra factor of depth to the Gaussian rotation modulus.

lemma tensorPathProfile_rotation_cap {m k : ℕ} (degree : Fin k → Fin m → ℕ)
    (amplitude : Fin k → ℝ) (n : ℕ) (treeDegree : Fin k → ℕ) :
    (∑ i : Fin (n + 1), ∑ j, (varianceIncrement (monomialPath n (treeDegree j)) i : ℝ) *
      amplitude j ^ 2 * ∑ a, (degree j a : ℝ)) ≤
      ∑ j, amplitude j ^ 2 * ∑ a, (degree j a : ℝ) := by
…

Mentions: OAI.InvariantIsing.varianceIncrement