module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaAmplitude`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (4)

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

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeAnalysis module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeStrongClosure module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSComplexAmplitude module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ObjecthoodRegistry module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability module_import

declarations in this module (20)

abbrev Amp L28
abbrev ComplexAmp L31
def normSq L34
def bornWeight L38
def Normalized L42
theorem bornWeight_nonneg L44
theorem normSq_nonneg L49
theorem born_weights_sum_one L54
def NormPreserving L61
theorem normalized_of_normPreserving L64
theorem delta_amplitude_headline L72
def complexBornWeight L84
def complexNormSq L88
def ComplexNormalized L92
theorem complexBornWeight_nonneg L94
theorem complexNormSq_nonneg L99
theorem complex_born_weights_sum_one L103
def ComplexNormPreserving L109
theorem complex_normalized_of_normPreserving L112
theorem delta_complex_amplitude_headline L122