Periodic

📁 Source: Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean

Statistics

Metric	Count
Definitions measurableEquivIco, measurableEquivIoc, measureSpace	3
Theorems add_projection_respects_measure, instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume, instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples, instIsAddHaarMeasureRealVolume, instIsUnifLocDoublingMeasureRealVolume, integral_liftIoc_eq_intervalIntegral, integral_preimage, intervalIntegral_preimage, isFiniteMeasure, lintegral_preimage, measurable_mk', measurePreserving_equivIoc, measurePreserving_mk, measure_univ, volume_closedBall, integral_le_sSup_add_zsmul_of_pos, intervalIntegrable, intervalIntegrable₀, intervalIntegral_add_eq, intervalIntegral_add_eq_add, intervalIntegral_add_eq_of_pos, intervalIntegral_add_zsmul_eq, sInf_add_zsmul_le_integral_of_pos, tendsto_atBot_intervalIntegral_of_pos, tendsto_atBot_intervalIntegral_of_pos', tendsto_atTop_intervalIntegral_of_pos, tendsto_atTop_intervalIntegral_of_pos', memLp_liftIoc, integral_preimage, intervalIntegral_preimage, lintegral_preimage, measurePreserving_mk, measure_univ, isAddFundamentalDomain_Ioc, isAddFundamentalDomain_Ioc'	35
Total	38

AddCircle

Definitions

Name	Category	Theorems
measurableEquivIco 📖	CompOp	—
measurableEquivIoc 📖	CompOp	—
measureSpace 📖	CompOp	31 math math: measure_univ, UnitAddCircle.lintegral_preimage, UnitAddCircle.intervalIntegral_preimage, volume_eq_smul_haarAddCircle, integral_haarAddCircle, intervalIntegral_preimage, instIsAddHaarMeasureRealVolume, MeasureTheory.memLp_haarAddCircle_iff, ergodic_nsmul_add, add_projection_respects_measure, MeasureTheory.MemLp.memLp_liftIoc, ergodic_add_left, ergodic_add_right, UnitAddCircle.measure_univ, instIsUnifLocDoublingMeasureRealVolume, volume_closedBall, ergodic_nsmul, measurePreserving_equivIoc, UnitAddCircle.measurePreserving_mk, ergodic_zsmul, addWellApproximable_ae_empty_or_univ, isFiniteMeasure, instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume, MeasureTheory.MemLp.of_haarAddCircle, lintegral_preimage, measurePreserving_mk, integral_liftIoc_eq_intervalIntegral, closedBall_ae_eq_ball, UnitAddCircle.integral_preimage, integral_preimage, ergodic_zsmul_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_projection_respects_measure 📖	mathematical	MeasurableSet AddCircle Real Real.instAddCommGroup QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples	DFunLike.coe MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Real.measureSpace Set.instInter Set.preimage HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup Set.Ioc Real.instPreorder Real.instAdd	—	MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure_apply instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume isAddFundamentalDomain_Ioc' Fact.out
instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume 📖	mathematical	—	MeasureTheory.AddQuotientMeasureEqMeasurePreimage AddOpposite Real AddSubgroup AddOpposite.instAddGroup AddCommGroup.toAddGroup Real.instAddCommGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zmultiples AddSubgroup.toAddGroup AddAction.instAddAction AddMonoid.toOppositeAddAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume AddCircle measureSpace	—	MeasureTheory.leftInvariantIsAddQuotientMeasureEqMeasurePreimage instIsTopologicalAddGroupReal Real.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace AddSubgroup.normal_of_comm TopologicalSpace.t2Space_of_metrizableSpace QuotientAddGroup.instSecondCountableTopology IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real AddSubgroup.instCountableSubtypeMemZMultiples MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal instIsAddHaarMeasureRealVolume CompactSpace.sigmaCompact compactSpace isFiniteMeasure instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume AddSubgroup.instCountableSubtypeAddOppositeMemOp AddSubgroup.instMeasurableConstVAdd AddOpposite.instMeasurableConstVAdd AddCommSemigroup.isCentralVAdd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_of_add ContinuousAdd.measurableAdd MeasureTheory.Subgroup.vaddInvariantMeasure MeasureTheory.Measure.IsAddRightInvariant.toVAddInvariantMeasure_op isAddFundamentalDomain_Ioc' Fact.out zero_add Real.volume_Ioc sub_zero measure_univ
instHasAddFundamentalDomainSubtypeAddOppositeRealMemAddSubgroupOpZmultiples 📖	mathematical	—	MeasureTheory.HasAddFundamentalDomain AddOpposite Real AddSubgroup AddOpposite.instAddGroup Real.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zmultiples AddSubgroup.zero AddSubgroup.instVAdd Real.measurableSpace MeasureTheory.MeasureSpace.volume Real.measureSpace	—	isAddFundamentalDomain_Ioc' Fact.out
instIsAddHaarMeasureRealVolume 📖	mathematical	—	MeasureTheory.Measure.IsAddHaarMeasure AddCircle Real Real.instAddCommGroup QuotientAddGroup.Quotient.addGroup AddCommGroup.toAddGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume	—	MeasureTheory.Measure.IsAddHaarMeasure.smul AddSubgroup.normal_of_comm compactSpace MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure Fact.out ENNReal.ofReal_ne_top
instIsUnifLocDoublingMeasureRealVolume 📖	mathematical	—	IsUnifLocDoublingMeasure AddCircle Real Real.instAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace QuotientAddGroup.instSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing AddSubgroup.zmultiples AddCommGroup.toAddGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume	—	Nat.instAtLeastTwoHAddOfNat Filter.Eventually.of_forall volume_closedBall ENNReal.ofReal_mul zero_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.ofReal_le_ofReal mul_min_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing min_le_min le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_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.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 Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq 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.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Fact.out le_refl
integral_liftIoc_eq_intervalIntegral 📖	mathematical	—	MeasureTheory.integral AddCircle Real Real.instAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume liftIoc Real.linearOrder Real.instIsOrderedAddMonoid Real.instArchimedean intervalIntegral Real.instAdd Real.measureSpace	—	Real.instIsOrderedAddMonoid Real.instArchimedean intervalIntegral_preimage intervalIntegral.integral_congr_ae Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass liftIoc_coe_apply Set.uIoc_of_le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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 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_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Fact.out
integral_preimage 📖	mathematical	—	MeasureTheory.integral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder Real.instAdd AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples AddCircle measureSpace	—	measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.integral_map_equiv MeasureTheory.MeasurePreserving.map_eq MeasureTheory.integral_subtype MeasureTheory.Measure.map_map measurable_mk' measurable_subtype_coe map_comap_subtype_coe
intervalIntegral_preimage 📖	mathematical	—	intervalIntegral Real AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instAdd MeasureTheory.MeasureSpace.volume Real.measureSpace MeasureTheory.integral AddCircle MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace	—	intervalIntegral.integral_of_le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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 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_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Fact.out integral_preimage
isFiniteMeasure 📖	mathematical	—	MeasureTheory.IsFiniteMeasure AddCircle Real Real.instAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume	—	measure_univ
lintegral_preimage 📖	mathematical	—	MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder Real.instAdd AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples AddCircle measureSpace	—	measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.lintegral_map_equiv MeasureTheory.MeasurePreserving.map_eq map_comap_subtype_coe MeasurableEmbedding.lintegral_map MeasurableEmbedding.subtype_coe MeasureTheory.Measure.map_map measurable_mk' measurable_subtype_coe
measurable_mk' 📖	mathematical	—	Measurable Real AddCircle Real.instAddCommGroup Real.measurableSpace QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	Continuous.measurable BorelSpace.opensMeasurable Real.borelSpace QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples continuous_mk'
measurePreserving_equivIoc 📖	mathematical	—	MeasureTheory.MeasurePreserving AddCircle Real Real.instAddCommGroup Set.Elem Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.linearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace Subtype.instMeasurableSpace Set Set.instMembership Real.measurableSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivIoc Real.instIsOrderedAddMonoid Real.instArchimedean MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.comap Real.measureSpace	—	MeasurableEquiv.measurable Real.instIsOrderedAddMonoid Real.instArchimedean MeasureTheory.Measure.ext MeasureTheory.Measure.comap_apply Subtype.val_injective MeasurableSet.subtype_image measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal MeasureTheory.Measure.map_apply add_projection_respects_measure Set.ext equivIoc_coe_eq
measurePreserving_mk 📖	mathematical	—	MeasureTheory.MeasurePreserving Real AddCircle Real.instAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.measurableSpace AddSubgroup.zmultiples MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder Real.instAdd measureSpace	—	measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage isAddFundamentalDomain_Ioc' Fact.out instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume
measure_univ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure AddCircle Real Real.instAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.univ ENNReal.ofReal	—	compactSpace TopologicalSpace.PositiveCompacts.coe_top MeasureTheory.Measure.addHaarMeasure_self AddSubgroup.normal_of_comm QuotientAddGroup.instIsTopologicalAddGroup instIsTopologicalAddGroupReal QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Real.borelSpace AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples mul_one
volume_closedBall 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure AddCircle Real Real.instAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace QuotientAddGroup.instSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing AddSubgroup.zmultiples AddCommGroup.toAddGroup ENNReal.ofReal Real.instMin Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	abs_eq_self Real.instIsOrderedAddMonoid LT.lt.le Fact.out Nat.instAtLeastTwoHAddOfNat Set.inter_eq_left Real.closedBall_eq_Icc zero_sub zero_add lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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 Nat.cast_one Mathlib.Tactic.Ring.one_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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le CancelDenoms.neg_subst le_of_not_gt Mathlib.Tactic.Linarith.add_neg if_ctx_congr coe_real_preimage_closedBall_inter_eq Set.Ioc_subset_Icc_self MeasureTheory.Measure.addHaar_closedBall_center QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples instIsAddHaarMeasureRealVolume add_projection_respects_measure measurableSet_closedBall BorelSpace.opensMeasurable Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf CancelDenoms.add_subst Real.volume_closedBall ENNReal.ofReal_mul ENNReal.ofReal_ofNat min_eq_right Real.volume_Ioc sub_neg_eq_add add_halves CharZero.NeZero.two min_eq_left Mathlib.Tactic.Linarith.add_lt_of_le_of_neg

Function.Periodic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_le_sSup_add_zsmul_of_pos 📖	mathematical	Function.Periodic Real Real.instAdd IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instZero Real.instLT	Real.instLE intervalIntegral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal SupSet.sSup Real.instSupSet Set.image Set.Icc Real.instPreorder SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Real.instAddGroup Int.floor Real.instRing Real.linearOrder Real.instFloorRing DivInvMonoid.toDiv Real.instDivInvMonoid	—	intervalIntegrable₀ Int.fract_div_mul_self_add_zsmul_eq Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero 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_zero_add Mathlib.Tactic.Ring.add_pf_add_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.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing sub_eq_zero_of_eq intervalIntegral.integral_add_adjacent_intervals intervalIntegral_add_zsmul_eq intervalIntegral_add_eq zero_add add_le_add_iff_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le ContinuousOn.le_sSup_image_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Continuous.continuousOn intervalIntegral.continuous_primitive Real.noAtoms_volume Set.mem_Icc_of_Ico Int.fract_div_mul_self_mem_Ico
intervalIntegrable 📖	—	Function.Periodic Real Real.instAdd Real.instLT Real.instZero ENNReal ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm Real.instMin Top.top instTopENNReal IntervalIntegrable SeminormedAddCommGroup.toPseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup MeasureTheory.MeasureSpace.volume Real.measureSpace	—	—	exists_nat_ge Real.instIsOrderedRing Real.instArchimedean Set.uIcc_subset_uIcc_iff_le min_le_left le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr 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.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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono le_max_right IntervalIntegrable.mono_set PseudoEMetricSpace.pseudoMetrizableSpace Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.mul_one Nat.cast_add add_sub_cancel_left IntervalIntegrable.trans_iterate Int.cast_sub Int.cast_natCast sub_int_mul_eq Nat.cast_one Mathlib.Tactic.Ring.cast_pos IntervalIntegrable.comp_sub_right
intervalIntegrable₀ 📖	—	Function.Periodic Real Real.instAdd Real.instLT Real.instZero IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup MeasureTheory.MeasureSpace.volume Real.measureSpace	—	—	intervalIntegrable enorm_ne_top zero_add
intervalIntegral_add_eq 📖	mathematical	Function.Periodic Real Real.instAdd	intervalIntegral MeasureTheory.MeasureSpace.volume Real.measureSpace	—	lt_trichotomy intervalIntegral_add_eq_of_pos add_zero intervalIntegral.integral_same intervalIntegral.integral_symm add_sub_cancel_right neg neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
intervalIntegral_add_eq_add 📖	mathematical	Function.Periodic Real Real.instAdd IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup MeasureTheory.MeasureSpace.volume Real.measureSpace	intervalIntegral AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	intervalIntegral_add_eq intervalIntegral.integral_add_adjacent_intervals
intervalIntegral_add_eq_of_pos 📖	mathematical	Function.Periodic Real Real.instAdd Real.instLT Real.instZero	intervalIntegral MeasureTheory.MeasureSpace.volume Real.measureSpace	—	intervalIntegral.integral_of_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le LT.lt.le MeasureTheory.IsAddFundamentalDomain.setIntegral_eq AddSubgroup.instMeasurableConstVAdd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_of_add ContinuousAdd.measurableAdd Real.borelSpace IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.measure_preimage_add MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real AddSubgroup.instCountableSubtypeMemZMultiples isAddFundamentalDomain_Ioc map_vadd_zmultiples
intervalIntegral_add_zsmul_eq 📖	mathematical	Function.Periodic Real Real.instAdd IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup MeasureTheory.MeasureSpace.volume Real.measureSpace	intervalIntegral SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Real.instAddGroup NormedAddGroup.toAddGroup	—	zero_nsmul intervalIntegral.integral_same succ_nsmul intervalIntegral_add_eq_add zero_add zsmul_eq_mul Int.cast_natCast natCast_zsmul nsmul_eq_mul negSucc_zsmul Int.cast_negSucc Nat.cast_add Nat.cast_one neg_add_rev 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.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.atom_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.one_mul 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.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing intervalIntegral.integral_symm funext nsmul intervalIntegral.integral_comp_add_right add_comm intervalIntegral_add_eq zsmul
sInf_add_zsmul_le_integral_of_pos 📖	mathematical	Function.Periodic Real Real.instAdd IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instZero Real.instLT	Real.instLE InfSet.sInf Real.instInfSet Set.image intervalIntegral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.Icc Real.instPreorder SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Real.instAddGroup Int.floor Real.instRing Real.linearOrder Real.instFloorRing DivInvMonoid.toDiv Real.instDivInvMonoid	—	intervalIntegrable₀ Int.fract_div_mul_self_add_zsmul_eq Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero 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_zero_add Mathlib.Tactic.Ring.add_pf_add_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.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing sub_eq_zero_of_eq intervalIntegral.integral_add_adjacent_intervals intervalIntegral_add_zsmul_eq intervalIntegral_add_eq zero_add add_le_add_iff_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le ContinuousOn.sInf_image_Icc_le instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Continuous.continuousOn intervalIntegral.continuous_primitive Real.noAtoms_volume Set.mem_Icc_of_Ico Int.fract_div_mul_self_mem_Ico
tendsto_atBot_intervalIntegral_of_pos 📖	mathematical	Function.Periodic Real Real.instAdd Real.instLT Real.instZero intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace	Filter.Tendsto Filter.atBot Real.instPreorder	—	intervalIntegral.intervalIntegrable_of_integral_ne_zero LT.lt.ne' Filter.tendsto_atBot_mono integral_le_sSup_add_zsmul_of_pos Filter.tendsto_atBot_add_const_left Real.instIsOrderedAddMonoid Filter.Tendsto.atBot_zsmul_const Real.instArchimedean Filter.Tendsto.comp tendsto_floor_atBot Real.instIsStrictOrderedRing Filter.Tendsto.atBot_mul_const inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Filter.tendsto_id
tendsto_atBot_intervalIntegral_of_pos' 📖	mathematical	Function.Periodic Real Real.instAdd IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instZero Real.instLT	Filter.Tendsto intervalIntegral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Filter.atBot Real.instPreorder	—	tendsto_atBot_intervalIntegral_of_pos intervalIntegral.intervalIntegral_pos_of_pos
tendsto_atTop_intervalIntegral_of_pos 📖	mathematical	Function.Periodic Real Real.instAdd Real.instLT Real.instZero intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace	Filter.Tendsto Filter.atTop Real.instPreorder	—	intervalIntegral.intervalIntegrable_of_integral_ne_zero LT.lt.ne' Filter.tendsto_atTop_mono sInf_add_zsmul_le_integral_of_pos Filter.tendsto_atTop_add_const_left Real.instIsOrderedAddMonoid Filter.Tendsto.atTop_zsmul_const Real.instArchimedean Filter.Tendsto.comp tendsto_floor_atTop Real.instIsStrictOrderedRing Filter.Tendsto.atTop_mul_const inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Filter.tendsto_id
tendsto_atTop_intervalIntegral_of_pos' 📖	mathematical	Function.Periodic Real Real.instAdd IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instZero Real.instLT	Filter.Tendsto intervalIntegral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Filter.atTop Real.instPreorder	—	tendsto_atTop_intervalIntegral_of_pos intervalIntegral.intervalIntegral_pos_of_pos

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
memLp_liftIoc 📖	mathematical	MeasureTheory.MemLp Real Complex MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder Real.instAdd	AddCircle Real.instAddCommGroup AddCircle.measureSpace AddCircle.liftIoc Real.linearOrder Real.instIsOrderedAddMonoid Real.instArchimedean	—	Real.instIsOrderedAddMonoid Real.instArchimedean comp_measurePreserving MeasureTheory.MeasurePreserving.comp MeasureTheory.measurePreserving_subtype_coe measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal AddCircle.measurePreserving_equivIoc

UnitAddCircle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_preimage 📖	mathematical	—	MeasureTheory.integral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder Real.instAdd Real.instOne AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples UnitAddCircle AddCircle.measureSpace ZeroLEOneClass.factZeroLtOne Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike	—	AddCircle.integral_preimage ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
intervalIntegral_preimage 📖	mathematical	—	intervalIntegral Real AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne Real.instAdd MeasureTheory.MeasureSpace.volume Real.measureSpace MeasureTheory.integral UnitAddCircle MeasureTheory.MeasureSpace.toMeasurableSpace AddCircle.measureSpace ZeroLEOneClass.factZeroLtOne Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike	—	AddCircle.intervalIntegral_preimage ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
lintegral_preimage 📖	mathematical	—	MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder Real.instAdd Real.instOne AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples UnitAddCircle AddCircle.measureSpace ZeroLEOneClass.factZeroLtOne Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike	—	AddCircle.lintegral_preimage ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
measurePreserving_mk 📖	mathematical	—	MeasureTheory.MeasurePreserving Real UnitAddCircle MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace QuotientAddGroup.measurableSpace AddCommGroup.toAddGroup Real.instAddCommGroup Real.measurableSpace AddSubgroup.zmultiples Real.instOne MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder Real.instAdd AddCircle.measureSpace ZeroLEOneClass.factZeroLtOne Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike	—	ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
measure_univ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure UnitAddCircle MeasureTheory.MeasureSpace.toMeasurableSpace AddCircle.measureSpace Real Real.instOne ZeroLEOneClass.factZeroLtOne Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.MeasureSpace.volume Set.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike AddCircle.measure_univ ENNReal.ofReal_one

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAddFundamentalDomain_Ioc 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.IsAddFundamentalDomain AddSubgroup Real.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.zmultiples AddSubgroup.zero AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup.normedAddCommGroup Real.normedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddAction.instAddAction AddTorsor.toAddAction NormedAddTorsor.toAddTorsor NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddCommGroup.toNormedAddTorsor Real.measurableSpace Set.Ioc Real.instPreorder Real.instAdd	—	MeasureTheory.IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Equiv.bijective StrictMono.injective zsmul_left_strictMono Function.Bijective.existsUnique_iff add_comm existsUnique_add_zsmul_mem_Ioc Real.instArchimedean
isAddFundamentalDomain_Ioc' 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.IsAddFundamentalDomain AddOpposite AddSubgroup AddOpposite.instAddGroup Real.instAddGroup SetLike.instMembership AddSubgroup.instSetLike AddSubgroup.op AddSubgroup.zmultiples AddSubgroup.zero AddSubgroup.instVAdd Real.measurableSpace Set.Ioc Real.instPreorder Real.instAdd	—	MeasureTheory.IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Equiv.bijective StrictMono.injective zsmul_left_strictMono Function.Bijective.existsUnique_iff Function.Bijective.comp zsmul_eq_mul Set.codRestrict.congr_simp existsUnique_add_zsmul_mem_Ioc Real.instArchimedean

---

← Back to Index