Documentation Verification Report

Analytic

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

Statistics

Metric	Count
Definitions	0
Theorems `analyticAt`, `analyticAt_complex_partial`, `differentiableAt_complex_partial`, `exists_analyticOnNhd_ball_re_eq`, `exists_analyticOnNhd_univ_re_eq`, `harmonic_is_realOfHolomorphic_univ`, `harmonic_is_realOfHolomorphic`	7
Total	7

HarmonicAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`analyticAt` 📖	mathematical	`InnerProductSpace.HarmonicAt` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.instFiniteDimensionalReal` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	`AnalyticAt` `Real` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `Real.normedAddCommGroup` `RCLike.toInnerProductSpaceReal`	—	`Complex.instFiniteDimensionalReal` `Metric.isOpen_iff` `InnerProductSpace.isOpen_setOf_harmonicAt` `InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq` `analyticAt_congr` `Filter.eventually_of_mem` `Metric.ball_mem_nhds` `Set.EqOn.symm` `AnalyticAt.comp` `ContinuousLinearMap.analyticAt` `AnalyticAt.restrictScalars` `IsScalarTower.right` `Metric.mem_ball_self`
`analyticAt_complex_partial` 📖	mathematical	`InnerProductSpace.HarmonicAt` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.instFiniteDimensionalReal` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	`AnalyticAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Complex.instSub` `Complex.ofReal` `DFunLike.coe` `ContinuousLinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Real.denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `AddCommGroup.toAddCommMonoid` `Complex.addCommGroup` `Real.pseudoMetricSpace` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `Real.instRCLike` `instInnerProductSpaceRealComplex` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `fderiv` `Complex.instOne` `Complex.instMul` `Complex.I`	—	`Complex.instFiniteDimensionalReal` `DifferentiableOn.analyticAt` `Complex.instCompleteSpace` `DifferentiableAt.differentiableWithinAt` `differentiableAt_complex_partial` `IsOpen.mem_nhds` `InnerProductSpace.isOpen_setOf_harmonicAt`
`differentiableAt_complex_partial` 📖	mathematical	`InnerProductSpace.HarmonicAt` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.instFiniteDimensionalReal` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.instSub` `Complex.ofReal` `DFunLike.coe` `ContinuousLinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Real.denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.pseudoMetricSpace` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `Real.normedCommRing` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `fderiv` `Complex.instOne` `Complex.instMul` `Complex.I`	—	`Complex.instFiniteDimensionalReal` `differentiableAt_complex_iff_differentiableAt_real` `DifferentiableAt.sub` `DifferentiableAt.clm_apply` `differentiableAt_const` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContDiffAt.differentiableAt_one` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `ContDiffAt.fderiv_succ` `ContDiffAt.fun_comp` `ContDiffAt.snd` `contDiffAt_fun_id` `DifferentiableAt.const_smul` `Localization.instSMulCommClassOfIsScalarTower` `IsScalarTower.complexToReal` `IsScalarTower.right` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `fderiv_sub` `fderiv_const_smul` `RingHomCompTriple.ids` `fderiv_comp` `ContinuousLinearMap.differentiableAt` `ContinuousLinearMap.comp.congr_simp` `ContinuousLinearMap.fderiv` `IsSemitopologicalSemiring.toContinuousAdd` `instIsTopologicalRingReal` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsBoundedSMul.continuousSMul` `Complex.instT2Space` `mul_sub` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.add_neg` `add_zero` `IsTopologicalAddGroup.toContinuousAdd` `fderiv_clm_apply` `fderiv_fun_const` `ContinuousLinearMap.comp_zero` `zero_add` `Complex.I_sq` `neg_mul` `one_mul` `sub_neg_eq_add` `add_comm` `sub_eq_add_neg` `Nat.cast_one` `ContDiffAt.isSymmSndFDerivAt` `minSmoothness_of_isRCLikeNormedField` `instIsRCLikeNormedField` `instReflLe` `Filter.EventuallyEq.eq_of_nhds` `FiniteDimensional.rclike_to_real` `InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane` `iteratedFDeriv_two_apply` `Matrix.cons_val_fin_one` `Complex.ofReal_neg` `mul_neg`

InnerProductSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`harmonic_is_realOfHolomorphic_univ` 📖	mathematical	`HarmonicOnNhd` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.instFiniteDimensionalReal` `Real` `Real.normedAddCommGroup` `toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Set.univ`	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set.univ` `Complex.re`	—	`HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq`

InnerProductSpace.HarmonicOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_analyticOnNhd_ball_re_eq` 📖	mathematical	`InnerProductSpace.HarmonicOnNhd` `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`	`AnalyticOnNhd` `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.EqOn` `Real` `Complex.re`	—	`Complex.instFiniteDimensionalReal` `Metric.ball_eq_empty` `DifferentiableAt.differentiableWithinAt` `HarmonicAt.differentiableAt_complex_partial` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Complex.IsExactOn.with_val_at` `DifferentiableOn.isExactOn_ball` `Complex.instCompleteSpace` `HasDerivAt.differentiableAt` `DifferentiableOn.restrictScalars` `IsScalarTower.right` `DifferentiableOn.analyticOnNhd` `Metric.isOpen_ball` `Convex.eqOn_of_fderivWithin_eq` `instIsRCLikeNormedField` `convex_ball` `Differentiable.comp_differentiableOn` `ContinuousLinearMap.differentiable` `ContDiffAt.differentiableAt` `two_ne_zero` `CharZero.NeZero.two` `WithTop.charZero` `IsOpen.uniqueDiffOn` `PerfectSpace.not_isolated` `instPerfectSpace` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `DifferentiableAt.restrictScalars` `fderivWithin_eq_fderiv` `instIsTopologicalRingReal` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsOpen.uniqueDiffWithinAt` `DifferentiableAt.comp` `ContinuousLinearMap.differentiableAt` `RingHomCompTriple.ids` `fderiv_comp` `ContinuousLinearMap.fderiv` `LinearMap.IsScalarTower.compatibleSMul` `DifferentiableAt.fderiv_restrictScalars` `ContinuousLinearMap.ext` `mul_one` `Complex.re_add_im` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `fderiv_eq_smul_deriv` `HasDerivAt.deriv` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `sub_self` `sub_zero` `one_mul` `zero_add` `zero_sub` `mul_neg` `sub_neg_eq_add` `dist_self`
`exists_analyticOnNhd_univ_re_eq` 📖	mathematical	`InnerProductSpace.HarmonicOnNhd` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.instFiniteDimensionalReal` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Set.univ`	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Set.univ` `Complex.re`	—	`Complex.instFiniteDimensionalReal` `HarmonicAt.differentiableAt_complex_partial` `Set.mem_univ` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Complex.IsExactOn.with_val_at` `Differentiable.isExactOn_univ` `Complex.instCompleteSpace` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `HasDerivAt.differentiableAt` `Differentiable.restrictScalars` `IsScalarTower.right` `DifferentiableOn.analyticOnNhd` `Differentiable.differentiableOn` `isOpen_univ` `Complex.reCLM_apply` `Convex.eqOn_of_fderivWithin_eq` `instIsRCLikeNormedField` `convex_univ` `DifferentiableOn.clm_apply` `differentiableOn_const` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `ContDiffOn.differentiableOn` `Nat.instAtLeastTwoHAddOfNat` `contDiffOn` `two_ne_zero` `CharZero.NeZero.two` `WithTop.charZero` `PerfectSpace.not_isolated` `instPerfectSpace` `fderivWithin_univ` `RingHomCompTriple.ids` `fderiv_comp` `ContinuousLinearMap.differentiableAt` `Differentiable.differentiableAt` `ContinuousLinearMap.ext` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.IsScalarTower.compatibleSMul` `ContinuousLinearMap.comp.congr_simp` `ContinuousLinearMap.fderiv` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `HasFDerivAt.fderiv` `Complex.instT2Space` `HasFDerivAt.restrictScalars` `HasDerivAt.hasFDerivAt` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `sub_self` `sub_zero` `one_mul` `zero_add` `zero_sub` `mul_neg` `sub_neg_eq_add` `mul_one` `Complex.re_add_im`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`harmonic_is_realOfHolomorphic` 📖	mathematical	`InnerProductSpace.HarmonicOnNhd` `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`	`AnalyticOnNhd` `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.EqOn` `Real` `Complex.re`	—	`InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq`

---

← Back to Index