Complex.Hadamard.hadamardQuotient_norm_le_exp_on_cartan_circle

theorem hadamardQuotient_norm_le_exp_on_cartan_circle    {f H : ℂ → ℂ} {ρ τ : ℝ} {m : ℕ} {Cf : ℝ}    (hmρ : (m : ℝ) ≤ ρ) (hτ : ρ < τ) (hτ_lt : τ < (m + 1 : ℝ))    (hτ_nonneg : 0 ≤ τ) (hentire : Differentiable ℂ f)    (hnot : ∃ z : ℂ, f z ≠ 0)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (hsumτ : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ))    (hf_boundτ : ∀ z : ℂ, ‖f z‖ ≤ Real.exp (Cf * (1 + ‖z‖) ^ τ))    (hfactor : ∀ z : ℂ,      f z =        H z * z ^ analyticOrderNatAt f 0 *          divisorCanonicalProduct m f (Set.univ : Set ℂ) z) :    let Sτ : ℝ :=      ∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ), ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ    let Cprod : ℝ := cartanProductConstant m τ Sτ    ∀ {R r : ℝ}, 0 < R → 1 ≤ R → R ≤ r → r ≤ 2 * R → 0 < r →      ∀ (smallSet : Set (divisorZeroIndex₀ f (Set.univ : Set ℂ)))        (hsmall_fin : smallSet.Finite),        smallSet =            {p : divisorZeroIndex₀ f (Set.univ : Set ℂ) |              ‖divisorZeroIndex₀_val p‖ ≤ 4 * R} →        (let small : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) := hsmall_fin.toFinset         let a : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℝ :=          fun p => ‖divisorZeroIndex₀_val p‖         r ∉ small.image a) →        (let small : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) := hsmall_fin.toFinset         let a : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℝ :=          fun p => ‖divisorZeroIndex₀_val p‖         (∑ p ∈ small, (1 : ℝ) * CartanBound.φ (r / a p)) ≤          CartanBound.Cφ * (small.card : ℝ)) →        ∀ u : ℂ, ‖u‖ = r → ‖H u‖ ≤ Real.exp ((Cf + Cprod + 10) * (1 + r) ^ τ) := by  classical  intro Sτ Cprod R r hRpos hRle hR_le_r hr_le_2R hrpos smallSet hsmall_fin    hsmallSet hr_not_bad hr_phi u hur  let small : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) := hsmall_fin.toFinset  let a : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℝ := fun p => ‖divisorZeroIndex₀_val p‖  let bad : Finset ℝ := small.image a  have hr_not_bad' : r ∉ bad := by    simpa [bad, small, a] using hr_not_bad  have hden_eq :      f u =        H u * (u ^ analyticOrderNatAt f 0 *          divisorCanonicalProduct m f (Set.univ : Set ℂ) u) := by    simpa [mul_assoc, mul_left_comm, mul_comm] using (hfactor u)  have hfu_ne : f u ≠ 0 := by    have hr_le_4R : r ≤ 4 * R := by nlinarith [hr_le_2R, hRpos]    exact no_zero_on_sphere_of_norm_image_avoid (f := f) hentire hnot      (B := 4 * R) (r := r) hrpos hr_le_4R smallSet hsmall_fin hsmallSet      (by simpa [small, a] using hr_not_bad) u hur  have hden_ne :      (u ^ analyticOrderNatAt f 0 *        divisorCanonicalProduct m f (Set.univ : Set ℂ) u) ≠ 0 := by    intro hden0    have : f u = 0 := by simpa [hden0] using hden_eq    exact hfu_ne this  have hHu :      H u =        f u / (u ^ analyticOrderNatAt f 0 *          divisorCanonicalProduct m f (Set.univ : Set ℂ) u) := by    exact eq_div_of_mul_eq hden_ne (Eq.symm hden_eq)  have hf_u : ‖f u‖ ≤ Real.exp (Cf * (1 + r) ^ τ) := by    simpa [hur] using hf_boundτ u  have hden_inv :      ‖(u ^ analyticOrderNatAt f 0 *          divisorCanonicalProduct m f (Set.univ : Set ℂ) u)⁻¹‖        ≤ Real.exp (Cprod * (1 + r) ^ τ) := by    simpa [Sτ, Cprod] using      (norm_inv_hadamardDenominator_le_exp_on_cartan_circle        (f := f) (ρ := ρ) (τ := τ) (m := m)        hmρ hτ hτ_lt hτ_nonneg h_sum hsumτ        (R := R) (r := r) hRpos hRle hR_le_r hr_le_2R        smallSet hsmall_fin hsmallSet        (by simpa [small, a] using hr_not_bad)        (by simpa [small, a, one_mul] using hr_phi)        u hur)  have :      ‖H u‖ ≤        ‖f u‖ *          ‖(u ^ analyticOrderNatAt f 0 *            divisorCanonicalProduct m f (Set.univ : Set ℂ) u)⁻¹‖ := by    have :        ‖H u‖ =          ‖f u /            (u ^ analyticOrderNatAt f 0 *              divisorCanonicalProduct m f (Set.univ : Set ℂ) u)‖ := by      simp [hHu]    simp [div_eq_mul_inv, norm_inv, this]  have hmul :      ‖f u‖ *          ‖(u ^ analyticOrderNatAt f 0 *            divisorCanonicalProduct m f (Set.univ : Set ℂ) u)⁻¹‖        ≤ Real.exp (Cf * (1 + r) ^ τ) * Real.exp (Cprod * (1 + r) ^ τ) :=    mul_le_mul hf_u hden_inv (by positivity) (by positivity)  have hexp :      Real.exp (Cf * (1 + r) ^ τ) * Real.exp (Cprod * (1 + r) ^ τ)        = Real.exp ((Cf + Cprod) * (1 + r) ^ τ) := by    simp [Real.exp_add, add_mul, add_comm]  have : ‖H u‖ ≤ Real.exp ((Cf + Cprod) * (1 + r) ^ τ) :=    (this.trans hmul).trans_eq hexp  have hslack :      Real.exp ((Cf + Cprod) * (1 + r) ^ τ) ≤        Real.exp ((Cf + Cprod + 10) * (1 + r) ^ τ) := by    refine Real.exp_le_exp.2 ?_    have hnn : 0 ≤ (1 + r) ^ τ := by positivity    nlinarith  exact this.trans hslack