OAI/Probability/InvariantIsing/Pressure/RandomBoundedDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A bounded random observable has a differentiable disorder-averaged CGF. This applies to the actual temperature observable retaining common disorder.

  1. lemma OAI.InvariantIsing.integrable_bounded_random_tilted_mean line 14
  2. theorem OAI.InvariantIsing.hasDerivAt_bounded_random_cgf line 27