OAI/Analysis/BiholderTransport/LinearAlgebra/MovingHessianLimit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.tendsto_clm_apply line 16
2. lemma OAI.WeakMTWTransport.moving_rough_hessian_limit line 24
3. lemma OAI.WeakMTWTransport.bilinear_limit_nonneg line 48
4. lemma OAI.WeakMTWTransport.bilinear_limit_symm line 55
5. lemma OAI.WeakMTWTransport.bilinear_limit_kernel line 64