OAI/Probability/InvariantIsing/Arrays/TensorZeroAmplitude.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorSiteProjection line 21
2. lemma OAI.InvariantIsing.tensorSiteProjection_add line 25
3. lemma OAI.InvariantIsing.tensorSiteProjection_measurePreserving line 30
4. lemma OAI.InvariantIsing.spinTensorEnergy_zero_amplitude line 52
5. lemma OAI.InvariantIsing.spinTensorTerminal_zero_amplitude line 61
6. theorem OAI.InvariantIsing.tensorCascadeValue_zero_amplitude line 75

   Source documentation

   Zero-amplitude tensor coordinates disappear at every Gaussian recursion step, irrespective of their unused variances.

   theorem tensorCascadeValue_zero_amplitude {N m k : ℕ} (eig : Fin N → ℝ) (U : Rotation N)
       (c : Fin N → ℝ) (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ)
       (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
       (site : ℕ → ℝ≥0) (hv : ∀ j i, v j (Sum.inl i) = site j)
       (z : SpinTensorIndex I degree → ℝ) :
       tensorCascadeValue eig U c I degree (fun _ => 0) n b v z =
         rotatedCascadeValue n b site eig U c (tensorSiteProjection I degree z) := by
   …

   Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorCascadeValue, OAI.InvariantIsing.rotatedCascadeValue, OAI.InvariantIsing.tensorSiteProjection

7. theorem OAI.InvariantIsing.tensorEnrichedPressure_zero_amplitude line 115

   Source documentation

   The exact unperturbed enriched-pressure identity used at temperature zero.

   theorem tensorEnrichedPressure_zero_amplitude {N m k : ℕ} (eig : Fin N → ℝ) (U : Rotation N)
       (c : Fin N → ℝ) (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ)
       (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
       (site : ℕ → ℝ≥0) (hv : ∀ j i, v j (Sum.inl i) = site j)
       (root : SpinTensorIndex I degree → ℝ≥0) (rootSite : ℝ≥0)
       (hroot : ∀ i, root (Sum.inl i) = rootSite) :
       tensorEnrichedPressure eig U c I degree (fun _ => 0) n b v root =
         rotatedEnrichedPressure n b site rootSite eig U c := by
   …

   Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorEnrichedPressure, OAI.InvariantIsing.rotatedEnrichedPressure

8. theorem OAI.InvariantIsing.tensorPathPressure_zero_amplitude line 139

   Source documentation

   The manuscript profile retains precisely the original linear-field increments when the monomial amplitudes vanish.

   theorem tensorPathPressure_zero_amplitude {N m k : ℕ} (eig : Fin N → ℝ) (U : Rotation N)
       (c : Fin N → ℝ) (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ)
       (n : ℕ) (b : ℕ → ℝ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) :
       tensorEnrichedPressure eig U c I degree (fun _ => 0) n b
         (fun i => tensorPathProfile I degree n treeDegree h (i + 1))
         (tensorPathProfile I degree n treeDegree h 0) =
       rotatedEnrichedPressure n b (fun i => varianceIncrement h (i + 1))
         (varianceIncrement h 0) eig U c :=
   …

   Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.tensorEnrichedPressure, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.rotatedEnrichedPressure, OAI.InvariantIsing.varianceIncrement

9. lemma OAI.InvariantIsing.varianceIncrement_heightSequence line 150
10. lemma OAI.InvariantIsing.varianceIncrement_heightSequence_zero line 156
11. theorem OAI.InvariantIsing.tensorPathPressure_field_zero_time line 166

    Source documentation

    The exact zero-temperature base value in the tensor model, with all unused monomial variances still present.

    theorem tensorPathPressure_field_zero_time {N m k : ℕ} (hN : 0 < N)
        (U : Rotation N) (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ)
        (treeDegree : Fin k → ℕ) (h : FieldStep) :
        tensorEnrichedPressure (fun _ => 0) U (fun _ => 0) I degree (fun _ => 0)
          h.depth (chainExponent h.cut)
          (fun i => tensorPathProfile I degree h.depth treeDegree (heightSequence h) (i + 1))
          (tensorPathProfile I degree h.depth treeDegree (heightSequence h) 0) -
          h.height (Fin.last h.depth) / 2 = fieldValue h 0 := by
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.tensorEnrichedPressure, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.heightSequence, OAI.InvariantIsing.fieldValue

12. theorem OAI.InvariantIsing.tensorPathPressure_zero_time_contact_nonneg line 180

    Source documentation

    The zero-temperature contact objective for the actual zero-amplitude tensor model is nonnegative.

    theorem tensorPathPressure_zero_time_contact_nonneg {N m k : ℕ} (hN : 0 < N)
        (U : Rotation N) (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ)
        (treeDegree : Fin k → ℕ) (h : FieldStep) (p : OverlapPath) {S : ℝ}
        (hS : entropyFunctional p ≤ (S : EReal)) :
        0 ≤ -(tensorEnrichedPressure (fun _ => 0) U (fun _ => 0) I degree (fun _ => 0)
          h.depth (chainExponent h.cut)
          (fun i => tensorPathProfile I degree h.depth treeDegree (heightSequence h) (i + 1))
          (tensorPathProfile I degree h.depth treeDegree (heightSequence h) 0) -
          h.height (Fin.last h.depth) / 2) - fieldPairing p h / 2 + S := by
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.entropyFunctional, OAI.InvariantIsing.tensorEnrichedPressure, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.heightSequence, OAI.InvariantIsing.fieldPairing