OAI/Probability/InvariantIsing/Core/TrialGridApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Lower finite-grid trials approximate each monotone overlap path in L1, remain below one, and do not increase the entropy functional.

  1. def OAI.InvariantIsing.lowerGridPath line 16
  2. lemma OAI.InvariantIsing.lowerGridPath_below_one line 22
  3. lemma OAI.InvariantIsing.lowerGridPath_le line 27
  4. lemma OAI.InvariantIsing.lowerGridPath_entropy_le line 32
  5. lemma OAI.InvariantIsing.lowerGridPath_on_cell line 36
  6. lemma OAI.InvariantIsing.lowerGridPath_L1_tendsto line 42
  7. lemma OAI.InvariantIsing.lowerGridPath_spectral_tendsto line 58