OAI/Analysis/BiholderTransport/LinearAlgebra/ShearedOperator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.shearedRadialOperator line 24
2. lemma OAI.WeakMTWTransport.inner_shearedRadialOperator line 33
3. lemma OAI.WeakMTWTransport.shearedRadialOperator_symmetric line 39
4. lemma OAI.WeakMTWTransport.uniform_sheared_radial_quadratic_bounds line 48
5. lemma OAI.WeakMTWTransport.WeakMTW.shearedRadialOperator_convexOn line 72
6. lemma OAI.WeakMTWTransport.ordered_sheared_background_spectrum line 97