OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ChargePivotAbsorption.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.charge_pivot_absorption line 21
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.chargedWeight line 36
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.chargedCodeWeight line 39
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.chargedCodeWeight_nonneg line 43
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.chargedWeight_le_code line 50
6. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.RecordPacket.charged_record_sum_le_codes line 60