Documentation Verification Report

CircleTransform

📁 Source: Mathlib/MeasureTheory/Integral/CircleTransform.lean

Statistics

Metric	Count
Definitions `circleTransform`, `circleTransformBoundingFunction`, `circleTransformDeriv`	3
Theorems `circleTransformDeriv_bound`, `circleTransformDeriv_eq`, `circleTransformDeriv_periodic`, `continuousOn_norm_circleTransformBoundingFunction`, `continuousOn_prod_circle_transform_function`, `continuous_circleTransform`, `continuous_circleTransformDeriv`, `integral_circleTransform`, `norm_circleTransformBoundingFunction_le`	9
Total	12

Complex

Definitions

Name	Category	Theorems
`circleTransform` 📖	CompOp	3 math math: `circleTransformDeriv_eq`, `integral_circleTransform`, `continuous_circleTransform`
`circleTransformBoundingFunction` 📖	CompOp	2 math math: `norm_circleTransformBoundingFunction_le`, `continuousOn_norm_circleTransformBoundingFunction`
`circleTransformDeriv` 📖	CompOp	4 math math: `circleTransformDeriv_eq`, `continuous_circleTransformDeriv`, `circleTransformDeriv_periodic`, `circleTransformDeriv_bound`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleTransformDeriv_bound` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex` `Set` `Set.instMembership` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.sphere`	`Set.instHasSubset` `Real.instLE` `Norm.norm` `instNorm` `circleTransformDeriv` `instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	—	`Metric.exists_lt_mem_ball_of_mem_ball` `Metric.exists_ball_subset_ball` `Nat.instAtLeastTwoHAddOfNat` `norm_circleTransformBoundingFunction_le` `LT.lt.le` `Metric.pos_of_mem_ball` `IsCompact.exists_isMaxOn` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `isCompact_sphere` `instProperSpace` `NormedSpace.sphere_nonempty` `EMetric.instNontrivialTopologyOfNontrivial` `instNontrivial` `ContinuousOn.norm` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.ball_subset_ball` `Function.Periodic.exists_mem_Ico₀` `Real.instArchimedean` `circleTransformDeriv_periodic` `Real.two_pi_pos` `Set.Icc_subset_uIcc` `Set.Ico_subset_Icc_self` `Metric.ball_subset_closedBall` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `circleMap_mem_sphere` `norm_nonneg` `mul_assoc` `mul_inv_rev` `inv_I` `neg_mul` `deriv_circleMap` `norm_neg` `norm_mul` `norm_I` `norm_inv` `norm_real` `norm_ofNat` `norm_circleMap_zero` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `one_mul` `mul_one` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `PosMulReflectLE.toPosMulReflectLT` `IsOrderedAddMonoid.toAddLeftMono` `Real.instNontrivial`
`circleTransformDeriv_eq` 📖	mathematical	—	`circleTransformDeriv` `Complex` `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` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `instNormedField` `instInv` `instSub` `circleMap` `circleTransform`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.sub_congr` `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.Ring.pow_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.mul_assoc_rev` `mul_one` `add_zero` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.RingNF.nnrat_rawCast` `Mathlib.Tactic.RingNF.add_neg` `inv_pow` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow`
`circleTransformDeriv_periodic` 📖	mathematical	—	`Function.Periodic` `Real` `Real.instAdd` `circleTransformDeriv` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `periodic_circleMap` `deriv_circleMap`
`continuousOn_norm_circleTransformBoundingFunction` 📖	mathematical	`Real` `Real.instLT`	`ContinuousOn` `Complex` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Real.pseudoMetricSpace` `Norm.norm` `instNorm` `circleTransformBoundingFunction` `SProd.sprod` `Set` `Set.instSProd` `Metric.closedBall` `Set.univ`	—	`ContinuousOn.smul` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuousOn_const` `deriv_circleMap` `ContinuousOn.mul` `IsTopologicalSemiring.toContinuousMul` `Continuous.comp_continuousOn` `continuous_circleMap` `continuousOn_snd` `inv_pow` `continuousOn_prod_circle_transform_function` `ContinuousOn.norm`
`continuousOn_prod_circle_transform_function` 📖	mathematical	`Real` `Real.instLT`	`ContinuousOn` `Complex` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Real.pseudoMetricSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instInv` `instSub` `circleMap` `SProd.sprod` `Set` `Set.instSProd` `Metric.closedBall` `Set.univ`	—	`ContinuousOn.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousOn.div` `IsTopologicalDivisionRing.toContinuousInv₀` `continuousOn_const` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Continuous.comp_continuousOn` `continuous_circleMap` `continuousOn_snd` `continuousOn_fst` `Metric.closedBall_subset_ball` `sub_ne_zero` `circleMap_ne_mem_ball`
`continuous_circleTransform` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.sphere` `Set` `Set.instMembership` `Metric.ball`	`Continuous` `Real.pseudoMetricSpace` `circleTransform`	—	`Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_const` `deriv_circleMap` `Continuous.comp'` `Continuous.fun_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuous_id'` `continuous_circleMap` `continuous_circleMap_inv` `ContinuousOn.comp_continuous` `circleMap_mem_sphere` `LT.lt.le`
`continuous_circleTransformDeriv` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Metric.sphere` `Set` `Set.instMembership` `Metric.ball`	`Continuous` `Real.pseudoMetricSpace` `circleTransformDeriv`	—	`circleTransformDeriv_eq` `Continuous.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_circleMap_inv` `continuous_circleTransform`
`integral_circleTransform` 📖	mathematical	—	`intervalIntegral` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `circleTransform` `Real` `Real.instZero` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `Complex` `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` `instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `instNormedField` `instInv` `instMul` `instNatCast` `ofReal` `I` `circleIntegral` `instSub`	—	`Nat.instAtLeastTwoHAddOfNat` `deriv_circleMap` `mul_inv_rev` `inv_I` `neg_mul` `zero_add` `neg_smul` `intervalIntegral.integral_neg` `intervalIntegral.integral_smul` `NormedSpace.toNormSMulClass` `SMulCommClass.complexToReal` `smulCommClass_self`
`norm_circleTransformBoundingFunction_le` 📖	mathematical	`Real` `Real.instLT` `Real.instLE` `Real.instZero`	`Norm.norm` `Complex` `instNorm` `circleTransformBoundingFunction` `Set` `Set.instMembership` `SProd.sprod` `Set.instSProd` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Set.uIcc` `Real.lattice` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`continuousOn_norm_circleTransformBoundingFunction` `Nat.instAtLeastTwoHAddOfNat` `IsCompact.prod` `ProperSpace.isCompact_closedBall` `instProperSpace` `isCompact_uIcc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `Set.Nonempty.prod` `Metric.nonempty_closedBall` `Set.nonempty_uIcc` `IsCompact.exists_isMaxOn` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ContinuousOn.mono` `Set.prod_mono_right` `Set.subset_univ`

---

← Back to Index