OAI/Probability/InvariantIsing/Spectral/SpectralGGGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.spectralGram_diagonal line 14
2. def OAI.InvariantIsing.spectralLinearEntry line 19
3. def OAI.InvariantIsing.spectralLinearArray line 22
4. lemma OAI.InvariantIsing.continuous_spectralLinearEntry line 25
5. lemma OAI.InvariantIsing.continuous_spectralLinearArray line 30
6. lemma OAI.InvariantIsing.spectralGram_linear line 35
7. lemma OAI.InvariantIsing.spectralGG_coordinate_nonnegative line 51
8. lemma OAI.InvariantIsing.spectralGG_linear_ultrametric line 63
9. theorem OAI.InvariantIsing.spectralGG_support_ordered line 82

   Source documentation

   Nonnegative combinations of the actual spectral and tree coordinates have ordered joint support. This is the finite-vector consequence used for the manuscript's simultaneous overlap paths.

   theorem spectralGG_support_ordered {m : ℕ} {Q : ProbabilityMeasure (SpectralArray m)}
       (hgg : HasEntryGhirlandaGuerra (fun x i j => x (i,j)) (Q : Measure (SpectralArray m)))
       (hG : ∀ᵐ x ∂(Q : Measure (SpectralArray m)), SpectralGram x)
       (q : Fin m → ℝ) (hq : ∀ a, 0 ≤ q a)
       (hd : ∀ᵐ x ∂(Q : Measure (SpectralArray m)), ∀ i a, (x (i,i) a : ℝ) = q a)
       (hE : ∀ e : Equiv.Perm ℕ,
         (Q : Measure (SpectralArray m)).map (permuteSpectralArray e) = Q)
       (w z : Fin m → ℝ) (hw : ∀ a, 0 ≤ w a) (hz : ∀ a, 0 ≤ z a) :
       let ν := (Q : Measure (SpectralArray m)).map
   …

   Mentions: OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.SpectralGram, OAI.InvariantIsing.permuteSpectralArray