OAI/Probability/InvariantIsing/Core/MultiplicityContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.eventually_relative_count_bound line 14
2. lemma OAI.InvariantIsing.eventually_surjective_label line 39
3. theorem OAI.InvariantIsing.meanPressure_same_proportions_tendsto line 59

   Source documentation

   Two spectra with the same finite alphabet and the same positive limiting proportions have asymptotically equal Haar mean pressures.

   theorem meanPressure_same_proportions_tendsto {m : ℕ}
       (N : ℕ → ℕ) (hN : ∀ k, 0 < N k)
       (μ : (k : ℕ) → Measure (SpecialOrthogonal (N k)))
       [∀ k, IsProbabilityMeasure (μ k)] (hμ : ∀ k, (μ k).IsMulLeftInvariant)
       (a b : (k : ℕ) → Fin (N k) → Fin m)
       (rho : Fin m → ℝ) (hrho : ∀ v, 0 < rho v)
       (ha : Tendsto (fun k v => ((Finset.univ.filter fun i => a k i = v).card : ℝ) / N k)
         atTop (𝓝 rho))
       (hb : Tendsto (fun k v => ((Finset.univ.filter fun i => b k i = v).card : ℝ) / N k)
         atTop (𝓝 rho))
       (lam : Fin m → ℝ) (c : (k : ℕ) → Fin (N k) → ℝ)
       (K : ℝ) (hK : ∀ v, |lam v| ≤ K)
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal