Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `HarmonicAt`, `HarmonicOnNhd`	2
Theorems `add`, `comp_CLM`, `const_smul`, `eventually`, `add`, `comp_CLM`, `const_smul`, `mono`, `harmonicAt_comp_CLE_iff`, `harmonicAt_congr_nhds`, `harmonicOnNhd_comp_CLE_iff`, `isOpen_setOf_harmonicAt`	12
Total	14

InnerProductSpace

Definitions

Name	Category	Theorems
`HarmonicAt` 📖	MathDef	9 math math: `AnalyticAt.harmonicAt_im`, `AnalyticAt.harmonicAt_conj`, `harmonicAt_comp_CLE_iff`, `ContDiffAt.harmonicAt`, `AnalyticAt.harmonicAt_re`, `harmonicAt_congr_nhds`, `AnalyticAt.harmonicAt_log_norm`, `isOpen_setOf_harmonicAt`, `AnalyticAt.harmonicAt`
`HarmonicOnNhd` 📖	MathDef	1 math math: `harmonicOnNhd_comp_CLE_iff`

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`
`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`
`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`	`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`	`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`	`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` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Filter.mp_mem` `Filter.Eventually.eventually_nhds` `ContDiffAt.eventually` `Filter.univ_mem'`

InnerProductSpace.HarmonicOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`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`	`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`	`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`
`mono` 📖	—	`InnerProductSpace.HarmonicOnNhd` `Set` `Set.instHasSubset`	—	—	—

---

← Back to Index