Order bounds from max-modulus bounds.

This file isolates a general lemma that converts an eventual max-modulus bound

maxModulus f r ≤ exp (r ^ ρ)

into an order bound order f ≤ ρ, where order is the limsup definition from LZC/HadamardFactorization/Basic.lean.

It is used in the order-≤ 1 Hadamard factorization proof to show the quotient Q := f / P has order Q < 2, hence is an exponential of a linear function.

A coboundedness helper for the order auxiliary function

Order bound from an eventual max-modulus bound

theorem Hadamard.order_le_of_eventually_maxModulus_le_exp_rpow (f : ℂ → ℂ) (ρ : ℝ) (hρ : 0 ≤ ρ) (hf : Differentiable ℂ f) (h : ∀ᶠ (r : ℝ) in Filter.atTop, maxModulus f r ≤ Real.exp (r ^ ρ)) : order f ≤ ρ

Order bounds from a ρ + ε max-modulus family

If we can bound maxModulus f r by exp(r^(ρ+ε)) for every ε > 0, then order f ≤ ρ.

This packages the exact “max-modulus form” pipeline used for order-≤ 1 goals: prove the family of bounds, then apply order_le_of_eventually_maxModulus_le_exp_rpow at exponent ρ+ε, and finally let ε → 0 using le_of_forall_pos_le_add.

theorem Hadamard.order_le_of_forall_pos_eventually_maxModulus_le_exp_rpow_add (f : ℂ → ℂ) (ρ : ℝ) (hρ : 0 ≤ ρ) (hf : Differentiable ℂ f) (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (r : ℝ) in Filter.atTop, maxModulus f r ≤ Real.exp (r ^ (ρ + ε))) : order f ≤ ρ

A convenient specialization for order-≤ 1 (the β use-case).

theorem Hadamard.order_le_one_of_forall_pos_eventually_maxModulus_le_exp_rpow_one_add (f : ℂ → ℂ) (hf : Differentiable ℂ f) (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (r : ℝ) in Filter.atTop, maxModulus f r ≤ Real.exp (r ^ (1 + ε))) : order f ≤ 1