CavityFieldIncrement.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The scalar field increments prescribed by the quadratic cavity calculation are exactly the integrals defining the manuscript field path.

lemma OAI.InvariantIsing.continuousAt_deriv_finiteR_pos line 17

theorem OAI.InvariantIsing.integral_finiteR_deriv_deficit_gap line 29

Source documentation

Positive-level covariance increments; no assumption about endpoint atoms is needed, only that the open interval is a gap in the support.

theorem integral_finiteR_deriv_deficit_gap (rho lam : ι → ℝ)
    (hrho : ∀ a, 0 < rho a) (hsum : ∑ a, rho a = 1)
    (p : OverlapPath) {a b : ℝ} (hab : a < b)
    (hgap : ∀ᵐ s ∂pathMeasure, p s ≤ a ∨ b ≤ p s)
    (hpos : 0 < deficit p b) (hmass : pathMeasure.real {s | p s ≤ a} ≠ 0) :
    (∫ r in a..b, deriv (finiteR rho lam hrho hsum) (deficit p r)) =
      (finiteR rho lam hrho hsum (deficit p a) -
        finiteR rho lam hrho hsum (deficit p b)) / pathMeasure.real {s | p s ≤ a} := by
…

Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.finiteR

theorem OAI.InvariantIsing.integral_finiteR_deriv_deficit_root line 70

Source documentation

The common-root contribution includes the full interval below the smallest overlap, on which the deficit is constant.

theorem integral_finiteR_deriv_deficit_root (rho lam : ι → ℝ)
    (hrho : ∀ a, 0 < rho a) (hsum : ∑ a, rho a = 1) (p : OverlapPath) :
    (∫ r in 0..Function.rightLim p.val 0,
      deriv (finiteR rho lam hrho hsum) (deficit p r)) =
      Function.rightLim p.val 0 * deriv (finiteR rho lam hrho hsum)
        (deficit p (Function.rightLim p.val 0)) := by
…

Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.finiteR