OAI/Probability/SKRatio/Variational/UniformGap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Fields.coupling_smul line 15
  2. lemma OAI.SKRatio.Fields.euclideanOpNorm_smul line 20
  3. theorem OAI.SKRatio.Fields.scaled_poincare_of_matrix_bounds line 30
  4. def OAI.SKRatio.Fields.linearObservable line 50
  5. lemma OAI.SKRatio.Fields.spinGradient_linearObservable line 52
  6. lemma OAI.SKRatio.Fields.dirichlet_linearObservable line 65
  7. theorem OAI.SKRatio.Fields.covariance_bound_of_poincare line 78
  8. lemma OAI.SKRatio.Fields.heatBathGenerator_zero_field line 85
  9. lemma OAI.SKRatio.Fields.variance_eq_finiteLaw line 95
  10. lemma OAI.SKRatio.Fields.dirichlet_zero_eq_stationaryEnergy line 98
  11. theorem OAI.SKRatio.Fields.stationary_poincare_of_matrix_bounds line 104
  12. theorem OAI.SKRatio.Fields.exists_uniform_gap_tolerance line 113