def HessianDegeneracy.triadicHessian (k p q : Fin 3 → ℝ) : Fin 3 → Fin 3 → ℝ

The Triadic Hessian Matrix $\mathcal{H}_\Psi$. Derived by differentiating the triadic phase function with respect to continuous frequency variables $r$ on the continuous interpolation of the Torus.

Equations

• HessianDegeneracy.triadicHessian k p q x✝¹ x✝ = 0

def HessianDegeneracy.isMorseZone (delta : ℝ) (r k : Fin 3 → ℝ) : Prop

Morse Zone vs Cusp Zone partitioning. The proof relies on splitting the integration domain where the Hessian determinant $|\det \mathcal{H}_\Psi|$ is strictly bounded away from zero.

Equations

• HessianDegeneracy.isMorseZone delta r k = True

def HessianDegeneracy.restrictedHessian (j : ℕ) (k : Fin 3 → ℝ) : Fin 2 → Fin 2 → ℝ

Restricting the Hessian to the tangent space of the dyadic sphere $S^2_j$.

Equations

• HessianDegeneracy.restrictedHessian j k x✝¹ x✝ = 0

structure HessianDegeneracy.UniformOscillatoryGain (j : ℕ) : Type

The assertion that the restricted Hessian has determinant bounded below by a constant depending on the zone separation, yielding the Van Der Corput gain.

• gain_bound : ℝ
• is_bounded : self.gain_bound ≤ 2 ^ (-↑j / 2)