OAI/Probability/InvariantIsing/Arrays/NSpinFactorization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantIsing.vectorCascade_logCosh_sum line 17
2. theorem OAI.InvariantIsing.rotatedCascadeValue_zero_interaction line 59
3. lemma OAI.InvariantIsing.integrable_gaussianReal_of_linearGrowth line 78
4. theorem OAI.InvariantIsing.rotatedEnrichedPressure_zero_interaction line 91
5. theorem OAI.InvariantIsing.rotatedEnrichedPressure_field_zero_time line 143

   Source documentation

   The exact zero-time normalization in up:zero-time, before perturbations.

   theorem rotatedEnrichedPressure_field_zero_time {N : ℕ} (hN : 0 < N)
       (h : FieldStep) (U : Rotation N) :
       rotatedEnrichedPressure h.depth (IsingPerceptron.chainExponent h.cut) (fieldCascadeVariance h)
         (NNReal.mk (h.height 0) (h.nonneg 0)) (fun _ => 0) U (fun _ => 0) -
         h.height (Fin.last h.depth) / 2 = fieldValue h 0 := by
   …

   Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.rotatedEnrichedPressure, OAI.IsingPerceptron.chainExponent, OAI.InvariantIsing.fieldCascadeVariance, OAI.InvariantIsing.fieldValue

6. theorem OAI.InvariantIsing.zero_time_contact_nonneg line 165

   Source documentation

   The unperturbed contact objective cannot be negative at zero interaction.

   theorem zero_time_contact_nonneg {N : ℕ} (hN : 0 < N) (h : FieldStep)
       (U : Rotation N) (p : OverlapPath) {S : ℝ} (hS : entropyFunctional p ≤ (S : EReal)) :
       0 ≤ -(rotatedEnrichedPressure h.depth (IsingPerceptron.chainExponent h.cut)
         (fieldCascadeVariance h) (NNReal.mk (h.height 0) (h.nonneg 0))
         (fun _ => 0) U (fun _ => 0) - h.height (Fin.last h.depth) / 2) -
         fieldPairing p h / 2 + S := by
   …

   Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.entropyFunctional, OAI.InvariantIsing.rotatedEnrichedPressure, OAI.IsingPerceptron.chainExponent, OAI.InvariantIsing.fieldCascadeVariance, OAI.InvariantIsing.fieldPairing