OAI/Analysis/FreeWords/TraceTransfer.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.KKTraceTransfer.trace_square_nonnegline 73 - lemma
OAI.KKTraceTransfer.traceNorm_sqline 78 - lemma
OAI.KKTraceTransfer.trace_square_tendstoline 86 - theorem
OAI.KKTraceTransfer.trace_transferline 96