OAI/Geometry/WeakHessian/LocalBounds/GraphReuse.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.IsLaplacian.gradient_energy line 25
  2. lemma OAI.WeakHessian.IsLaplacian.gradient_norm_sq_le line 32
  3. lemma OAI.WeakHessian.graph_tendsto_gradient_difference line 44
  4. lemma OAI.WeakHessian.graph_tendsto_weakGradient line 72
  5. lemma OAI.WeakHessian.tendsto_toLp_mul_bounded line 95
  6. lemma OAI.WeakHessian.integral_mul_eq_inner line 115
  7. lemma OAI.WeakHessian.tendsto_integral_mul_L2 line 123
  8. lemma OAI.WeakHessian.graph_tendsto_gamma line 135
  9. def OAI.WeakHessian.graphBochner line 166
  10. lemma OAI.WeakHessian.graphBochner_tendsto line 171
  11. lemma OAI.WeakHessian.graph_tendsto_weighted_gamma line 212
  12. lemma OAI.WeakHessian.graphBochner_bound_of_approx line 232
  13. lemma OAI.WeakHessian.graphBochner_eq_core line 248
  14. lemma OAI.WeakHessian.graphBochner_eq_BE line 285
  15. lemma OAI.WeakHessian.graph_tendsto_reweight line 316
  16. def OAI.WeakHessian.OriginalTestGraphCore line 351
  17. lemma OAI.WeakHessian.graphBochner_reweight_eq_drift line 361
  18. lemma OAI.WeakHessian.OriginalTestGraphCore.reweight_approx line 395