Pith. sign in

Information

Information modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.

53 modules · 319 thm/lemma · 5972 lines
module thm lemma def lines papers
Information 0 0 2 49 4
Information.AlgorithmicProb3FromJCost 4 0 3 36 -
Information.Bandwidth_Phi_RS 4 0 3 36 -
Information.ChannelCapacity 9 0 8 288 -
Information.ChannelCapacity2FromJCost 4 0 3 36 -
Information.Channel_Capacity_Qubit_RS 4 0 3 36 -
Information.ChurchTuring 7 0 4 252 -
Information.ChurchTuringPhysicsStructure 14 0 6 190 -
Information.Compression 5 2 15 252 -
Information.Compression3DeepFromJCost 4 0 3 36 -
Information.CompressionPrior 1 0 2 28 -
Information.Compression_Ratio_RS 4 0 3 36 -
Information.ComputationLimitsStructure 17 0 9 207 -
Information.DNA_Storage_Density_RS 4 0 3 36 -
Information.DataCompression3FromJCost 4 0 3 36 -
Information.EMLFromRecognition 9 0 6 133 -
Information.ErrorCorrection3DeepFromJCost 4 0 3 36 -
Information.ErrorCorrectionBounds 8 0 8 240 -
Information.ErrorCorrectionCodesFromJCost 3 0 2 61 -
Information.FEPBridgeFromJCost 9 0 4 151 -
Information.HelmholtzDecomposition 2 0 3 49 -
Information.Holevo_Bound_RS 4 0 3 36 -
Information.Information 4 0 3 36 -
Information.InformationIsLedger 22 1 6 298 -
Information.Internet_Traffic_RS 4 0 3 36 -
Information.JCostNecessity 2 0 0 58 -
Information.KolmogorovComplexity3FromJCost 4 0 3 36 -
Information.Kolmogorov_Complexity_RS 4 0 3 36 -
Information.LDPCCodeRateFromJCost 4 0 3 51 -
Information.LDPCCodeRateFromPhi 6 0 3 112 -
Information.LandauerBound 9 0 14 244 -
Information.LocalCache 9 0 7 281 -
Information.Moore_Law_RS 4 0 3 36 -
Information.MutualInfo2FromJCost 4 0 3 36 -
Information.NESSConditionalIndependenceMeasure 3 0 6 118 -
Information.NetworkTopologyFromSigma 3 0 2 61 -
Information.NoCloning 12 2 3 240 -
Information.PhiHierarchyGrowth 12 0 2 197 -
Information.PhysicsComplexityStructure 17 1 5 256 -
Information.PolarCodeGapFromPhi 3 0 3 66 -
Information.QECThresholdFromPhiLadder 3 0 2 54 -
Information.QuantumChannelCapacityFromPhi 3 0 2 90 -
Information.QuantumErrorCorrection 1 0 7 256 -
Information.QuantumErrorCorrectionThreshold 3 0 2 69 -
Information.Quantum_Error_Rate_RS 4 0 3 36 -
Information.RecognitionBremermann 7 0 2 77 -
Information.ShannonAsJCostLimit 4 0 4 120 -
Information.ShannonEntropy 9 0 8 248 -
Information.ShannonEntropy3FromJCost 4 0 3 36 -
Information.ShannonHighNLimit 6 0 1 187 -
Information.Shannon_Entropy_Max_RS 4 0 3 36 -
Information.SimulationHypothesisStructure 12 0 5 207 -
Information.Thermodynamics 3 0 5 98 -

full source mirrored from github.com/jonwashburn/shape-of-logic