OAI/Probability/InvariantIsing/Spectral/MeasurePointMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The degenerate spectral law in the general approximation argument.

  1. lemma OAI.InvariantIsing.measureR_dirac line 14
  2. lemma OAI.InvariantIsing.measureVariational_dirac line 19
  3. theorem OAI.InvariantIsing.tendsto_pressure_scalar_variational line 25

    Source documentation

    The scalar spectral case of the pressure formula, for arbitrary rotations.

    theorem tendsto_pressure_scalar_variational
    (eig : (N : ℕ) → Fin (N + 1) → ℝ) (U : (N : ℕ) → Rotation (N + 1))
    (a : ℝ) (δ : ℕ → ℝ) (hδ : Tendsto δ atTop (𝓝 0))
    (heig : ∀ N i, |eig N i - a| ≤ δ N) :
    Tendsto (fun N => rotatedPressure (eig N) (U N) (fun _ => 0)) atTop
      (𝓝 (variationalFunctional (measureR (Measure.dirac a) a)).toReal) := by
…

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.variationalFunctional, OAI.InvariantIsing.measureR