OAI/Probability/InvariantIsing/Spectral/SpectralSymbols.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Symbols of reconstructed finite spectral-group overlap paths.

  1. def OAI.InvariantIsing.pathSymbol line 16
  2. theorem OAI.InvariantIsing.deficit_at_path_eq_symbol line 20

    Source documentation

    The total-overlap symbol is the deficit evaluated at the path.

    theorem deficit_at_path_eq_symbol (p : OverlapPath) {s : ℝ} (hs : s ∈ Icc (0 : ℝ) 1) :
    deficit p (p s) = pathSymbol 1 p s := by
…

    Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.pathSymbol

  3. theorem OAI.InvariantIsing.spectralGroupSymbol_nonneg line 53
  4. theorem OAI.InvariantIsing.sum_spectralGroupSymbol line 68