PoissonSummation

📁 Source: Mathlib/Analysis/Fourier/PoissonSummation.lean

Statistics

Metric	Count
Definitions	0
Theorems fourierCoeff_tsum_comp_add, tsum_eq_tsum_fourier, tsum_eq_tsum_fourierIntegral, tsum_eq_tsum_fourierIntegral_of_rpow_decay, tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable, tsum_eq_tsum_fourier_of_rpow_decay, tsum_eq_tsum_fourier_of_rpow_decay_of_summable, tsum_eq_tsum_fourier, tsum_eq_tsum_fourierIntegral, isBigO_norm_Icc_restrict_atBot, isBigO_norm_Icc_restrict_atTop, isBigO_norm_restrict_cocompact	12
Total	12

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourierCoeff_tsum_comp_add 📖	mathematical	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Norm.norm ContinuousMap Set.Elem SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike Complex instTopologicalSpaceSubtype Set Set.instMembership SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instNorm ContinuousMap.instCompactSpaceElemCoeCompacts NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing ContinuousMap.restrict ContinuousMap.comp ContinuousMap.addRight instAdd IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIntCast SummationFilter.unconditional	fourierCoeff instOne ZeroLEOneClass.factZeroLtOne instZero partialOrder instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing RCLike.charZero_rclike instRCLike Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Function.Periodic.lift DFunLike.coe ContinuousMap.instFunLike tsum ContinuousMap.instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.compactOpen AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ContinuousMap.periodic_tsum_comp_add_zsmul Complex.instT2Space FourierTransform.fourier instFourierTransform normedAddCommGroup RCLike.toInnerProductSpaceReal measurableSpace borelSpace FiniteDimensional.rclike_to_real	—	ContinuousMap.instCompactSpaceElemCoeCompacts IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_quotient_mk' IsTopologicalSemiring.toContinuousMul IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Circle.norm_coe AddSubgroup.normal_of_comm ContinuousMap.norm_eq_iSup_norm norm_mul NormedDivisionRing.toNormMulClass one_mul ContinuousMap.ext Function.Periodic.comp AddCircle.coe_add_period mul_one Function.Periodic.int_mul ZeroLEOneClass.factZeroLtOne instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike ContinuousMap.periodic_tsum_comp_add_zsmul Complex.instT2Space borelSpace FiniteDimensional.rclike_to_real fourierCoeff_eq_intervalIntegral div_one one_smul zero_add ContinuousMap.addRight.congr_simp zsmul_one IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMap.tsum_apply ContinuousMap.summable_of_locally_summable_norm locallyCompact_of_proper instProperSpaceReal Complex.instCompleteSpace SummationFilter.instNeBotUnconditional tsum_mul_left intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm instCountableInt isCompact_uIcc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal integrable_of_summable_norm_Icc compactSpace_Icc CompactIccSpace.isCompact_Icc HasSum.tsum_eq MeasureTheory.Integrable.hasSum_intervalIntegral_comp_add_int Nat.instAtLeastTwoHAddOfNat fourier_real_eq_integral_exp_smul smul_eq_mul ContinuousMap.comp_apply ContinuousMap.continuous_toFun ContinuousMap.toFun_eq_coe fourier_coe_apply Int.cast_neg Complex.ofReal_mul Complex.ofReal_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_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.mul_pf_left Mathlib.Tactic.Ring.neg_congr 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 Nat.cast_one Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat
tsum_eq_tsum_fourier 📖	mathematical	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Norm.norm ContinuousMap Set.Elem SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike Complex instTopologicalSpaceSubtype Set Set.instMembership SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instNorm ContinuousMap.instCompactSpaceElemCoeCompacts NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing ContinuousMap.restrict ContinuousMap.comp ContinuousMap.addRight instAdd IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIntCast SummationFilter.unconditional ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup FourierTransform.fourier instFourierTransform InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace normedAddCommGroup RCLike.toInnerProductSpaceReal instRCLike measurableSpace borelSpace FiniteDimensional.rclike_to_real DFunLike.coe ContinuousMap.instFunLike	tsum Complex.instMul AddCircle instAddCommGroup instOne QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples fourier	—	ContinuousMap.instCompactSpaceElemCoeCompacts IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal borelSpace FiniteDimensional.rclike_to_real IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMap.periodic_tsum_comp_add_zsmul Complex.instT2Space continuous_coinduced_dom ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass ZeroLEOneClass.factZeroLtOne instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike fourierCoeff_tsum_comp_add Function.Periodic.lift.congr_simp ContinuousMap.addRight.congr_simp zsmul_one HasSum.tsum_eq IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup SummationFilter.instNeBotUnconditional ContinuousMap.hasSum_apply Summable.hasSum ContinuousMap.summable_of_locally_summable_norm locallyCompact_of_proper instProperSpaceReal Complex.instCompleteSpace has_pointwise_sum_fourier_series_of_summable
tsum_eq_tsum_fourierIntegral 📖	mathematical	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace Norm.norm ContinuousMap Set.Elem SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike Complex instTopologicalSpaceSubtype Set Set.instMembership SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ContinuousMap.instNorm ContinuousMap.instCompactSpaceElemCoeCompacts NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing ContinuousMap.restrict ContinuousMap.comp ContinuousMap.addRight instAdd IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instIntCast SummationFilter.unconditional ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup FourierTransform.fourier instFourierTransform InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace normedAddCommGroup RCLike.toInnerProductSpaceReal instRCLike measurableSpace borelSpace FiniteDimensional.rclike_to_real DFunLike.coe ContinuousMap.instFunLike	tsum Complex.instMul AddCircle instAddCommGroup instOne QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples fourier	—	tsum_eq_tsum_fourier
tsum_eq_tsum_fourierIntegral_of_rpow_decay 📖	mathematical	Continuous Real Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instLT instOne Asymptotics.IsBigO Complex.instNorm norm Filter.cocompact instPow abs lattice instAddGroup instNeg FourierTransform.fourier instFourierTransform Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace normedAddCommGroup RCLike.toInnerProductSpaceReal instRCLike measurableSpace borelSpace FiniteDimensional.rclike_to_real	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instAdd instIntCast SummationFilter.unconditional Complex.instMul DFunLike.coe ContinuousMap AddCircle instAddCommGroup QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ContinuousMap.instFunLike fourier	—	tsum_eq_tsum_fourier_of_rpow_decay
tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable 📖	mathematical	Continuous Real Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instLT instOne Asymptotics.IsBigO Complex.instNorm norm Filter.cocompact instPow abs lattice instAddGroup instNeg Summable ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup FourierTransform.fourier instFourierTransform InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace normedAddCommGroup RCLike.toInnerProductSpaceReal instRCLike measurableSpace borelSpace FiniteDimensional.rclike_to_real instIntCast SummationFilter.unconditional	tsum instAdd Complex.instMul DFunLike.coe ContinuousMap AddCircle instAddCommGroup QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ContinuousMap.instFunLike fourier	—	tsum_eq_tsum_fourier_of_rpow_decay_of_summable
tsum_eq_tsum_fourier_of_rpow_decay 📖	mathematical	Continuous Real Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instLT instOne Asymptotics.IsBigO Complex.instNorm norm Filter.cocompact instPow abs lattice instAddGroup instNeg FourierTransform.fourier instFourierTransform Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace normedAddCommGroup RCLike.toInnerProductSpaceReal instRCLike measurableSpace borelSpace FiniteDimensional.rclike_to_real	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instAdd instIntCast SummationFilter.unconditional Complex.instMul DFunLike.coe ContinuousMap AddCircle instAddCommGroup QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ContinuousMap.instFunLike fourier	—	borelSpace FiniteDimensional.rclike_to_real tsum_eq_tsum_fourier_of_rpow_decay_of_summable summable_of_isBigO Complex.instCompleteSpace summable_abs_int_rpow Asymptotics.IsBigO.comp_tendsto Int.tendsto_coe_cofinite
tsum_eq_tsum_fourier_of_rpow_decay_of_summable 📖	mathematical	Continuous Real Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField instLT instOne Asymptotics.IsBigO Complex.instNorm norm Filter.cocompact instPow abs lattice instAddGroup instNeg Summable ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup FourierTransform.fourier instFourierTransform InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace normedAddCommGroup RCLike.toInnerProductSpaceReal instRCLike measurableSpace borelSpace FiniteDimensional.rclike_to_real instIntCast SummationFilter.unconditional	tsum instAdd Complex.instMul DFunLike.coe ContinuousMap AddCircle instAddCommGroup QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ContinuousMap.instFunLike fourier	—	borelSpace FiniteDimensional.rclike_to_real tsum_eq_tsum_fourier summable_of_isBigO instCompleteSpace ContinuousMap.instCompactSpaceElemCoeCompacts IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal summable_abs_int_rpow Asymptotics.IsBigO.comp_tendsto isBigO_norm_restrict_cocompact LT.lt.trans zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Int.tendsto_coe_cofinite

SchwartzMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tsum_eq_tsum_fourier 📖	mathematical	—	tsum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup DFunLike.coe SchwartzMap Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex instFunLike Real.instAdd Real.instIntCast SummationFilter.unconditional Complex.instMul NormedSpace.complexToReal Complex.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.innerProductSpace FourierTransform.fourier instFourierTransform FiniteDimensional.rclike_to_real Real.measurableSpace Real.borelSpace ContinuousMap AddCircle Real.instAddCommGroup Real.instOne QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ContinuousMap.instFunLike fourier	—	Real.tsum_eq_tsum_fourier_of_rpow_decay continuous Nat.instAtLeastTwoHAddOfNat one_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid isBigO_cocompact_rpow instProperSpaceReal FiniteDimensional.rclike_to_real Real.borelSpace
tsum_eq_tsum_fourierIntegral 📖	mathematical	—	tsum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup DFunLike.coe SchwartzMap Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instInnerProductSpaceRealComplex instFunLike Real.instAdd Real.instIntCast SummationFilter.unconditional Complex.instMul NormedSpace.complexToReal Complex.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing RCLike.innerProductSpace FourierTransform.fourier instFourierTransform FiniteDimensional.rclike_to_real Real.measurableSpace Real.borelSpace ContinuousMap AddCircle Real.instAddCommGroup Real.instOne QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ContinuousMap.instFunLike fourier	—	tsum_eq_tsum_fourier

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBigO_norm_Icc_restrict_atBot 📖	mathematical	Real Real.instLT Real.instZero Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter.atBot Real.instPreorder DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousMap.instFunLike Real.instPow abs Real.lattice Real.instAddGroup Real.instNeg	Norm.norm Set.Elem Set.Icc Real.instAdd instTopologicalSpaceSubtype Set Set.instMembership ContinuousMap.instNorm compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace Real.instConditionallyCompleteLinearOrder instOrderTopologyReal ContinuousMap.restrict	—	ContinuousNeg.continuous_neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal abs_neg Asymptotics.IsBigO.comp_tendsto Filter.tendsto_neg_atTop_atBot Real.instIsOrderedAddMonoid compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal isBigO_norm_Icc_restrict_atTop Filter.tendsto_neg_atBot_atTop Asymptotics.IsBigO.trans Asymptotics.isBigO_of_le norm_norm ContinuousMap.norm_le norm_nonneg LE.le.trans 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.neg_congr Mathlib.Tactic.Ring.atom_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.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat 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 Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le le_of_eq ContinuousMap.comp_apply ContinuousMap.continuous_toFun neg_neg ContinuousMap.norm_coe_le_norm
isBigO_norm_Icc_restrict_atTop 📖	mathematical	Real Real.instLT Real.instZero Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter.atTop Real.instPreorder DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousMap.instFunLike Real.instPow abs Real.lattice Real.instAddGroup Real.instNeg	Norm.norm Set.Elem Set.Icc Real.instAdd instTopologicalSpaceSubtype Set Set.instMembership ContinuousMap.instNorm compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace Real.instConditionallyCompleteLinearOrder instOrderTopologyReal ContinuousMap.restrict	—	Nat.instAtLeastTwoHAddOfNat max_lt_iff Real.mul_rpow le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo Real.rpow_le_rpow_of_nonpos lt_of_not_ge 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 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.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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.mul_pf_right 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.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.mul_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true le_of_not_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.mul_neg compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal Asymptotics.IsBigO.exists_pos Asymptotics.IsBigO_def Asymptotics.IsBigOWith_def instIsDirectedOrder Real.instArchimedean neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one max_le_iff norm_norm ContinuousMap.norm_le mul_nonneg IsOrderedRing.toPosMulMono mul_pos Real.rpow_pos_of_pos norm_nonneg LE.le.trans Real.rpow_nonneg abs_nonneg IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add mul_assoc mul_le_mul_iff_right₀ Real.norm_of_nonneg abs_of_nonneg abs_of_pos
isBigO_norm_restrict_cocompact 📖	mathematical	Real Real.instLT Real.instZero Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe ContinuousMap SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousMap.instFunLike Real.instPow abs Real.lattice Real.instAddGroup Real.instNeg	Norm.norm Set.Elem SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike instTopologicalSpaceSubtype Set Set.instMembership ContinuousMap.instNorm ContinuousMap.instCompactSpaceElemCoeCompacts ContinuousMap.restrict ContinuousMap.comp ContinuousMap.addRight Real.instAdd IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal	—	ContinuousMap.instCompactSpaceElemCoeCompacts IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Bornology.IsBounded.subset_closedBall IsCompact.isBounded TopologicalSpace.Compacts.isCompact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal ContinuousMap.norm_le norm_nonneg LE.le.trans 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero 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 Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le zero_sub zero_add Real.closedBall_eq_Icc le_of_eq ContinuousMap.norm_coe_le_norm cocompact_eq_atBot_atTop instNoMaxOrderOfNontrivial Real.instNontrivial instNoMinOrderOfNontrivial HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Asymptotics.IsBigO.trans Asymptotics.isBigO_of_le norm_norm isBigO_norm_Icc_restrict_atBot isBigO_norm_Icc_restrict_atTop

---

← Back to Index