IndisputableMonolith.Algebra.CostAlgebra — Recognition explainer

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Algebra.PhiRing module_import
IndisputableMonolith.Algebra.RecognitionCategory module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.FunctionalEquation module_import
IndisputableMonolith.Cost.FunctionalEquationAczel module_import

declarations in this module (94)

def J L63
theorem J_at_one L66
theorem J_reciprocal L71
theorem J_nonneg L75
theorem J_defect_form L79
def SatisfiesRCL L92
theorem RCL_holds L98
def costCompose L115
theorem costCompose_comm L121
theorem costCompose_assoc_defect L126
theorem costCompose_flexible L132
theorem costCompose_zero_left L136
theorem costCompose_zero_right L140
theorem costCompose_nonneg L146
theorem costCompose_factored L156
theorem costCompose_no_identity L161
theorem costCompose_power_assoc L175
theorem costCompose_fourfold_power_counterexample L179
def H L188
theorem H_at_one L191
theorem H_dAlembert L199
abbrev ShiftedCarrier L222
def shiftedCompose L225
def shiftedUnit L232
theorem shiftedUnit_val L236
theorem shiftedCompose_val L238
theorem H_ge_one L262
def shiftedOfH L268
abbrev ShiftedHValue L274
def shiftedComposeH L277
theorem shiftedComposeH_val L283
def shiftedHValueOf L298
def defectDist L310
theorem defectDist_self L313
theorem defectDist_symm L319
theorem defectDist_nonneg L328
theorem J_le_J_of_inv_le_le L336
theorem defectDist_le_J_of_ratio_bounds L361
theorem quasiTriangleConstant_eq L369
theorem defectDist_quasi_triangle_local L376
theorem defectDist_no_global_quasi_triangle L426
theorem costCompose_sub_left L490
theorem costCompose_left_cancel L496
theorem costCompose_right_cancel L509
def PositiveDomain L517
structure RecognitionCostSystem L521
def canonicalSigma L530
def canonicalRecognitionCostSystem L534
theorem canonicalRecognitionCostSystem_domain L543
theorem canonicalRecognitionCostSystem_cost_one L547
theorem canonicalRecognitionCostSystem_cost_inv L552
def seqShift L559
def windowSums L562
theorem windowSums_shift_equivariant L567
structure CostAlgebraData L589
def canonicalCostAlgebra L602
theorem cost_algebra_unique L612
theorem cost_algebra_unique_aczel L641
structure CostMorphism L655
def reciprocalAuto L688
theorem reciprocal_involution L691
theorem reciprocal_preserves_cost L697
theorem J_eq_iff_eq_or_inv L704
abbrev PosReal L732
def posMul L735
def posInv L739
def posOne L743
def posTwo L744
def posHalf L745
theorem posInv_inv L747
theorem posInv_one L751
theorem posInv_two L755
theorem posInv_half L759
def JAut L764
theorem multiplicative L774
theorem preserves_cost L779
theorem ext L783
def id L789
def reciprocal L798
def comp L808

… and 14 more