Pith. sign in

Cost

Reciprocal-symmetric cost. Uniqueness of J(x) = ½(x + x⁻¹) − 1, convexity, the Aczél class, and the d'Alembert factorization.

46 modules · 516 thm/lemma · 10200 lines
module thm lemma def lines papers
Cost 21 28 6 688 444
Cost.AczelClass 1 0 0 57 -
Cost.AczelClassification 7 0 1 124 -
Cost.AczelProof 7 7 1 415 -
Cost.AczelTheorem 10 7 2 465 -
Cost.Calibration 3 5 0 69 -
Cost.CauchyAuxiliary 4 0 3 150 -
Cost.ClassicalResults 9 2 0 152 -
Cost.ContDiffReduction 7 3 0 248 -
Cost.Convexity 5 7 2 160 5
Cost.Derivative 3 5 2 141 -
Cost.FrequencyLadder 5 0 3 104 -
Cost.FunctionalEquation 35 18 16 1356 27900
Cost.FunctionalEquationAczel 1 0 0 46 -
Cost.FunctionalEquationStrict 2 0 0 60 -
Cost.GaugeOrbitClassification 17 0 0 399 -
Cost.GaugeOrbitFromRealCharacter 35 0 6 479 -
Cost.JcostCore 1 1 0 67 51
Cost.JcostLogic 7 0 3 113 -
Cost.JensenSketch 0 0 0 26 -
Cost.Jlog 1 6 1 62 -
Cost.MonotoneMultiplicativePower 8 0 0 192 -
Cost.Ndim.BlockReduction 6 0 3 202 -
Cost.Ndim.Bridge 4 0 3 65 -
Cost.Ndim.Calibration 4 0 3 66 -
Cost.Ndim.Connections 5 0 4 82 -
Cost.Ndim.Core 11 0 8 141 -
Cost.Ndim.CurvatureBridge 10 0 5 422 -
Cost.Ndim.DAlembert 1 1 0 62 -
Cost.Ndim.Hessian 7 0 7 120 -
Cost.Ndim.Metric 2 0 1 31 -
Cost.Ndim.Neutrality 3 0 0 39 -
Cost.Ndim.Octave 1 0 2 32 -
Cost.Ndim.Projector 21 0 7 311 -
Cost.Ndim.RadicalDistribution 11 0 3 136 -
Cost.Ndim.RicciScalar 5 0 3 96 -
Cost.Ndim.ScalarCertificates 10 0 9 299 -
Cost.Ndim.Symmetry 2 0 1 34 -
Cost.Ndim.Uniqueness 2 0 1 46 -
Cost.Ndim.XCoordinates 8 0 6 154 -
Cost.OscillatoryBranchAudit 10 0 1 139 -
Cost.RealCharacterFactorization 55 0 14 990 -
Cost.RealTraceRoot 11 0 1 190 -
Cost.SymplecticAction 19 0 5 312 -
Cost.TraceRationalExponent 7 0 1 285 -
Cost.UnitFromMinimality 17 5 2 373 -

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