Complex.Hadamard.cartan_card_small_le

lemma cartan_card_small_le    {f : ℂ → ℂ} {τ R : ℝ} (hRpos : 0 < R) (hτ_nonneg : 0 ≤ τ)    (small : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)))    (hsmall : ∀ p ∈ small, ‖divisorZeroIndex₀_val p‖ ≤ 4 * R)    (hsumτ :      Summable        (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>          ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ)) :    (small.card : ℝ)      ≤ (4 * R) ^ τ          * ((∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ),                ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ) + 1) := by  classical  set Sτ : ℝ :=    ∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ), ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ  have hsum_le : (∑ p ∈ small, ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ) ≤ Sτ := by    have hnn :        ∀ p : divisorZeroIndex₀ f (Set.univ : Set ℂ),          0 ≤ ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ := by      intro p      exact Real.rpow_nonneg (inv_nonneg.2 (norm_nonneg _)) _    simpa [Sτ] using      (Summable.sum_le_tsum (s := small)        (f := fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>          ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ)        (fun p _ => hnn p) hsumτ)  have hgeom_sum :      (small.card : ℝ) ≤ ∑ p ∈ small, (4 * R) ^ τ * ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ := by    have hcard_eq : (small.card : ℝ) = ∑ p ∈ small, (1 : ℝ) := by simp    rw [hcard_eq]    refine Finset.sum_le_sum (fun p hp => ?_)    have hp_le : ‖divisorZeroIndex₀_val p‖ ≤ 4 * R := hsmall p hp    have hap : 0 < ‖divisorZeroIndex₀_val p‖ :=      norm_pos_iff.2 (divisorZeroIndex₀_val_ne_zero p)    have hbase : (1 : ℝ) ≤ (4 * R) / ‖divisorZeroIndex₀_val p‖ := by      exact (le_div_iff₀ hap).2 (by simpa [mul_one] using hp_le)    have : (1 : ℝ) ≤ ((4 * R) / ‖divisorZeroIndex₀_val p‖) ^ τ :=      Real.one_le_rpow hbase hτ_nonneg    have hdiv :        ((4 * R) / ‖divisorZeroIndex₀_val p‖) ^ τ =          (4 * R) ^ τ * (‖divisorZeroIndex₀_val p‖)⁻¹ ^ τ := by      have h4 : 0 ≤ (4 * R : ℝ) := by nlinarith [le_of_lt hRpos]      have ha : 0 ≤ (‖divisorZeroIndex₀_val p‖ : ℝ)⁻¹ := by positivity      simpa [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using        (Real.mul_rpow (x := (4 * R : ℝ))          (y := (‖divisorZeroIndex₀_val p‖ : ℝ)⁻¹) (z := τ) h4 ha)    have : (1 : ℝ) ≤ (4 * R) ^ τ * ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ := by      simpa [hdiv] using this    exact this  have hgeom :      (small.card : ℝ) ≤ (4 * R) ^ τ * (∑ p ∈ small, ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ) := by    simpa [Finset.mul_sum] using hgeom_sum  have hsmall_le : (small.card : ℝ) ≤ (4 * R) ^ τ * Sτ := by    exact hgeom.trans (mul_le_mul_of_nonneg_left hsum_le (by positivity))  have hS_le : (4 * R) ^ τ * Sτ ≤ (4 * R) ^ τ * (Sτ + 1) := by    refine mul_le_mul_of_nonneg_left ?_ (by positivity)    linarith  have : (small.card : ℝ) ≤ (4 * R) ^ τ * (Sτ + 1) := hsmall_le.trans hS_le  simpa [Sτ, add_comm, add_left_comm, add_assoc, mul_assoc] using this