OAI/Analysis/BiholderTransport/Regularity/MaximumReindex.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.WeakMTWTransport.MaximumJensenFamily.compline 24 - def
OAI.WeakMTWTransport.MaximumDiagonal.compline 32 - lemma
OAI.WeakMTWTransport.MaximumJensenFamily.sampleProjectionline 49 - lemma
OAI.WeakMTWTransport.MaximumDiagonal.endpointSourceline 57 - lemma
OAI.WeakMTWTransport.MaximumDiagonal.endpointChartline 64