OAI/Probability/InvariantIsing/Cavity/CavityRDerivative.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The continuous nonnegative right derivative of the finite spectral R-transform. Its extension at zero is the spectral variance; the constant extension of finiteR to negative arguments is not differentiated there.

  1. def OAI.InvariantIsing.cavityRDerivative line 17
  2. lemma OAI.InvariantIsing.cavityRDerivative_nonneg line 22
  3. lemma OAI.InvariantIsing.continuous_cavityRDerivative line 27
  4. lemma OAI.InvariantIsing.cavityRDerivative_zero line 34
  5. theorem OAI.InvariantIsing.cavityRDerivative_eq_deriv line 41
  6. theorem OAI.InvariantIsing.cavityRDerivative_le line 70
  7. theorem OAI.InvariantIsing.integral_cavityRDerivative line 91

    Source documentation

    The ordinary FTC includes the right endpoint derivative extension at zero while using derivatives only at strictly positive interior points.

    theorem integral_cavityRDerivative (rho lam : ι → ℝ) (hrho : ∀ a, 0 < rho a)
    (hsum : ∑ a, rho a = 1) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) :
    (∫ x in a..b, cavityRDerivative rho lam hrho hsum x) =
      finiteR rho lam hrho hsum b - finiteR rho lam hrho hsum a := by
…

    Mentions: OAI.InvariantIsing.cavityRDerivative, OAI.InvariantIsing.finiteR