PosLogEqCircleAverage

📁 Source: Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean

Statistics

Metric	Count
Definitions	0
Theorems circleAverage_log_norm_add_const_eq_posLog, circleAverage_log_norm_sub_const_eq_log_radius_add_posLog, circleAverage_log_norm_sub_const_eq_posLog, circleAverage_log_norm_sub_const_of_mem_closedBall, circleAverage_log_norm_sub_const₀, circleAverage_log_norm_sub_const₁, circleAverage_log_norm_sub_const₂, circleIntegrable_log_norm_sub_const	8
Total	8

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleAverage_log_norm_add_const_eq_posLog 📖	mathematical	—	Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log Norm.norm Complex Complex.instNorm Complex.instAdd Complex.instZero Real.instOne Real.posLog	—	sub_neg_eq_add circleAverage_log_norm_sub_const_eq_posLog norm_neg
circleAverage_log_norm_sub_const_eq_log_radius_add_posLog 📖	mathematical	—	Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log Norm.norm Complex Complex.instNorm Complex.instSub Real.instAdd Real.posLog Real.instMul Real.instInv	—	Real.circleAverage_eq_circleAverage_zero_one Complex.ofReal_inv Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Complex.ofReal_ne_zero Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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 Real.circleAverage_congr_codiscreteWithin codiscreteWithin_iff_locallyFiniteComplementWithin T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace abs_one Real.instIsOrderedRing Set.univ_inter Set.Subsingleton.finite add_eq_zero_iff_eq_neg sub_zero Filter.mp_mem Filter.univ_mem' norm_mul NormedDivisionRing.toNormMulClass Real.log_mul norm_ne_zero_iff Complex.norm_real Real.log_abs zero_ne_one' NeZero.charZero_one RCLike.charZero_rclike Pi.add_def Real.circleAverage_add circleIntegrable_const circleIntegrable_log_norm_meromorphicOn MeromorphicAt.fun_add MeromorphicAt.id MeromorphicAt.const Real.circleAverage_const Real.instCompleteSpace circleAverage_log_norm_add_const_eq_posLog Complex.norm_mul norm_inv Ne.lt_or_gt abs_of_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid inv_neg neg_mul Real.posLog_neg abs_of_pos
circleAverage_log_norm_sub_const_eq_posLog 📖	mathematical	—	Real.circleAverage Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log Norm.norm Complex Complex.instNorm Complex.instSub Complex.instZero Real.instOne Real.posLog	—	lt_trichotomy circleAverage_log_norm_sub_const₂ Real.posLog_eq_log abs_norm le_of_lt circleAverage_log_norm_sub_const₁ Real.posLog_eq_zero_iff circleAverage_log_norm_sub_const₀
circleAverage_log_norm_sub_const_of_mem_closedBall 📖	mathematical	Complex Set Set.instMembership Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField abs Real Real.lattice Real.instAddGroup	Real.circleAverage Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log Norm.norm Complex.instNorm Complex.instSub	—	abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Metric.closedBall_zero Real.circleAverage_zero Real.instCompleteSpace sub_self norm_zero Real.log_zero circleAverage_log_norm_sub_const_eq_log_radius_add_posLog add_eq_left AddLeftCancelSemigroup.toIsLeftCancelAdd Real.posLog_eq_zero_iff abs_mul Real.instIsOrderedRing abs_inv Real.instIsStrictOrderedRing abs_of_nonneg norm_nonneg inv_mul_le_one_of_le₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instZeroLEOneClass dist_eq_norm' Metric.mem_closedBall abs_nonneg covariant_swap_add_of_covariant_add
circleAverage_log_norm_sub_const₀ 📖	mathematical	Real Real.instLT Norm.norm Complex Complex.instNorm Real.instOne	Real.circleAverage Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log Complex.instSub Complex.instZero Real.instZero	—	Real.circleAverage_congr_sphere norm_zero NeZero.charZero_one RCLike.charZero_rclike abs_one Real.instIsOrderedRing sub_zero Complex.norm_mul norm_inv inv_one one_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_ne_zero NeZero.one GroupWithZero.toNontrivial Real.circleAverage_zero_one_congr_inv HarmonicOnNhd.circleAverage_eq mul_le_of_le_one_left IsOrderedRing.toMulPosMono norm_nonneg dist_zero_right AnalyticAt.harmonicAt_log_norm AnalyticAt.fun_sub analyticAt_const AnalyticAt.fun_mul analyticAt_id sub_ne_zero lt_self_iff_false CStarRing.norm_of_mem_unitary RCLike.instCStarRing Complex.instNontrivial Submonoid.one_mem MulZeroClass.zero_mul Real.log_one
circleAverage_log_norm_sub_const₁ 📖	mathematical	Norm.norm Complex Complex.instNorm Real Real.instOne	Real.circleAverage Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log Complex.instSub Complex.instZero Real.instZero	—	mul_inv_rev NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike Set.exists_range_iff range_circleMap abs_one Real.instIsOrderedRing sub_zero norm_inv inv_one Nat.instAtLeastTwoHAddOfNat Complex.norm_mul norm_circleMap_zero one_mul zero_add mul_sub Complex.ofReal_add add_mul Distrib.rightDistribClass Complex.exp_add inv_mul_cancel₀ norm_zero NeZero.charZero_one periodic_circleMap Function.Periodic.intervalIntegral_add_eq intervalIntegral.integral_comp_add_left add_zero intervalIntegral.integral_congr Complex.norm_def Real.log_sqrt Complex.normSq_nonneg Complex.exp_ofReal_mul_I_re Complex.exp_ofReal_mul_I_im Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add 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_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_mul Real.sin_sq_add_cos_sq Mathlib.Meta.NormNum.IsNat.to_eq mul_div_assoc mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Real.cos_two_mul Mathlib.Meta.NormNum.isNat_mul mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
circleAverage_log_norm_sub_const₂ 📖	mathematical	Real Real.instLT Real.instOne Norm.norm Complex Complex.instNorm	Real.circleAverage Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log Complex.instSub Complex.instZero	—	HarmonicOnNhd.circleAverage_eq AnalyticAt.harmonicAt_log_norm AnalyticAt.fun_sub analyticAt_id analyticAt_const sub_ne_zero Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le abs_one dist_zero_right zero_sub norm_neg
circleIntegrable_log_norm_sub_const 📖	mathematical	—	CircleIntegrable Real Real.normedAddCommGroup Real.log Norm.norm Complex Complex.instNorm Complex.instSub	—	circleIntegrable_log_norm_meromorphicOn MeromorphicAt.fun_sub MeromorphicAt.id MeromorphicAt.const

---

← Back to Index