LogDerivUniformlyOn

Statistics

Metric	Count
Definitions	0
Theorems `logDeriv_tprod_eq_tsum`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`logDeriv_tprod_eq_tsum` 📖	mathematical	`IsOpen` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `DifferentiableOn` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `logDeriv` `NormedAlgebra.id` `NontriviallyNormedField.toNormedField` `SummationFilter.unconditional` `MultipliableLocallyUniformlyOn` `CommRing.toCommMonoid` `Complex.commRing`	`tprod` `tsum`	—	`Summable.hasSum_iff` `Complex.instT2Space` `SummationFilter.instNeBotUnconditional` `Filter.Tendsto.congr` `logDeriv_prod` `DifferentiableWithinAt.differentiableAt` `IsOpen.mem_nhds` `Complex.logDeriv_tendsto` `MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn` `Filter.Eventually.of_forall` `DifferentiableOn.fun_finset_prod`

---