ModulusRigidity

theorem HermitekLEAN.leading_term_extraction {N : ℕ} {α : ℂ} {q : ℝ → ℂ} : (∀ (ε : ℝ), 0 < ε → ∃ (R0 : ℝ), ∀ r ≥ R0, ‖q r / ↑r ^ N‖ ≤ ε) → (∃ (R0 : ℝ), ∀ r ≥ R0, α * ↑r ^ N + q r = 0) → α = 0

If a unique top-order term survives asymptotically, its coefficient must vanish.

theorem HermitekLEAN.growth_forces_finite {k d : ℕ} (a : Fin (d + 1) → ℂ) (_hTop : topCoeff a ≠ 0) {G : ℂ → ℂ} : G ∈ Hk k → (∀ (z : ℂ), ‖G z‖ = ‖finiteHermiteSum k a z‖) → ∀ (n : ℕ), d < n → hermiteCoeff k G n = 0

Modulus equality against a finite Hermite sum forces vanishing of high Hermite coefficients.

theorem HermitekLEAN.finite_modulus_rigidity {k d : ℕ} (a b : Fin (d + 1) → ℂ) (_hTop : topCoeff a ≠ 0) : (∀ (z : ℂ), ‖finiteHermiteSum k b z‖ = ‖finiteHermiteSum k a z‖) → ∃ (w : ℂ), ‖w‖ = 1 ∧ finiteHermiteSum k b = w • finiteHermiteSum k a

Finite modulus rigidity up to a unimodular scalar.

theorem HermitekLEAN.modulus_rigidity {k d : ℕ} (a : Fin (d + 1) → ℂ) (_hTop : topCoeff a ≠ 0) {G : ℂ → ℂ} : G ∈ Hk k → (∀ (z : ℂ), ‖G z‖ = ‖finiteHermiteSum k a z‖) → ∃ (w : ℂ), ‖w‖ = 1 ∧ G = w • finiteHermiteSum k a

Full modulus rigidity inside H_k.

theorem HermitekLEAN.real_part_rigidity {k d : ℕ} (a : Fin (d + 1) → ℂ) (_hTop : topCoeff a ≠ 0) {G : ℂ → ℂ} : G ∈ Hk k → (∀ (z : ℂ), (G z * star (finiteHermiteSum k a z)).re = 0) → ∃ (c : ℝ), G = (Complex.I * ↑c) • finiteHermiteSum k a