OAI/Probability/InvariantIsing/Fields/FieldTiltDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A local integrable envelope permits covariance derivatives of a Gaussian logarithmic mean without a bounded-payoff assumption.

  1. lemma OAI.InvariantIsing.hasDerivAt_logMean_of_integrable_envelope line 14