SpectralMultiplicity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The spectral multiplicity comparison, with an arbitrary deterministic magnetic field. The relative count error is supplied as a scalar bound.

theorem OAI.InvariantIsing.meanPressure_multiplicity_comparison line 17

Source documentation

Manuscript Lemma gen:counts. Taking r to be the maximum relative multiplicity error gives its displayed bound.

theorem meanPressure_multiplicity_comparison {N m : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
    (a b : Fin N → Fin m) (ha : Function.Surjective a) (hb : Function.Surjective b)
    (lam : Fin m → ℝ) (c : Fin N → ℝ)
    (K : ℝ) (hK : ∀ v, |lam v| ≤ K)
    (L r : ℝ) (hL : 0 ≤ L) (hr : 0 ≤ r)
    (hdiam : ∀ v w, |lam v - lam w| ≤ L)
    (herr : ∀ v,
      |((Finset.univ.filter fun i => a i = v).card : ℝ) -
        ((Finset.univ.filter fun i => b i = v).card : ℝ)| ≤
      r * min ((Finset.univ.filter fun i => a i = v).card : ℝ)
        ((Finset.univ.filter fun i => b i = v).card : ℝ)) :
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal