OAI/Probability/InvariantIsing/Fields/FieldPairingContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pairing errors for the rounded quantile paths used in the cavity calculation. A uniform field-height bound suffices for L1 stability.

  1. lemma OAI.InvariantIsing.field_pairing_path_error line 14
  2. theorem OAI.InvariantIsing.field_pairing_path_tendsto line 42