OAI/Probability/InvariantIsing/Cavity/CavityHaarCascadeMatch.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The fresh Haar field and the recalculated finite cascade have matching bounded spectral-group replica tests. The common limit is identified by GG and the Ward equations, rather than assumed as an auxiliary cascade law.

  1. def OAI.InvariantIsing.cavityGroupBlockOfBlock line 16
  2. lemma OAI.InvariantIsing.continuous_cavityGroupBlockOfBlock line 19
  3. lemma OAI.InvariantIsing.cavityGroupBlockOfBlock_view line 24
  4. theorem OAI.InvariantIsing.cavity_haar_recalculated_cascade_match line 27