Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section24.Sensitivity.Semantics

Semantics #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Section 2.4 sensitivity: semantic import hub for provider modules #

Import hub collecting the proved semantic units (frozen definition and characterization files together with the public Section 2.4 A modules) needed by the Section 2.4 sensitivity provider modules.

Cycle-safety rule #

Provider modules import this file, never Algsuperdiff.Section24.Sensitivity.Vocabulary. Vocabulary is imported by the frozen sensitivity anchors, so a provider importing it (directly or transitively) would create an import cycle when the anchors are onto their providers. Accordingly, this file must never import Vocabulary or any frozen sensitivity anchor (ResponseJDerivative, CoarseMatrixDerivativeBound, LambdaSensitivity, ResponseJSensitivity, BigLambdaSensitivity, BigLambdaSensitivityAtDelta, LambdaSensitivityUnconditional, ResponseJSensitivityUnconditional).