OAI/Probability/InvariantIsing/Cavity/CavityBaseReplacement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact removal and replacement of the small spectral block. The base matrix is defined without choosing bases in the retained eigenspaces.

  1. lemma OAI.InvariantIsing.cavityPhysicalChange_sub_special line 14
  2. lemma OAI.InvariantIsing.cavityPhysicalChange_pullback line 23
  3. lemma OAI.InvariantIsing.cavityPhysicalChange_reconstruct line 33
  4. def OAI.InvariantIsing.cavityBaseReplacement line 47
  5. theorem OAI.InvariantIsing.cavityBaseReplacement_difference line 53
  6. theorem OAI.InvariantIsing.cavityBaseReplacement_energy_difference line 66