module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSComplexAmplitude
show as:
view Lean formalization →
used by (3)
depends on (2)
declarations in this module (15)
-
structure
FRSIExpr -
def
eval -
theorem
eval_re -
theorem
eval_im -
theorem
eval_re_mem -
theorem
eval_im_mem -
abbrev
FRSIAmp -
def
displayAmp -
def
bornWeight -
theorem
display_bornWeight_eq -
theorem
display_normSq_eq -
theorem
bornWeight_nonneg -
def
Normalized -
theorem
normalized_iff_display -
theorem
frsi_amplitude_headline