LogDerivLems

theorem logDeriv_tprod_eq_tsum2 {s : Set ℂ} (hs : IsOpen s) (x : ↑s) (f : ℕ → ℂ → ℂ) (hf : ∀ (i : ℕ), f i ↑x ≠ 0) (hd : ∀ (i : ℕ), DifferentiableOn ℂ (f i) s) (hm : Summable fun (i : ℕ) => logDeriv (f i) ↑x) (htend : MultipliableLocallyUniformlyOn f s) (hnez : ∏' (i : ℕ), f i ↑x ≠ 0) : logDeriv (fun (x : ℂ) => ∏' (i : ℕ), f i x) ↑x = ∑' (i : ℕ), logDeriv (f i) ↑x

theorem logDeriv_tprod_eq_tsumold {s : Set ℂ} (hs : IsOpen s) (x : ↑s) (f : ℕ → ℂ → ℂ) (hf : ∀ (i : ℕ), f i ↑x ≠ 0) (hd : ∀ (i : ℕ), DifferentiableOn ℂ (f i) s) (hm : Summable fun (i : ℕ) => logDeriv (f i) ↑x) (htend : TendstoLocallyUniformlyOn (fun (n : ℕ) => ∏ i ∈ Finset.range n, f i) (fun (x : ℂ) => ∏' (i : ℕ), f i x) Filter.atTop s) (hnez : ∏' (i : ℕ), f i ↑x ≠ 0) : logDeriv (fun (x : ℂ) => ∏' (i : ℕ), f i x) ↑x = ∑' (i : ℕ), logDeriv (f i) ↑x

theorem logDeriv_one_sub_exp (r : ℂ) : (logDeriv fun (z : ℂ) => 1 - r * Complex.exp z) = fun (z : ℂ) => -r * Complex.exp z / (1 - r * Complex.exp z)

theorem logDeriv_one_sub_exp_comp (r : ℂ) (g : ℂ → ℂ) (hg : Differentiable ℂ g) : logDeriv ((fun (z : ℂ) => 1 - r * Complex.exp z) ∘ g) = fun (z : ℂ) => -r * deriv g z * Complex.exp (g z) / (1 - r * Complex.exp (g z))

theorem logDeriv_q_expo_summable (r : ℂ) (hr : ‖r‖ < 1) : Summable fun (n : ℕ) => ↑n * r ^ n / (1 - r ^ n)

theorem func_div (a b c d : ℂ → ℂ) (x : ℂ) (hb : b x ≠ 0) (hd : d x ≠ 0) : (a / b) x = (c / d) x ↔ (a * d) x = (b * c) x

theorem deriv_EqOn_congr {f g : ℂ → ℂ} (s : Set ℂ) (hfg : Set.EqOn f g s) (hs : IsOpen s) : Set.EqOn (deriv f) (deriv g) s

theorem logDeriv_eqOn_iff2 (f g : ℂ → ℂ) (s : Set ℂ) (hf : DifferentiableOn ℂ f s) (hg : DifferentiableOn ℂ g s) (_hs : s.Nonempty) (hs2 : IsOpen s) (hsc : Convex ℝ s) (hgn : ∀ x ∈ s, g x ≠ 0) (hfn : ∀ x ∈ s, f x ≠ 0) : Set.EqOn (logDeriv f) (logDeriv g) s ↔ ∃ (z : ℂ), z ≠ 0 ∧ Set.EqOn f (z • g) s