OAI/Analysis/BiholderTransport/LinearAlgebra/RescaledJoinOperator.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.fixedJoinAction_regular_contDiffAt line 22
2. lemma OAI.WeakMTWTransport.fixedJoinOperator_regular_rescale line 45
3. lemma OAI.WeakMTWTransport.fixedJoinOperator_regular_nonneg line 68
4. lemma OAI.WeakMTWTransport.fixedJoinOperator_inverse_nonneg line 83