OAI/Probability/FreeIsing/Ising/CopySpectral.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.IsingCopySpectral.centeredAverage_norm_le line 17
  2. abbrev OAI.Problem367.IsingCopySpectral.differenceSpace line 27
  3. def OAI.Problem367.IsingCopySpectral.averageOnDifferences line 33
  4. theorem OAI.Problem367.IsingCopySpectral.copyReflection_involutive line 44
  5. theorem OAI.Problem367.IsingCopySpectral.averageOnDifferences_isSelfAdjoint line 51
  6. theorem OAI.Problem367.IsingCopySpectral.averageOnDifferences_norm_le line 59
  7. def OAI.Problem367.IsingCopySpectral.differenceReflection line 71
  8. theorem OAI.Problem367.IsingCopySpectral.differenceReflection_involutive line 81
  9. theorem OAI.Problem367.IsingCopySpectral.neighborAverage_differenceReflection line 89
  10. theorem OAI.Problem367.IsingCopySpectral.forwardOperator_pow_bound line 97
  11. theorem OAI.Problem367.IsingCopySpectral.summable_forwardOperator_pow line 109