OAI/Probability/InvariantIsing/Core/GGErrorAlgebra.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Error bookkeeping in the Gaussian GG comparison.

  1. lemma OAI.InvariantIsing.gaussianGG_of_energy_identities line 11

    Source documentation

    Compare the replica energy identity with its one-replica version, keeping both the energy fluctuation and diagonal covariance errors.

    lemma gaussianGG_of_energy_identities {t b c E U M V L L₀ O F P n : ℝ}
    (hE : 0 ≤ E) (hU : |U - b * V| ≤ c * E) (hM : |M - b| ≤ E)
    (hV : |V| ≤ c) (hu : U = t * (L + O - n * F))
    (hm : M = t * (L₀ - P)) :
    |t| * |n * F - V * P - O| ≤ 2 * c * E + |t| * |L - V * L₀| := by
…