OAI/Probability/InvariantIsing/Spectral/SpectralPartitionPaths.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.spectralCoordinate_unit line 15
2. def OAI.InvariantIsing.spectralPartitionQuantileWeights line 23
3. def OAI.InvariantIsing.spectralPartitionRelation line 26
4. lemma OAI.InvariantIsing.spectralPartitionQuantileWeights_nonneg line 29
5. lemma OAI.InvariantIsing.spectralPartitionRelation_eq_zero line 38
6. theorem OAI.InvariantIsing.spectralPartitionQuantileWeights_unit line 48
7. theorem OAI.InvariantIsing.spectralPartition_quantile_sum line 63

   Source documentation

   The spectral partition and vector Ghirlanda–Guerra synchronization yield the sum identity.

   theorem spectralPartition_quantile_sum {m : ℕ}
       {Q : ProbabilityMeasure (SpectralArray (m + 1))}
       (hgg : HasEntryGhirlandaGuerra (fun x i j => x (i,j)) (Q : Measure (SpectralArray (m + 1))))
       (hG : ∀ᵐ x ∂(Q : Measure (SpectralArray (m + 1))), SpectralGram x)
       (q : Fin (m + 1) → ℝ) (hq : ∀ a, 0 ≤ q a)
       (hd : ∀ᵐ x ∂(Q : Measure (SpectralArray (m + 1))), ∀ i a, (x (i,i) a : ℝ) = q a)
       (hE : ∀ e : Equiv.Perm ℕ,
         (Q : Measure (SpectralArray (m + 1))).map (permuteSpectralArray e) = Q)
       (hP : ∀ᵐ x ∂(Q : Measure (SpectralArray (m + 1))), SpectralPartitionGeometry m x)
       (hn : ∀ᵐ x ∂(Q : Measure (SpectralArray (m + 1))), ∀ a, 0 ≤ (x (0,1) a : ℝ)) :
       ∀ᵐ s ∂pathMeasure,
         (∑ a : Fin m, spectralQuantilePath Q (Pi.single a.castSucc 1) (spectralCoordinate_unit hn a.castSucc) s) =
   …

   Mentions: OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.SpectralGram, OAI.InvariantIsing.permuteSpectralArray, OAI.InvariantIsing.SpectralPartitionGeometry, OAI.InvariantIsing.spectralQuantilePath, OAI.InvariantIsing.spectralCoordinate_unit

8. lemma OAI.InvariantIsing.group_increment_le_total line 87