OAI/Analysis/BiholderTransport/Regularity/MaximumDiagonal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakMTWTransport.MaximumJensenFamily.sampleIndex line 24
2. def OAI.WeakMTWTransport.MaximumJensenFamily.samplePoint line 27
3. def OAI.WeakMTWTransport.MaximumJensenFamily.sampleCenter line 33
4. def OAI.WeakMTWTransport.MaximumJensenFamily.sampleGradient line 36
5. def OAI.WeakMTWTransport.MaximumJensenFamily.sampleH line 43
6. def OAI.WeakMTWTransport.MaximumJensenFamily.sampleL line 48
7. structure OAI.WeakMTWTransport.MaximumDiagonal line 53
8. lemma OAI.WeakMTWTransport.MaximumJensenFamily.exists_diagonal line 71
9. lemma OAI.WeakMTWTransport.MaximumDiagonal.limits line 80