OAI/Probability/InvariantIsing/Spectral/SpectralCountComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Pressure comparison from the fractions of changed axes in the two endpoint eigenspaces. This is the analytic part of manuscript Lemma gen:counts.

  1. lemma OAI.InvariantIsing.measurable_countPressure line 15
  2. lemma OAI.InvariantIsing.integrable_countPressure line 19
  3. lemma OAI.InvariantIsing.rotatedPressure_spectral_secant line 33
  4. theorem OAI.InvariantIsing.meanPressure_change_counts_le line 65

    Source documentation

    Changing a fraction at most r of every endpoint eigenspace changes the mean pressure by at most L*r/2, where every eigenvalue displacement is at most L.

    theorem meanPressure_change_counts_le {N m : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
    (eig kap c : Fin N → ℝ) (K : ℝ)
    (heig : ∀ i, |eig i| ≤ K) (hkap : ∀ i, |kap i| ≤ K)
    (label label' : Fin N → Fin m)
    (hl : Function.Surjective label) (hl' : Function.Surjective label')
    (lam : Fin m → ℝ) (he : ∀ i, eig i = lam (label i))
    (hk : ∀ i, kap i = lam (label' i))
    (changed : Finset (Fin N)) (hzero : ∀ i, i ∉ changed → kap i = eig i)
    (L r : ℝ) (hL : 0 ≤ L) (hdelta : ∀ i, |kap i - eig i| ≤ L)
    (hc : ∀ a, ((changed.filter fun i => label i = a).card : ℝ) ≤
      r * ((Finset.univ.filter fun i => label i = a).card : ℝ))
…

    Mentions: OAI.InvariantIsing.SpecialOrthogonal