OAI/Probability/InvariantIsing/Fields/FieldProjectionLoss.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A depth-free terminal loss estimate for the actual constrained partition function. It separates the field second moment from the expected number of flips, before any Gaussian-path averaging.

  1. def OAI.InvariantIsing.fieldProjectionDistance line 17
  2. lemma OAI.InvariantIsing.fieldProjectionDistance_nonneg line 20
  3. lemma OAI.InvariantIsing.two_sqrt_mul_le_add_div line 25
  4. theorem OAI.InvariantIsing.field_projection_terminal_loss line 32
  5. theorem OAI.InvariantIsing.field_projection_terminal_loss_linear line 44