TensorContactTemperature.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The temperature-coordinate inequality at an actual joint minimum. The left variation remains valid at the upper endpoint t=1.

theorem OAI.InvariantIsing.tensorContact_minimum_temperature line 15

theorem OAI.InvariantIsing.tensorContact_minimum_energy_gap line 66

Source documentation

The manuscript's strict temperature tilt gives an energy gap at the same finite-volume minimum, including at temperature one.

theorem tensorContact_minimum_energy_gap {N m n : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (b : ℕ → ℝ) (w : Fin (n + 1) → ℝ)
    (ρ lam : Fin m → ℝ) (hρ : ∀ a, 0 < ρ a) (hρsum : ∑ a, ρ a = 1)
    (trial : OverlapPath) (δ S H : ℝ) (p : TensorContactParameter N m n)
    (hp : p ∈ tensorContactRegion N m n H)
    (hmin : ∀ q ∈ tensorContactRegion N m n H,
      tensorContactObjective μ eig c I b w S
        (fun t => finiteTemperatureFunctional ρ lam hρ hρsum trial t + t * δ) p ≤
      tensorContactObjective μ eig c I b w S
        (fun t => finiteTemperatureFunctional ρ lam hρ hρsum trial t + t * δ) q)
    (ht : 0 < p.1) (K : ℝ) (hK : ∀ i, |eig i| ≤ K) :
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.TensorContactParameter, OAI.InvariantIsing.tensorContactRegion, OAI.InvariantIsing.tensorContactObjective, OAI.InvariantIsing.finiteTemperatureFunctional