Poisson

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

Statistics

Metric	Count
Definitions herglotzRieszKernel, poissonKernel	2
Theorems circleAverage_poissonKernel_smul, circleAverage_poissonKernel_smul', circleAverage_re_herglotzRieszKernel_smul, circleAverage_re_herglotzRieszKernel_smul', herglotzRieszKernel_def, herglotzRieszKernel_fun_def, le_re_herglotzRieszKernel, poissonKernel_def, poissonKernel_eq_re_herglotzRieszKernel, re_herglotzRieszKernel_le	10
Total	12

DiffContOnCl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleAverage_poissonKernel_smul 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set Set.instMembership	Real.circleAverage NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup Pi.smul' Complex Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField poissonKernel	—	poissonKernel_eq_re_herglotzRieszKernel circleAverage_re_herglotzRieszKernel_smul
circleAverage_poissonKernel_smul' 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set Set.instMembership	Real.circleAverage NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Monoid.toPow Norm.norm Complex Complex.instNorm Complex.instSub	—	circleAverage_poissonKernel_smul
circleAverage_re_herglotzRieszKernel_smul 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set Set.instMembership	Real.circleAverage NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup Pi.smul' Complex Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Complex.re herglotzRieszKernel	—	le_or_gt Metric.ball_eq_empty comp DifferentiableOn.diffContOnCl DifferentiableOn.add_const differentiableOn_id dist_add_self_left dist_zero_right mem_ball_iff_norm herglotzRieszKernel_def add_sub_cancel_right add_zero sub_add_cancel
circleAverage_re_herglotzRieszKernel_smul' 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set Set.instMembership	Real.circleAverage NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Complex.re Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instAdd Complex.instSub	—	circleAverage_re_herglotzRieszKernel_smul

(root)

Definitions

Name	Category	Theorems
herglotzRieszKernel 📖	CompOp	6 math math: herglotzRieszKernel_fun_def, herglotzRieszKernel_def, DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul, poissonKernel_eq_re_herglotzRieszKernel, InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul, InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul
poissonKernel 📖	CompOp	5 math math: InnerProductSpace.HarmonicOnNhd.circleAverage_poissonKernel_smul, DiffContOnCl.circleAverage_poissonKernel_smul, poissonKernel_eq_re_herglotzRieszKernel, InnerProductSpace.HarmonicContOnCl.circleAverage_poissonKernel_smul, poissonKernel_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
herglotzRieszKernel_def 📖	mathematical	—	herglotzRieszKernel Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instAdd Complex.instSub	—	—
herglotzRieszKernel_fun_def 📖	mathematical	—	herglotzRieszKernel Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instAdd Complex.instSub	—	herglotzRieszKernel_def
le_re_herglotzRieszKernel 📖	mathematical	Complex Set Set.instMembership Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Metric.ball	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Norm.norm Complex Complex.instNorm Complex.instSub Real.instAdd Complex.re Complex.instDivInvMonoid Complex.instAdd	—	norm_zero sub_zero add_zero div_self instReflLe sub_sub_sub_cancel_right Complex.norm_mul_exp_arg_mul_I mem_ball_iff_norm
poissonKernel_def 📖	mathematical	—	poissonKernel Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Monoid.toPow Real.instMonoid Norm.norm Complex Complex.instNorm Complex.instSub	—	—
poissonKernel_eq_re_herglotzRieszKernel 📖	mathematical	—	poissonKernel Complex Real Complex.re herglotzRieszKernel	—	—
re_herglotzRieszKernel_le 📖	mathematical	Complex Set Set.instMembership Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Metric.ball	Real Real.instLE Complex.re Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instAdd Complex.instSub Real.instDivInvMonoid Real.instAdd Norm.norm Complex.instNorm Real.instSub	—	add_zero sub_zero div_self norm_zero instReflLe sub_sub_sub_cancel_right Complex.norm_mul_exp_arg_mul_I mem_ball_iff_norm

---

← Back to Index