OAI/Probability/SKRatio/Calculus/SignedVector.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Calculus.gradientForm_pairs_bound line 14
  2. theorem OAI.SKRatio.Calculus.rough_gradient_bound line 61
  3. def OAI.SKRatio.Calculus.signedVector line 71
  4. lemma OAI.SKRatio.Calculus.norm_signedVector line 74
  5. lemma OAI.SKRatio.Calculus.signConjugate_action line 79
  6. lemma OAI.SKRatio.Calculus.euclideanOpNorm_signConjugate_le line 92
  7. lemma OAI.SKRatio.Calculus.signConjugate_twice line 100
  8. lemma OAI.SKRatio.Calculus.euclideanOpNorm_signConjugate line 108
  9. theorem OAI.SKRatio.Calculus.gradient_global_bound line 113
  10. lemma OAI.SKRatio.Calculus.rough_coefficient_lt_two line 127
  11. theorem OAI.SKRatio.Calculus.gradient_dissipation_small_norm line 135
  12. def OAI.SKRatio.Calculus.attemptLM line 151
  13. def OAI.SKRatio.Calculus.continuousKernel line 155
  14. def OAI.SKRatio.Calculus.siteRefresh line 159
  15. theorem OAI.SKRatio.Calculus.generator_siteRefresh line 164
  16. theorem OAI.SKRatio.Calculus.attempt_apply_of_pos line 177
  17. theorem OAI.SKRatio.Calculus.generator_const line 187
  18. theorem OAI.SKRatio.Calculus.siteRefresh_const line 191
  19. theorem OAI.SKRatio.Calculus.attempt_const line 196
  20. theorem OAI.SKRatio.Calculus.attempt_pow_const line 202
  21. theorem OAI.SKRatio.Calculus.siteRefresh_nonneg line 208
  22. theorem OAI.SKRatio.Calculus.attempt_nonneg line 216
  23. theorem OAI.SKRatio.Calculus.attempt_pow_nonneg line 225
  24. theorem OAI.SKRatio.Calculus.exp_apply_hasSum line 233
  25. theorem OAI.SKRatio.Calculus.exp_apply_of_apply_eq_zero line 242
  26. theorem OAI.SKRatio.Calculus.semigroup_const line 257
  27. theorem OAI.SKRatio.Calculus.exp_smul_identity line 264
  28. theorem OAI.SKRatio.Calculus.semigroup_uniformization line 270
  29. theorem OAI.SKRatio.Calculus.semigroup_nonneg line 289
  30. theorem OAI.SKRatio.Calculus.continuousKernel_nonneg line 311
  31. theorem OAI.SKRatio.Calculus.continuousKernel_sum line 315
  32. theorem OAI.SKRatio.Calculus.attempt_eq_transition line 324
  33. theorem OAI.SKRatio.Calculus.attempt_pow_eq_transition_pow line 337
  34. theorem OAI.SKRatio.Calculus.semigroup_add line 345
  35. theorem OAI.SKRatio.Calculus.semigroup_mono line 353
  36. theorem OAI.SKRatio.Calculus.semigroup_abs_le line 359
  37. theorem OAI.SKRatio.Calculus.observable_basis line 367
  38. theorem OAI.SKRatio.Calculus.semigroup_eq_kernel line 372
  39. theorem OAI.SKRatio.Calculus.kernel_eq_mulVec line 380
  40. theorem OAI.SKRatio.Calculus.continuousKernel_add line 385
  41. theorem OAI.SKRatio.Calculus.continuousKernel_poisson_hasSum line 393