OAI/Probability/InvariantIsing/Spectral/SpectralPathSynchronization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.group_abs_increment_le_total line 14
2. theorem OAI.InvariantIsing.group_quantile_lipschitz_factor line 29

   Source documentation

   A group coordinate is a Lipschitz function of total overlap on the entire set of good quantile parameters. Plateaus give a unique value.

   theorem group_quantile_lipschitz_factor {m : ℕ} (p : OverlapPath) (pa : Fin m → OverlapPath)
       (hsum : ∀ᵐ s ∂pathMeasure, (∑ a, pa a s) = p s) (a : Fin m) :
       ∃ f : ℝ → ℝ, LipschitzWith 1 f ∧ ∀ᵐ s ∂pathMeasure, pa a s = f (p s) := by
   …

   Mentions: OAI.InvariantIsing.OverlapPath

3. lemma OAI.InvariantIsing.factor_of_pair_law line 55
4. theorem OAI.InvariantIsing.spectralPartition_lipschitz_synchronization line 70

   Source documentation

   The actual group overlap is a measurable, one-Lipschitz function of the actual total overlap. No separate synchronization hypothesis is used.

   theorem spectralPartition_lipschitz_synchronization {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 : ℝ))
       (a : Fin m) :
       ∃ f : ℝ → ℝ, LipschitzWith 1 f ∧
   …

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

5. lemma OAI.InvariantIsing.exists_injective_nat_pair line 110
6. lemma OAI.InvariantIsing.spectral_factor_all_off_diagonal line 120