Basic

📁 Source: Mathlib/Analysis/InnerProductSpace/Harmonic/Basic.lean

Statistics

Metric	Count
Definitions HarmonicAt, HarmonicOnNhd	2
Theorems add, comp_CLM, const_smul, eventually, neg, sub, add, comp_CLM, const_smul, contDiffOn, continuousOn, mono, neg, sub, harmonicAt_comp_CLE_iff, harmonicAt_congr_nhds, harmonicAt_const, harmonicOnNhd_comp_CLE_iff, harmonicOnNhd_const, isOpen_setOf_harmonicAt	20
Total	22

InnerProductSpace

Definitions

Name	Category	Theorems
HarmonicAt 📖	MathDef	16 math math: harmonicAt_const, HarmonicAt.const_smul, AnalyticAt.harmonicAt_im, HarmonicAt.eventually, AnalyticAt.harmonicAt_conj, harmonicAt_comp_CLE_iff, HarmonicAt.sub, ContDiffAt.harmonicAt, HarmonicAt.neg, AnalyticAt.harmonicAt_re, harmonicAt_congr_nhds, AnalyticAt.harmonicAt_log_norm, isOpen_setOf_harmonicAt, AnalyticAt.harmonicAt, HarmonicAt.comp_CLM, HarmonicAt.add
HarmonicOnNhd 📖	MathDef	10 math math: harmonicOnNhd_comp_CLE_iff, HarmonicOnNhd.comp_CLM, harmonicOnNhd_const, HarmonicOnNhd.add, HarmonicOnNhd.neg, HarmonicOnNhd.sub, HarmonicOnNhd.const_smul, HarmonicContOnCl.harmonicOnNhd, IsClosed.harmonicContOnCl_iff, HarmonicOnNhd.mono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
harmonicAt_comp_CLE_iff 📖	mathematical	—	HarmonicAt DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike ContinuousLinearEquiv.equivLike	—	RingHomInvPair.ids HarmonicAt.congr_simp ContinuousLinearEquiv.symm_apply_apply HarmonicAt.comp_CLM
harmonicAt_congr_nhds 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	HarmonicAt	—	ContDiffAt.congr_of_eventuallyEq Filter.EventuallyEq.symm Filter.EventuallyEq.trans laplacian_congr_nhds
harmonicAt_const 📖	mathematical	—	HarmonicAt	—	contDiffAt_const laplacian_const
harmonicOnNhd_comp_CLE_iff 📖	mathematical	—	HarmonicOnNhd DFunLike.coe ContinuousLinearEquiv Real Real.semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike ContinuousLinearEquiv.equivLike	—	RingHomInvPair.ids harmonicAt_comp_CLE_iff
harmonicOnNhd_const 📖	mathematical	—	HarmonicOnNhd	—	—
isOpen_setOf_harmonicAt 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup setOf HarmonicAt	—	isOpen_iff_mem_nhds HarmonicAt.eventually

InnerProductSpace.HarmonicAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	InnerProductSpace.HarmonicAt	InnerProductSpace.HarmonicAt Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	ContDiffAt.add Filter.mp_mem ContDiffAt.laplacian_add_nhds Filter.univ_mem' add_zero
comp_CLM 📖	mathematical	InnerProductSpace.HarmonicAt	InnerProductSpace.HarmonicAt DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike	—	ContDiffAt.continuousLinearMap_comp Filter.mp_mem ContDiffAt.laplacian_CLM_comp_left_nhds Filter.univ_mem' map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
const_smul 📖	mathematical	InnerProductSpace.HarmonicAt	InnerProductSpace.HarmonicAt Real Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	ContDiffAt.const_smul smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Filter.mp_mem InnerProductSpace.laplacian_smul_nhds IsScalarTower.left Filter.univ_mem' smul_zero
eventually 📖	mathematical	InnerProductSpace.HarmonicAt	Filter.Eventually InnerProductSpace.HarmonicAt nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Filter.mp_mem Filter.Eventually.eventually_nhds ContDiffAt.eventually Filter.univ_mem'
neg 📖	mathematical	InnerProductSpace.HarmonicAt	InnerProductSpace.HarmonicAt Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	ContDiffAt.neg Filter.mp_mem Filter.univ_mem' InnerProductSpace.laplacian_neg neg_zero
sub 📖	mathematical	InnerProductSpace.HarmonicAt	InnerProductSpace.HarmonicAt Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	ContDiffAt.sub Filter.mp_mem ContDiffAt.laplacian_sub_nhds Filter.univ_mem' sub_self

InnerProductSpace.HarmonicOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	InnerProductSpace.HarmonicOnNhd	InnerProductSpace.HarmonicOnNhd Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	InnerProductSpace.HarmonicAt.add
comp_CLM 📖	mathematical	InnerProductSpace.HarmonicOnNhd	InnerProductSpace.HarmonicOnNhd DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike	—	InnerProductSpace.HarmonicAt.comp_CLM
const_smul 📖	mathematical	InnerProductSpace.HarmonicOnNhd	InnerProductSpace.HarmonicOnNhd Real Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	InnerProductSpace.HarmonicAt.const_smul
contDiffOn 📖	mathematical	InnerProductSpace.HarmonicOnNhd	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	—	ContDiffAt.contDiffWithinAt
continuousOn 📖	mathematical	InnerProductSpace.HarmonicOnNhd	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	ContinuousAt.continuousWithinAt ContDiffAt.continuousAt
mono 📖	mathematical	InnerProductSpace.HarmonicOnNhd Set Set.instHasSubset	InnerProductSpace.HarmonicOnNhd	—	—
neg 📖	mathematical	InnerProductSpace.HarmonicOnNhd	InnerProductSpace.HarmonicOnNhd Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	InnerProductSpace.HarmonicAt.neg
sub 📖	mathematical	InnerProductSpace.HarmonicOnNhd	InnerProductSpace.HarmonicOnNhd Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	InnerProductSpace.HarmonicAt.sub

---

← Back to Index