OAI/Probability/InvariantIsing/Arrays/NSpinTensorTerminalDerivative.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.integral_uniformSpinPrior line 15
2. lemma OAI.InvariantIsing.integral_uniformSpinGibbs_eq line 25
3. def OAI.InvariantIsing.tensorCoordinateVariation line 45
4. lemma OAI.InvariantIsing.spinTensorEnergy_coordinateVariation line 50
5. def OAI.InvariantIsing.tensorTerminalCoordinateMean line 61
6. def OAI.InvariantIsing.tensorFeatureCoordinateCap line 68
7. lemma OAI.InvariantIsing.tensorTerminalCoordinateMean_abs_le line 73
8. lemma OAI.InvariantIsing.measurable_tensorTerminalCoordinateMean line 84
9. theorem OAI.InvariantIsing.hasDerivAt_spinTensorTerminal_coordinate line 97

   Source documentation

   An actual coordinate derivative of the finite Ising terminal.

   theorem hasDerivAt_spinTensorTerminal_coordinate {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 → ℝ)
       (z : SpinTensorIndex I degree → ℝ) (j : SpinTensorIndex I degree) (t : ℝ) :
       HasDerivAt (fun s => spinTensorTerminal eig U c I degree amplitude
         (tensorCoordinateVariation I degree z j s))
         (tensorTerminalCoordinateMean eig U c I degree amplitude
           (tensorCoordinateVariation I degree z j t) j) t := by
   …

   Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.spinTensorTerminal, OAI.InvariantIsing.tensorCoordinateVariation, OAI.InvariantIsing.tensorTerminalCoordinateMean

10. def OAI.InvariantIsing.tensorProjectedMagnetization line 121
11. lemma OAI.InvariantIsing.tensorProjectedMagnetization_eq line 128
12. lemma OAI.InvariantIsing.tensorPairPathSpinMean_overlap line 149
13. theorem OAI.InvariantIsing.tensorPairPathSpinMean_overlap_gradient line 171

    Source documentation

    The actual projected overlap along two paths is the product of the projected terminal Gibbs gradients.

    theorem tensorPairPathSpinMean_overlap_gradient {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 : ℕ) (p : TensorPairPathData I degree n) (J : Finset (Fin N)) :
        tensorPairPathSpinMean eig U c I degree amplitude n p
          (fun σ => projectedOverlap U J (σ 0) (σ 1)) =
          (N : ℝ)⁻¹ * ∑ a ∈ J,
            U (WithLp.toLp 2 (fun i => tensorTerminalCoordinateMean eig U c I degree amplitude
              (tensorPairPathState I degree n p 0) (Sum.inl i))) a *
            U (WithLp.toLp 2 (fun i => tensorTerminalCoordinateMean eig U c I degree amplitude
              (tensorPairPathState I degree n p 1) (Sum.inl i))) a := by
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.TensorPairPathData, OAI.InvariantIsing.tensorPairPathSpinMean, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.tensorTerminalCoordinateMean, OAI.InvariantIsing.tensorPairPathState