CavityScalarRoot.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The root-averaged scalar spin recursion occurring after the cavity quadratic change of measure, in the manuscript's field normalization.

def OAI.InvariantIsing.cavityScalarCascadeMean line 14
theorem OAI.InvariantIsing.cavityScalarCascadeMean_normalized line 20

theorem OAI.InvariantIsing.cavityScalarCascadeMean_fieldStep line 53

Source documentation

The scalar part in cav:before-parts, with the root interval and ordinary residual both included.

theorem cavityScalarCascadeMean_fieldStep (N : ℕ) (hN : 0 < N)
    (h : FieldStep) (residual : ℝ≥0) (c : ℝ) (U : Rotation N) :
    (N : ℝ)⁻¹ * cavityScalarCascadeMean N h.depth (chainExponent h.cut)
      (fieldCascadeVariance h) (NNReal.mk (h.height 0) (h.nonneg 0)) residual c =
      fieldValue h 0 + h.height (Fin.last h.depth) / 2 + (c + residual) / 2 := by
…

Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.cavityScalarCascadeMean, OAI.InvariantIsing.fieldCascadeVariance, OAI.InvariantIsing.fieldValue

theorem OAI.InvariantIsing.cavityScalarCascadeMean_diagonal line 67

Source documentation

A residual variance equal to the gap from the final common-level variance to the diagonal removes that final height from the normalized spin contribution.

theorem cavityScalarCascadeMean_diagonal (N : ℕ) (hN : 0 < N)
    (h : FieldStep) (diagonal : ℝ) (hd : h.height (Fin.last h.depth) ≤ diagonal)
    (c : ℝ) (U : Rotation N) :
    (N : ℝ)⁻¹ * cavityScalarCascadeMean N h.depth (chainExponent h.cut)
      (fieldCascadeVariance h) (NNReal.mk (h.height 0) (h.nonneg 0))
      (NNReal.mk (diagonal - h.height (Fin.last h.depth)) (sub_nonneg.mpr hd)) c =
      fieldValue h 0 + (c + diagonal) / 2 := by
…

Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.cavityScalarCascadeMean, OAI.InvariantIsing.fieldCascadeVariance, OAI.InvariantIsing.fieldValue