module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.RecognitionLowerBound
show as:
view Lean formalization →
used by (1)
depends on (1)
declarations in this module (11)
-
def
MagnitudeOnlyObservable -
def
productMagnitudeObservable -
theorem
productMagnitudeObservable_magnitudeOnly -
theorem
leftFactorObservable_not_magnitudeOnly -
theorem
rightFactorObservable_not_magnitudeOnly -
def
productMagnitudePostprocess -
theorem
productMagnitudePostprocess_magnitudeOnly -
theorem
no_productMagnitudePostprocess_extracts_left_factor -
theorem
no_productMagnitudePostprocess_extracts_right_factor -
structure
RecognitionLowerBoundCertificate -
theorem
recognition_lower_bound_certificate