Complex.Hadamard.norm_inv_hadamardDenominator_le_exp_on_cartan_circle

theorem norm_inv_hadamardDenominator_le_exp_on_cartan_circle    {f : ℂ → ℂ} {ρ τ : ℝ} {m : ℕ}    (hmρ : (m : ℝ) ≤ ρ) (hτ : ρ < τ) (hτ_lt : τ < (m + 1 : ℝ))    (hτ_nonneg : 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‖⁻¹ ^ τ)) :    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 →      ∀ (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 →          ‖(u ^ analyticOrderNatAt f 0 *              divisorCanonicalProduct m f (Set.univ : Set ℂ) u)⁻¹‖            ≤ Real.exp (Cprod * (1 + r) ^ τ) := by  classical  intro Sτ Cprod R r hRpos hRle hR_le_r hr_le_2R 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 hr1 : (1 : ℝ) ≤ r := le_trans hRle hR_le_r  have hpow_inv_le1 : ‖(u ^ analyticOrderNatAt f 0)⁻¹‖ ≤ 1 :=    Complex.norm_inv_pow_le_one_of_one_le_norm u (analyticOrderNatAt f 0) (by simpa [hur] using hr1)  let fac : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℂ :=    fun p => weierstrassFactor m (u / divisorZeroIndex₀_val p)  have hloc :      HasProdLocallyUniformlyOn        (fun (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) (w : ℂ) =>          weierstrassFactor m (w / divisorZeroIndex₀_val p))        (divisorCanonicalProduct m f (Set.univ : Set ℂ))        (Set.univ : Set ℂ) :=    hasProdLocallyUniformlyOn_divisorCanonicalProduct_univ (m := m) (f := f) h_sum  have hprod :      HasProd fac (divisorCanonicalProduct m f (Set.univ : Set ℂ) u) :=    hloc.hasProd (by simp : u ∈ (Set.univ : Set ℂ))  let ap : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℝ := fun p => ‖divisorZeroIndex₀_val p‖  haveI : DecidablePred (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) => p ∈ small) :=    Classical.decPred _  let b : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℝ :=    fun p =>      if hp : p ∈ small then        CartanBound.φ (r / ap p) + (m : ℝ) * (1 + (r / ap p) ^ τ)      else        (2 : ℝ) * (r / ap p) ^ τ  have hterm : ∀ p, ‖(fac p)⁻¹‖ ≤ Real.exp (b p) := by    intro p    by_cases hp : p ∈ small    · have hval_ne : r ≠ ap p := by        intro hEq        have : r ∈ bad := by          refine Finset.mem_image.2 ⟨p, hp, ?_⟩          simp [ap, a, hEq]        exact (hr_not_bad' this).elim      have hval0 : divisorZeroIndex₀_val p ≠ 0 := divisorZeroIndex₀_val_ne_zero p      have hmτ : (m : ℝ) ≤ τ := le_trans hmρ (le_of_lt hτ)      have hnear :          ‖(weierstrassFactor m (u / divisorZeroIndex₀_val p))⁻¹‖            ≤ Real.exp (CartanBound.φ (r / ap p) + (m : ℝ) * (1 + (r / ap p) ^ τ)) := by        simpa [ap] using          (norm_inv_weierstrassFactor_le_exp_near (m := m) (τ := τ) (r := r)              (u := u) (a := divisorZeroIndex₀_val p)              (hur := hur) (ha := hval0) (hr := by simpa [ap] using hval_ne) hmτ)      simpa [fac, b, hp] using hnear    · have hlarge : (4 * R : ℝ) < ap p := by        have : ¬ap p ≤ 4 * R := by          intro hle          have : p ∈ small := by            have hp_mem : p ∈ smallSet := by              simpa [hsmallSet, ap] using hle            simpa [small] using (hsmall_fin.mem_toFinset.2 hp_mem)          exact hp this        exact lt_of_not_ge this      have hz' : ‖u / divisorZeroIndex₀_val p‖ ≤ (1 / 2 : ℝ) :=        norm_div_le_half_of_norm_le_of_two_mul_lt (z := u) (a := divisorZeroIndex₀_val p)          (R := 2 * R) (by nlinarith [hRpos]) (by rw [hur]; exact hr_le_2R)          (by nlinarith [hlarge])      have hτ_le : τ ≤ (m + 1 : ℝ) := le_of_lt hτ_lt      have hfar :          ‖(weierstrassFactor m (u / divisorZeroIndex₀_val p))⁻¹‖ ≤            Real.exp ((2 : ℝ) * (r / ap p) ^ τ) := by        simpa [ap] using          (norm_inv_weierstrassFactor_le_exp_far (m := m) (τ := τ) (r := r)              (u := u) (a := divisorZeroIndex₀_val p)              (hur := hur) (ha := divisorZeroIndex₀_val_ne_zero p) (hz := hz') hτ_le)      simpa [fac, b, hp] using hfar  have hb_le :      ∀ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)),        (∑ p ∈ s, b p) ≤ Cprod * (1 + r) ^ τ := by    intro s    simpa [small, ap, b, Sτ, Cprod, a, hsmallSet] using      (Complex.Hadamard.cartan_sum_majorant_le (f := f) (m := m) (τ := τ) (R := R) (r := r)        (hRpos := hRpos) (hrpos := lt_of_lt_of_le hRpos hR_le_r)        (hR_le_r := hR_le_r) (hτ_nonneg := hτ_nonneg)        (smallSet := smallSet) (hsmall_fin := hsmall_fin) (hsmallSet := hsmallSet)        (hsumτ := hsumτ)        (hr_phi := by          simpa [small, a, one_mul] using hr_phi)        s)  have hcprod_inv :      ‖(divisorCanonicalProduct m f (Set.univ : Set ℂ) u)⁻¹‖ ≤        Real.exp (Cprod * (1 + r) ^ τ) := by    refine hasProd_norm_inv_le_exp_of_pointwise_le_exp      (α := divisorZeroIndex₀ f (Set.univ : Set ℂ)) (fac := fac)      (F := divisorCanonicalProduct m f (Set.univ : Set ℂ) u)      hprod (b := b) (B := Cprod * (1 + r) ^ τ) ?_ ?_    · exact hterm    · intro s      exact hb_le s  have hmul :      ‖(u ^ analyticOrderNatAt f 0 *          divisorCanonicalProduct m f (Set.univ : Set ℂ) u)⁻¹‖        =      ‖(u ^ analyticOrderNatAt f 0)⁻¹‖ *        ‖(divisorCanonicalProduct m f (Set.univ : Set ℂ) u)⁻¹‖ := by    simp [mul_inv_rev, mul_comm]  rw [hmul]  have :      ‖(u ^ analyticOrderNatAt f 0)⁻¹‖ *          ‖(divisorCanonicalProduct m f (Set.univ : Set ℂ) u)⁻¹‖        ≤ 1 * Real.exp (Cprod * (1 + r) ^ τ) :=    mul_le_mul hpow_inv_le1 hcprod_inv (by positivity) (by positivity)  simpa using this