Poisson

📁 Source: Mathlib/Analysis/Complex/Harmonic/Poisson.lean

Statistics

Metric	Count
Definitions	0
Theorems circleAverage_poissonKernel_smul, circleAverage_re_herglotzRieszKernel_smul, circleAverage_poissonKernel_smul, circleAverage_re_herglotzRieszKernel_smul	4
Total	4

InnerProductSpace.HarmonicContOnCl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleAverage_poissonKernel_smul 📖	mathematical	InnerProductSpace.HarmonicContOnCl Complex Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set Set.instMembership	Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Pi.smul' Complex Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id poissonKernel	—	Complex.instFiniteDimensionalReal circleAverage_re_herglotzRieszKernel_smul Real.circleAverage_congr_sphere
circleAverage_re_herglotzRieszKernel_smul 📖	mathematical	InnerProductSpace.HarmonicContOnCl Complex Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set Set.instMembership	Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Pi.smul' Complex Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Complex.re herglotzRieszKernel	—	Complex.instFiniteDimensionalReal Real.ContinuousOn.eq_of_eqOn_Ioo Real.ContinuousOn.circleAverage herglotzRieszKernel_fun_def ContinuousOn.smul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousOn.mono continuousOn InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul InnerProductSpace.HarmonicOnNhd.mono harmonicOnNhd Metric.closedBall_subset_ball

InnerProductSpace.HarmonicOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleAverage_poissonKernel_smul 📖	mathematical	InnerProductSpace.HarmonicOnNhd Complex Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set Set.instMembership Metric.ball	Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Pi.smul' Complex Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id poissonKernel	—	Complex.instFiniteDimensionalReal circleAverage_re_herglotzRieszKernel_smul Real.circleAverage_congr_sphere
circleAverage_re_herglotzRieszKernel_smul 📖	mathematical	InnerProductSpace.HarmonicOnNhd Complex Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex Complex.instFiniteDimensionalReal Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set Set.instMembership Metric.ball	Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Pi.smul' Complex Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Complex.re herglotzRieszKernel	—	Complex.instFiniteDimensionalReal IsCompact.exists_thickening_subset_open ProperSpace.isCompact_closedBall Complex.instProperSpace InnerProductSpace.isOpen_setOf_harmonicAt exists_analyticOnNhd_ball_re_eq thickening_closedBall LT.lt.le Metric.pos_of_mem_ball AnalyticAt.differentiableWithinAt herglotzRieszKernel_def sub_sub_sub_cancel_right Metric.sphere_subset_ball lt_add_of_pos_left IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add MulZeroClass.zero_mul sub_zero Real.circleAverage_congr_sphere abs_of_pos ContinuousLinearMap.circleAverage_comp_comm Real.instCompleteSpace Complex.instCompleteSpace ContinuousOn.circleIntegrable' ContinuousOn.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.mono AnalyticOnNhd.continuousOn AnalyticOnNhd.mono DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul' DifferentiableOn.diffContOnCl

---

← Back to Index