OAI/Probability/InvariantIsing/Pressure/ThermalPressure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.rotatedEnergy_scale line 15
2. lemma OAI.InvariantIsing.abs_rotatedEnergy_le line 21
3. lemma OAI.InvariantIsing.GibbsReference_one line 27
4. def OAI.InvariantIsing.thermalPressureDerivative line 31
5. lemma OAI.InvariantIsing.hasDerivAt_rotatedPressure_temperature line 35
6. lemma OAI.InvariantIsing.abs_thermalPressureDerivative_le line 54
7. lemma OAI.InvariantIsing.measurable_thermalPressureDerivative line 68
8. theorem OAI.InvariantIsing.hasDerivAt_mean_pressure_temperature line 79

   Source documentation

   Differentiation commutes with the disorder expectation. The bound is uniform in the field and does not require Haar invariance.

   theorem hasDerivAt_mean_pressure_temperature {N : ℕ} (hN : 0 < N)
       {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
       (U : Ω → SpecialOrthogonal N) (hU : Measurable U)
       (eig c : Fin N → ℝ) (K : ℝ) (heig : ∀ i, |eig i| ≤ K) (t : ℝ) :
       HasDerivAt (fun s => ∫ ω, rotatedPressure (fun i => s * eig i) (specialRotation (U ω)) c ∂P)
         (∫ ω, thermalPressureDerivative eig c (specialRotation (U ω)) t ∂P) t := by
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.thermalPressureDerivative