NSpinTensorBackwardPaths.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Collapse the two independent residual paths to actual backward gradients.

def OAI.InvariantIsing.tensorPairCoordinatePayoff line 14
lemma OAI.InvariantIsing.tensorPairCoordinatePayoff_cons line 22
lemma OAI.InvariantIsing.tensorPairCoordinatePayoff_abs_le line 31

theorem OAI.InvariantIsing.tensorAncestorPairPathMean_independent_coordinates line 45

Source documentation

Once the two paths have branched, each terminal gradient averages independently to its actual backward gradient.

theorem tensorAncestorPairPathMean_independent_coordinates {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) (d q i : ℕ) (hqi : i + q = n) (hdi : d ≤ i)
    (z₁ z₂ : SpinTensorIndex I degree → ℝ) (j₁ j₂ : SpinTensorIndex I degree) :
    tensorAncestorPairPathMean eig U c I degree amplitude n b v d q i z₁ z₂
      (tensorPairCoordinatePayoff eig U c I degree amplitude q z₁ z₂ j₁ j₂) =
      tensorBackwardCoordinateMean eig U c I degree amplitude n b v i z₁ j₁ *
        tensorBackwardCoordinateMean eig U c I degree amplitude n b v i z₂ j₂ := by
…

Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorAncestorPairPathMean, OAI.InvariantIsing.tensorPairCoordinatePayoff, OAI.InvariantIsing.tensorBackwardCoordinateMean

def OAI.InvariantIsing.tensorSharedCoordinateProduct line 99

Source documentation

Only the shared ancestor increments remain after the independent suffixes have been integrated. At the branching level the integrand is the product of actual backward gradients.

def tensorSharedCoordinateProduct {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) (d : ℕ)
    (j₁ j₂ : SpinTensorIndex I degree) :
    (q : ℕ) → ℕ → (SpinTensorIndex I degree → ℝ) → (SpinTensorIndex I degree → ℝ) → ℝ
  | 0, i, z₁, z₂ =>
      tensorBackwardCoordinateMean eig U c I degree amplitude n b v i z₁ j₁ *
        tensorBackwardCoordinateMean eig U c I degree amplitude n b v i z₂ j₂
  | q + 1, i, z₁, z₂ =>
      if i < d then
        ∫ a, tensorSharedCoordinateProduct eig U c I degree amplitude n b v d j₁ j₂ q
…

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

lemma OAI.InvariantIsing.tensorSharedCoordinateProduct_nonneg line 116

theorem OAI.InvariantIsing.tensorAncestorPairPathMean_coordinates line 132

Source documentation

The finite pair-path expectation is an expectation over the common ancestor path of the backward gradient product at branching.

theorem tensorAncestorPairPathMean_coordinates {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) (d q i : ℕ) (hqi : i + q = n)
    (z₁ z₂ : SpinTensorIndex I degree → ℝ) (j₁ j₂ : SpinTensorIndex I degree) :
    tensorAncestorPairPathMean eig U c I degree amplitude n b v d q i z₁ z₂
      (tensorPairCoordinatePayoff eig U c I degree amplitude q z₁ z₂ j₁ j₂) =
      tensorSharedCoordinateProduct eig U c I degree amplitude n b v d j₁ j₂ q i z₁ z₂ := by
…

lemma OAI.InvariantIsing.tensorAncestorPairPathMean_const_mul line 166
lemma OAI.InvariantIsing.tensorPairPathSpinMean_features line 180

theorem OAI.InvariantIsing.tensorFeaturePair_backward_identity line 202

Source documentation

Actual finite tensor feature pair tests are expectations of backward gradient products along the shared ancestor path.

theorem tensorFeaturePair_backward_identity (hpub : PanchenkoTalagrandTensorPairInput)
    {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) (z : SpinTensorIndex I degree → ℝ)
    (ψ : ℕ → ℝ) {B : ℝ} (hB : 0 ≤ B) (hψ : ∀ d, |ψ d| ≤ B)
    (j₁ j₂ : SpinTensorIndex I degree) :
    tensorSpinPairAverage eig U c I degree amplitude n b v z ψ
      (fun σ => spinTensorFeature U I degree amplitude (σ 0) j₁ *
        spinTensorFeature U I degree amplitude (σ 1) j₂) =
      ∫ α : ℕ → LabeledLeaf n, ψ (labeledCommonDepth n (α 0) (α 1)) *
…

Mentions: OAI.InvariantIsing.PanchenkoTalagrandTensorPairInput, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorSpinPairAverage, OAI.InvariantIsing.spinTensorFeature

theorem OAI.InvariantIsing.tensorFeaturePair_nonneg line 233