Theorems · Theorem · real analysis
Real.log_prod
∀ {α : Type u_1} {s : Finset α} {f : α → ℝ}, (∀ x ∈ s, f x ≠ 0) → Real.log (∏ i ∈ s, f i) = ∑ i ∈ s, Real.log (f i)- Cited by
- 13 results in Mathlib
- Foundations
- Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Finsetstatement and proof · cited by 13,712
- Finset.sumstatement and proof · cited by 5,195
- Finset.prodstatement · cited by 2,356
- Finset.sum_congrproof · cited by 2,323
- Real.logstatement and proof · cited by 939
- Finset.prod_map_toListproof · cited by 5
- Finset.sum_map_toListproof · cited by 4
- Real.log_list_prodproof · cited by 2
Cited by13
Results whose statement or proof uses this declaration.
- MeromorphicOn.extract_zeros_poles_logproof · cited by 3
- NumberField.Units.sum_mult_mul_logproof · cited by 2
- NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_applyproof · cited by 2
- Real.log_finprodproof · cited by 1
- Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAtproof · cited by 1
- ProbabilityTheory.iIndepFun.cgf_sum₀proof · cited by 1
- Finsupp.log_prodproof · cited by 1
- NumberField.Units.abs_det_eq_abs_detproof · cited by 1
- Chebyshev.theta_eq_log_primorialproof · cited by 1
- Chebyshev.psi_eq_log_lcmUptoproof · cited by 1
- Height.logHeight_fun_prod_eqproof · cited by 0
- Complex.ECanonicalDecomp.log_norm_eqproof · cited by 0