ContDiff

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

Statistics

Metric	Count
Definitions ContDiff	1
Theorems enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc, enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc, integral_derivWithin_Icc_of_contDiffOn_Icc, integral_derivWithin_uIcc_of_contDiffOn_uIcc, integral_deriv_of_contDiffOn_Icc, integral_deriv_of_contDiffOn_uIcc	6
Total	7

(root)

Definitions

Name	Category	Theorems
ContDiff 📖	MathDef	225 math math: ContinuousMap.dense_setOf_contDiff, ContDiff.sub, contDiff_fst, contDiff_prod_iff, smooth_barycentric_coord, PiLp.contDiff_toLp, IsBoundedLinearMap.contDiff, MeasureTheory.contDiff_charFun', ContDiff.fderiv_succ, ContDiff.fst, ContDiff.div_const, ContDiffMapSupportedInClass.map_contDiff, OpenPartialHomeomorph.contDiff_unitBallBall_symm, ContDiff.iteratedFDeriv_right, ContinuousLinearEquiv.contDiff_comp_iff, contDiff_prodAssoc_symm, ContDiff.sigmoid, ContDiffOn.comp_contDiff, contDiff_piLp', Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le, ContDiff.pow, IsOpen.exists_smooth_support_eq, contDiff_id, contDiff_one_iff_fderiv, contDiff_nat_succ_iff_contDiff_one_iteratedDeriv, contDiff_zero, ContDiffMapSupportedIn.contDiff, contDiff_prodAssoc, Homeomorph.contDiff_unitBall, ContDiffMapSupportedIn.contDiff', exists_smooth_tsupport_subset, Continuous.exists_contDiff_approx_and_eqOn, MeasureTheory.MemLp.exist_eLpNorm_sub_le, Complex.contDiff_cosh, ContDiff.arctan, ContDiff.ccos, OpenPartialHomeomorph.contDiff_univUnitBall, contDiff_iff_forall_nat_le, contDiff_succ_iff_fderiv, TestFunction.contDiff, ContDiff.cos, ContDiff.cexp, contDiff_circleMap, ContDiff.prodMk, contDiff_apply, ContDiff.log, LinearIsometryEquiv.contDiff, Function.hasTemperateGrowth_iff_isBigO, contDiff_all_iff_nat, ContDiffBump.contDiff, ContDiff.fun_comp, contDiff_update, contDiff_prodMk_right, ContDiff.prodMap, ContDiff.norm_rpow, ContDiff.fst', IsBoundedBilinearMap.contDiff, ContDiff.sin, contMDiff_vectorSpace_iff_contDiff, AnalyticOnNhd.contDiff, contDiff_bernoulliFun, contDiff_iff_iteratedDeriv, ContDiff.sum, ContDiff.euclidean_dist, contDiff_const, contDiff_const_smul, contDiff_iff_continuous_differentiable, contDiff_nat_iff_iteratedDeriv, ExistsContDiffBumpBase.u_exists, contMDiff_iff_contDiff, WithLp.contDiff_toLp, ContDiff.norm_sq, contDiff_of_differentiable_iteratedFDeriv, contDiff_pi', ContinuousAffineMap.contDiff, ContinuousMultilinearMap.contDiff, Real.contDiff_arsinh, Real.contDiff_fourierIntegral, Homeomorph.contDiff_symm, ContDiff.smulRight, ContDiff.rpow, ContDiff.comp_continuousLinearMap, ContDiff.exp, contDiff_norm_sq, contDiff_apply_apply, ContDiff.inner, Complex.contDiff_exp, Real.contDiff_sin, WithLp.contDiff_ofLp, Diffeomorph.contDiff, contDiff_smul_const, contDiff_piLp, ContDiff.smul_const, ContDiff.ccosh, Real.contDiff_cos, ContDiff.iterate_deriv, ContDiff.deriv', contDiff_succ_iff_fderiv_apply, OpenPartialHomeomorph.contDiff_univBall, ContDiff.clm_comp, ContDiff.fderiv_apply, contDiff_add, ExistsContDiffBumpBase.u_smooth, Real.contDiff_fourier, Differentiable.contDiff, ContDiff.fourierPowSMulRight, contDiff_neg, OpenPartialHomeomorph.contDiff_unitBallBall, ContDiff.rpow_const_of_le, ContDiff.of_le, VectorFourier.contDiff_fourierIntegral, ContDiffBump.contDiff_normed, ContDiff.comp, Diffeology.isPlot_iff_contDiff, ContDiff.rpow_const_of_ne, contDiff_clm_apply_iff, HasCompactSupport.contDiff_convolution_left, contDiff_iff_ftaylorSeries, ContDiff.smul, Complex.contDiff_sinh, ContDiff.of_succ, ContDiff.add, expNegInvGlue.contDiff, ContDiff.inversion, Diffeology.IsContDiffCompatible.isPlot_iff, contDiff_prod', contDiff_of_subsingleton, ContDiff.iteratedFDeriv_right', Real.contDiff_sinh, MeasureTheory.LocallyIntegrable.exists_contDiff_dist_le_of_forall_mem_ball_dist_le, contDiff_nat_iff_continuous_differentiable, contDiff_inner, ContDiff.comp₂, ContDiff.inv, Real.contDiff_arctan, contDiff_single, ContDiff.one_of_succ, Diffeology.IsPlot.contDiff, contDiff_of_contDiffOn_iUnion_of_isOpen, contDiff_stereoInvFunAux, expNegInvGlue.contDiff_polynomial_eval_inv_mul, contDiff_one_iff_hasFDerivAt, ContDiff.dist, contDiff_mul, PiLp.contDiff_ofLp, Real.contDiff_cosh, MeasureTheory.contDiff_charFun, contDiff_omega_iff_analyticOnNhd, ContDiff.iterate_deriv', ContDiff.clm_apply, contDiff_smul, IsOpen.exists_contDiff_support_eq, contDiff_piLp_apply, Real.contDiff_rpow_const_of_le, LinearIsometry.contDiff, ContDiff.lieBracket_vectorField, contDiff_fun_id, Continuous.exists_contDiff_approx, ContMDiff.contDiff, ContDiff.abs, contDiff_succ_iff_deriv, TestFunction.contDiff', contDiff_of_contDiffOn_union_of_isOpen, HasFTaylorSeriesUpTo.contDiff, Polynomial.contDiff_aeval, ContDiff.norm, contDiff_infty_iff_deriv, ContDiff.sqrt, Function.Periodic.contDiff_qParam, contDiff_of_differentiable_iteratedDeriv, ContDiff.contDiff_fderiv_apply, ContDiff.csinh, contDiff_tsum, contDiff_infty, ContDiff.neg, UniformContinuous.exists_contDiff_dist_le, ContDiff.comp₃, ContDiff.contDiffBump, ContDiff.sinh, contDiff_tsum_of_eventually, ContDiff.snd', Homeomorph.contDiff_symm_deriv, ContinuousLinearMap.contDiff, HasCompactSupport.exist_eLpNorm_sub_le_of_continuous, contDiff_norm_rpow, exists_contDiff_tsupport_subset, ContDiff.restrict_scalars, SchwartzMap.smooth', Real.contDiff_exp, ContDiff.fderiv_right, ContinuousLinearEquiv.comp_contDiff_iff, MeasureTheory.Lp.dense_hasCompactSupport_contDiff, contDiff_snd, ContDiff.continuousLinearMap_comp, contDiff_infty_iff_fderiv, Complex.contDiff_sin, Complex.contDiff_cos, HasCompactSupport.contDiff_convolution_right, contDiffOn_univ, Diffeology.DSmooth.contDiff, ContDiff.real_of_complex, contDiff_iff_contDiffAt, ContDiff.fderiv, ContDiff.csin, SchwartzMap.smooth, contDiff_pi, TestFunctionClass.map_contDiff, ContDiff.fun_smul, AnalyticOn.contDiff, contDiff_prodMk_left, ContDiff.const_smul, ContDiff.arsinh, contDiff_sigmoid, contDiff_euclidean, contDiff_prod, contDiff_succ_iff_hasFDerivAt, ContDiff.mul, contDiff_one_iff_deriv, ContDiff.snd, ContDiff.cosh, ContDiff.div, contDiff_zero_fun, Real.smoothTransition.contDiff, ContinuousLinearEquiv.contDiff, Diffeology.dSmooth_iff_contDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set.Icc Real.instPreorder Real.instLE	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Icc Real.instPreorder derivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField SeminormedAddCommGroup.toPseudoMetricSpace	—	LE.le.trans_eq enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc MeasureTheory.lintegral_congr_ae MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.restrict_Ioo_eq_restrict_Icc Real.noAtoms_volume Filter.mp_mem MeasureTheory.self_mem_ae_restrict measurableSet_Ioo BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.univ_mem' derivWithin_of_mem_nhds Icc_mem_nhds
enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set.Icc Real.instPreorder Real.instLE	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Icc Real.instPreorder deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField SeminormedAddCommGroup.toPseudoMetricSpace	—	SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul edist_eq_enorm_sub Isometry.edist_eq LinearIsometry.isometry intervalIntegral.integral_deriv_of_contDiffOn_Icc UniformSpace.Completion.completeSpace ContDiff.comp_contDiffOn LinearIsometry.contDiff intervalIntegral.integral_of_le MeasureTheory.restrict_Ioc_eq_restrict_Icc Real.noAtoms_volume LE.le.trans MeasureTheory.enorm_integral_le_lintegral_enorm MeasureTheory.lintegral_mono_ae MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.restrict_Ioo_eq_restrict_Icc Filter.mp_mem MeasureTheory.self_mem_ae_restrict measurableSet_Ioo BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.univ_mem' fderiv_comp_deriv Differentiable.differentiableAt ContDiff.differentiable one_ne_zero NeZero.charZero_one WithTop.charZero ContDiffAt.differentiableAt ContDiffWithinAt.contDiffAt LT.lt.le Icc_mem_nhds ContinuousLinearMap.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul UniformSpace.Completion.instIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace LinearIsometry.enorm_map instReflLe

intervalIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_derivWithin_Icc_of_contDiffOn_Icc 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set.Icc Real.instPreorder Real.instLE	intervalIntegral derivWithin Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.Icc Real.instPreorder MeasureTheory.MeasureSpace.volume Real.measureSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	integral_deriv_of_contDiffOn_Icc integral_of_le MeasureTheory.integral_congr_ae MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.restrict_Ioo_eq_restrict_Ioc Real.noAtoms_volume Filter.mp_mem MeasureTheory.self_mem_ae_restrict measurableSet_Ioo BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.univ_mem' derivWithin_of_mem_nhds Icc_mem_nhds
integral_derivWithin_uIcc_of_contDiffOn_uIcc 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set.uIcc Real.lattice	intervalIntegral derivWithin Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.uIcc Real.lattice MeasureTheory.MeasureSpace.volume Real.measureSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	le_or_gt Set.uIcc_of_le integral_derivWithin_Icc_of_contDiffOn_Icc Set.uIcc_of_ge LT.lt.le integral_symm Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_termg add_zero
integral_deriv_of_contDiffOn_Icc 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set.Icc Real.instPreorder Real.instLE	intervalIntegral deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.MeasureSpace.volume Real.measureSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	LE.le.eq_or_lt integral_same sub_self integral_eq_sub_of_hasDerivAt_of_le ContDiffOn.continuousOn DifferentiableAt.hasDerivAt DifferentiableWithinAt.differentiableAt ContDiffWithinAt.differentiableWithinAt LT.lt.le one_ne_zero NeZero.charZero_one WithTop.charZero Icc_mem_nhds HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContDiffOn.derivWithin uniqueDiffOn_Icc zero_add instReflLe IntervalIntegrable.congr_ae PseudoEMetricSpace.pseudoMetrizableSpace ContinuousOn.intervalIntegrable_of_Icc Real.locallyFinite_volume MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae.congr_simp Set.uIoc_of_le MeasureTheory.restrict_Ioo_eq_restrict_Ioc Real.noAtoms_volume Filter.mp_mem MeasureTheory.self_mem_ae_restrict measurableSet_Ioo BorelSpace.opensMeasurable Real.borelSpace Filter.univ_mem' derivWithin_of_mem_nhds
integral_deriv_of_contDiffOn_uIcc 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Set.uIcc Real.lattice	intervalIntegral deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.MeasureSpace.volume Real.measureSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	le_or_gt integral_deriv_of_contDiffOn_Icc Set.uIcc_of_le integral_symm Set.uIcc_of_ge LT.lt.le Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_termg add_zero

---

← Back to Index