MeanValue

📁 Source: Mathlib/Analysis/Complex/MeanValue.lean

Statistics

Metric	Count
Definitions	0
Theorems circleAverage, circleAverage_smul_div, circleAverage_of_differentiable_on, circleAverage_of_differentiable_on_off_countable, circleAverage_sub_sub_inv_smul_of_differentiable_on, circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable	6
Total	6

DiffContOnCl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleAverage 📖	mathematical	DiffContOnCl 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 abs Real Real.lattice Real.instAddGroup	Real.circleAverage NormedSpace.complexToReal	—	Real.circleAverage_zero circleAverage_smul_div dist_self IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.circleAverage_congr_sphere div_self one_smul
circleAverage_smul_div 📖	mathematical	DiffContOnCl 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 abs Real Real.lattice Real.instAddGroup Set Set.instMembership	Real.circleAverage NormedSpace.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instSub	—	Metric.ball_eq_empty circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable Set.countable_empty closure_ball ne_of_not_ge continuousOn DifferentiableWithinAt.differentiableAt differentiableOn Set.diff_empty IsOpen.mem_nhds Metric.isOpen_ball

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleAverage_of_differentiable_on 📖	mathematical	DiffContOnCl 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 abs Real Real.lattice Real.instAddGroup	Real.circleAverage NormedSpace.complexToReal	—	DiffContOnCl.circleAverage
circleAverage_of_differentiable_on_off_countable 📖	mathematical	ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Metric.closedBall abs Real Real.lattice Real.instAddGroup DifferentiableAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	Real.circleAverage NormedSpace.complexToReal	—	Real.circleAverage_zero circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable dist_self IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.circleAverage_congr_sphere div_self one_smul
circleAverage_sub_sub_inv_smul_of_differentiable_on 📖	mathematical	DiffContOnCl 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 abs Real Real.lattice Real.instAddGroup Set Set.instMembership	Real.circleAverage NormedSpace.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instSub	—	DiffContOnCl.circleAverage_smul_div
circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable 📖	mathematical	ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Metric.closedBall abs Real Real.lattice Real.instAddGroup DifferentiableAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Set Set.instMembership Metric.ball	Real.circleAverage NormedSpace.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instSub	—	Real.circleAverage_abs_radius le_or_gt Metric.ball_eq_empty Nat.instAtLeastTwoHAddOfNat Real.circleAverage_eq_circleIntegral LT.lt.ne' mul_inv_rev Complex.inv_I neg_mul neg_smul instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instCharZero circleIntegral.integral_congr LT.lt.le Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable mul_one 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.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ one_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero mul_neg 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'_ofNat Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_ne_zero NeZero.one GroupWithZero.toNontrivial Complex.I_sq neg_neg

---

← Back to Index