OAI/Combinatorics/Chromatic/Walls/IncomingTransportTrace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.FormalLog.inverse_coeff_congr line 11
2. lemma OAI.ElementaryPositivity.FormalLog.log_one line 22
3. lemma OAI.ElementaryPositivity.QuantumTorus.chartNegative_log_positive line 36
4. lemma OAI.ElementaryPositivity.QuantumTorus.chartNegative_log_negative_kernel line 45
5. lemma OAI.ElementaryPositivity.QuantumTorus.kernel_trace_log_inverse line 73
6. lemma OAI.ElementaryPositivity.QuantumTorus.incoming_negative_ratio_log line 86