OAI/MathematicalPhysics/CriticalSK/Resolvent.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.directed_neighbor_sum_general line 36
  2. def OAI.CriticalSK.triSampleMatrix line 55
  3. lemma OAI.CriticalSK.triSampleMatrix_hermitian line 60
  4. def OAI.CriticalSK.triSampleOperator line 67
  5. lemma OAI.CriticalSK.triSampleOperator_symmetric line 70
  6. lemma OAI.CriticalSK.generic_tridiagonal_quadratic line 73
  7. lemma OAI.CriticalSK.triSampleOperator_inner line 105
  8. def OAI.CriticalSK.extendPath line 112
  9. lemma OAI.CriticalSK.extendPath_restrict line 115
  10. lemma OAI.CriticalSK.extendPath_mass line 120
  11. lemma OAI.CriticalSK.pathOperator_energy line 127
  12. lemma OAI.CriticalSK.pathOperator_inner_le_two line 134
  13. lemma OAI.CriticalSK.pathOperator_eigenvalue_le_two line 140
  14. lemma OAI.CriticalSK.triSampleOperator_form_good line 149
  15. lemma OAI.CriticalSK.weighted_resolvent_integrable line 167
  16. lemma OAI.CriticalSK.fractional_power_integral_bound line 180
  17. lemma OAI.CriticalSK.fractional_trace_bound line 205
  18. lemma OAI.CriticalSK.inverse_perturbation_bound line 237
  19. lemma OAI.CriticalSK.inverse_perturbation_bound' line 258
  20. lemma OAI.CriticalSK.resolvent_trace_transfer line 262
  21. def OAI.CriticalSK.formA line 314
  22. def OAI.CriticalSK.formB line 318
  23. def OAI.CriticalSK.formC line 320
  24. lemma OAI.CriticalSK.formError_eq line 322
  25. lemma OAI.CriticalSK.formA_nonneg line 325
  26. lemma OAI.CriticalSK.formB_nonneg line 327
  27. lemma OAI.CriticalSK.formC_nonneg line 329
  28. def OAI.CriticalSK.orderedJacobiGaps line 331
  29. def OAI.CriticalSK.sampleEigenvalues line 334
  30. lemma OAI.CriticalSK.orderedJacobiGaps_nonneg line 337
  31. lemma OAI.CriticalSK.triSample_eigenvalue_good line 340
  32. lemma OAI.CriticalSK.symmetric_eigenvalue_sum_congr line 354
  33. lemma OAI.CriticalSK.sum_orderedJacobiGaps line 362
  34. lemma OAI.CriticalSK.orderedJacobi_trace line 374
  35. lemma OAI.CriticalSK.triSample_resolvent_good line 396