module
module
IndisputableMonolith.Cost.JcostCore
show as:
view Lean formalization →
used by (22)
-
IndisputableMonolith.Complexity.TuringBridge -
IndisputableMonolith.Cost.FrequencyLadder -
IndisputableMonolith.Ethics.MoralDebt -
IndisputableMonolith.Foundation.HamiltonianEmergence -
IndisputableMonolith.Foundation.JCostGeometry -
IndisputableMonolith.Foundation.RHatFixedPoint -
IndisputableMonolith.Foundation.SpinStatistics -
IndisputableMonolith.Gravity.GravitationalLensing -
IndisputableMonolith.Gravity.UltramassiveBH -
IndisputableMonolith.Information.RecognitionEntropy -
IndisputableMonolith.Physics.AnomalousMagneticMoment -
IndisputableMonolith.Physics.BAO -
IndisputableMonolith.Physics.CMBTemperature -
IndisputableMonolith.Physics.CooperPair -
IndisputableMonolith.Physics.GammaRayBursts -
IndisputableMonolith.Physics.NeutronStarTOV -
IndisputableMonolith.Physics.NoHairTheorem -
IndisputableMonolith.Physics.ProtonRadius -
IndisputableMonolith.Physics.QuantumHallEffect -
IndisputableMonolith.Physics.RunningCouplings -
IndisputableMonolith.Physics.StellarEvolution -
IndisputableMonolith.Physics.Superfluidity
declarations in this module (22)
-
def
Jcost -
structure
CostRequirements -
lemma
Jcost_unit0 -
lemma
Jcost_symm -
lemma
Jcost_eq_sq -
lemma
Jcost_nonneg -
lemma
Jcost_one_plus_eps_quadratic -
lemma
Jcost_small_strain_bound -
def
AgreesOnExp -
lemma
Jcost_exp -
class
SymmUnit -
class
AveragingAgree -
class
AveragingDerivation -
class
AveragingBounds -
def
mkAveragingBounds -
class
JensenSketch -
def
F_ofLog -
class
LogModel -
theorem
Jcost_agrees_on_exp -
lemma
Jcost_deriv -
lemma
Jcost_strict_mono_on_one_infty -
lemma
Jcost_pos_of_ne_one