Constructions

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

Statistics

Metric	Count
Definitions	0
Theorems harmonicAt, harmonicAt_conj, harmonicAt_im, harmonicAt_log_norm, harmonicAt_re, harmonicAt	6
Total	6

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
harmonicAt 📖	mathematical	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	InnerProductSpace.HarmonicAt instInnerProductSpaceRealComplex FiniteDimensional.rclike_to_real NormedSpace.complexToReal	—	ContDiffAt.harmonicAt contDiffAt Nat.instAtLeastTwoHAddOfNat
harmonicAt_conj 📖	mathematical	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	InnerProductSpace.HarmonicAt instInnerProductSpaceRealComplex FiniteDimensional.rclike_to_real Real Real.instRCLike DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.commSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Pi.starRing' NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instStarRing	—	FiniteDimensional.rclike_to_real RingHomInvPair.ids InnerProductSpace.harmonicAt_comp_CLE_iff harmonicAt Complex.instCompleteSpace
harmonicAt_im 📖	mathematical	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	InnerProductSpace.HarmonicAt instInnerProductSpaceRealComplex FiniteDimensional.rclike_to_real Real Real.normedAddCommGroup Real.instRCLike RCLike.toInnerProductSpaceReal Complex.im	—	InnerProductSpace.HarmonicAt.comp_CLM FiniteDimensional.rclike_to_real harmonicAt Complex.instCompleteSpace
harmonicAt_log_norm 📖	mathematical	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	InnerProductSpace.HarmonicAt instInnerProductSpaceRealComplex FiniteDimensional.rclike_to_real Real Real.normedAddCommGroup Real.instRCLike RCLike.toInnerProductSpaceReal Real.log Norm.norm Complex.instNorm	—	Nat.instAtLeastTwoHAddOfNat Complex.norm_def Real.log_sqrt Complex.normSq_nonneg Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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.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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.instAtLeastTwo CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul CancelDenoms.mul_subst Mathlib.Tactic.Linarith.mul_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true FiniteDimensional.rclike_to_real InnerProductSpace.HarmonicAt.const_smul Complex.normSq_neg neg Complex.mem_slitPlane_or_neg_mem_slitPlane
harmonicAt_re 📖	mathematical	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	InnerProductSpace.HarmonicAt instInnerProductSpaceRealComplex FiniteDimensional.rclike_to_real Real Real.normedAddCommGroup Real.instRCLike RCLike.toInnerProductSpaceReal Complex.re	—	InnerProductSpace.HarmonicAt.comp_CLM FiniteDimensional.rclike_to_real harmonicAt Complex.instCompleteSpace

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
harmonicAt 📖	mathematical	ContDiffAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat	InnerProductSpace.HarmonicAt instInnerProductSpaceRealComplex FiniteDimensional.rclike_to_real NormedSpace.complexToReal	—	Nat.instAtLeastTwoHAddOfNat FiniteDimensional.rclike_to_real restrict_scalars IsScalarTower.right IsScalarTower.complexToReal IsScalarTower.left Filter.mp_mem restrictScalars_iteratedFDeriv_eventuallyEq Filter.univ_mem' ContinuousMultilinearMap.map_smul_univ InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane Matrix.smul_cons mul_one Matrix.smul_empty Finset.prod_const Fintype.card_fin Complex.I_sq neg_smul one_smul add_neg_cancel

---

← Back to Index