Basic

📁 Source: Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems integral_const_on_unit_interval, integral_cos, integral_cos_mul_complex, integral_cos_pow, integral_cos_pow_aux, integral_cos_pow_three, integral_cos_sq, integral_cos_sq_sub_sin_sq, integral_cpow, integral_div_sq_add_sq, integral_exp, integral_exp_mul_I_eq_sin, integral_exp_mul_I_eq_sinc, integral_exp_mul_complex, integral_id, integral_inv, integral_inv_of_neg, integral_inv_of_pos, integral_inv_one_add_sq, integral_inv_sq_add_sq, integral_log, integral_log_from_zero, integral_log_from_zero_of_pos, integral_mul_cpow_one_add_sq, integral_mul_rpow_one_add_sq, integral_one, integral_one_div, integral_one_div_of_neg, integral_one_div_of_pos, integral_one_div_one_add_sq, integral_pow, integral_pow_abs_sub_uIoc, integral_rpow, integral_sin, integral_sin_mul_cos_sq, integral_sin_mul_cos₁, integral_sin_mul_cos₂, integral_sin_pow, integral_sin_pow_antitone, integral_sin_pow_aux, integral_sin_pow_even, integral_sin_pow_even_mul_cos_pow_even, integral_sin_pow_mul_cos_pow_odd, integral_sin_pow_odd, integral_sin_pow_odd_mul_cos_pow, integral_sin_pow_pos, integral_sin_pow_succ_le, integral_sin_pow_three, integral_sin_sq, integral_sin_sq_mul_cos, integral_sin_sq_mul_cos_sq, integral_sqrt_one_sub_sq, integral_zpow, inv_mul_integral_comp_add_div, inv_mul_integral_comp_div, inv_mul_integral_comp_div_add, inv_mul_integral_comp_div_sub, inv_mul_integral_comp_sub_div, mul_integral_comp_add_mul, mul_integral_comp_mul_add, mul_integral_comp_mul_left, mul_integral_comp_mul_right, mul_integral_comp_mul_sub, mul_integral_comp_sub_mul	64
Total	64

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_const_on_unit_interval 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instAdd Real.instOne MeasureTheory.MeasureSpace.volume Real.measureSpace	—	intervalIntegral.integral_const Real.instCompleteSpace add_sub_cancel_left one_mul
integral_cos 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.sin	—	intervalIntegral.integral_deriv_eq_sub' Real.instCompleteSpace Real.deriv_sin Real.continuousOn_cos
integral_cos_mul_complex 📖	mathematical	—	intervalIntegral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.cos Complex.instMul Complex.ofReal MeasureTheory.MeasureSpace.volume Real.measureSpace Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.sin	—	intervalIntegral.integral_eq_sub_of_hasDerivAt Complex.instCompleteSpace ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.hasDerivAt_sin IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology hasDerivAt_mul_const HasDerivAt.comp IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.comp_ofReal HasDerivAt.div_const mul_comm mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass HasDerivAt.congr_simp Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.comp' Complex.continuous_cos Continuous.fun_mul continuous_const continuous_id' Complex.continuous_ofReal
integral_cos_pow 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instMul Real.sin Real.instNatCast instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.instOne	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_nonneg' Real.instZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw eq_sub_iff_add_eq integral_cos_pow_aux
integral_cos_pow_aux 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.instAdd Real.instMul Real.sin Real.instNatCast Real.instOne	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.congr_simp neg_mul mul_right_comm IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mul_neg HasDerivAt.pow Real.hasDerivAt_cos Real.hasDerivAt_sin intervalIntegral.integral_mul_deriv_eq_deriv_mul Real.instCompleteSpace Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.comp' continuous_mul IsTopologicalSemiring.toContinuousMul Continuous.prodMk Continuous.fun_mul continuous_const continuous_id' Real.continuous_sin Continuous.pow Real.continuous_cos pow_succ Nat.cast_add Nat.cast_one intervalIntegral.integral_neg intervalIntegral.integral_const_mul sub_neg_eq_add sq Real.sin_sq sub_mul one_mul add_comm intervalIntegral.integral_sub mul_sub add_sub_assoc
integral_cos_pow_three 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.sin DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	integral_sin_pow_mul_cos_pow_odd Mathlib.Meta.NormNum.instAtLeastTwo pow_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat one_mul pow_one intervalIntegral.integral_sub Real.locallyFinite_volume Nat.cast_one enorm_one NormedDivisionRing.to_normOneClass intervalIntegral.integral_const Real.instCompleteSpace mul_one integral_pow Mathlib.Meta.NormNum.isNat_natCast
integral_cos_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instAdd Real.instMul Real.sin instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat integral_cos_pow zero_add pow_one CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike one_div pow_zero intervalIntegral.integral_const Real.instCompleteSpace mul_one add_sub_assoc Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
integral_cos_sq_sub_sin_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instSub Monoid.toNatPow Real.instMonoid Real.cos Real.sin MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instMul	—	sq sub_eq_add_neg neg_mul_eq_mul_neg intervalIntegral.integral_deriv_mul_eq_sub Real.instCompleteSpace Real.hasDerivAt_sin Real.hasDerivAt_cos ContinuousOn.intervalIntegrable Real.locallyFinite_volume Real.continuousOn_cos ContinuousOn.neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal Real.continuousOn_sin
integral_cpow 📖	mathematical	Real Real.instLT Real.instNeg Real.instOne Complex.re Set Set.instMembership Set.uIcc Real.lattice Real.instZero	intervalIntegral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.instPow Complex.ofReal MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instSub Complex.instAdd Complex.instOne	—	sub_div Complex.add_re Complex.one_re Complex.zero_re add_eq_zero_iff_eq_neg LT.lt.ne' intervalIntegral.integral_eq_sub_of_hasDerivAt Complex.instCompleteSpace hasDerivAt_ofReal_cpow_const' Mathlib.Tactic.Contrapose.contrapose₄ intervalIntegral.intervalIntegrable_cpow Real.locallyFinite_volume intervalIntegral.integral_eq_sub_of_hasDeriv_right Continuous.continuousOn Continuous.div_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.continuous_ofReal_cpow_const neg_lt_iff_pos_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid HasDerivAt.hasDerivWithinAt le_total LT.lt.ne max_eq_left min_eq_left Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.add_pf_add_overlap_zero 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 intervalIntegral.intervalIntegrable_cpow' intervalIntegral.integral_add_adjacent_intervals intervalIntegral.integral_symm Complex.zero_cpow Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' 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.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt
integral_div_sq_add_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd Monoid.toNatPow Real.instMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.arctan	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero zero_pow Nat.instCharZero zero_add MulZeroClass.zero_mul intervalIntegral.integral_zero div_zero Real.arctan_zero sub_self intervalIntegral.integral_const_mul integral_inv_sq_add_sq Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
integral_exp 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.exp MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub	—	intervalIntegral.integral_deriv_eq_sub' Real.instCompleteSpace Real.deriv_exp Real.differentiableAt_exp Real.continuousOn_exp
integral_exp_mul_I_eq_sin 📖	mathematical	—	intervalIntegral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.exp Complex.instMul Complex.ofReal Complex.I Real.instNeg MeasureTheory.MeasureSpace.volume Real.measureSpace instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.sin	—	Nat.instAtLeastTwoHAddOfNat mul_comm integral_exp_mul_complex Complex.ofReal_neg mul_neg Complex.div_I Complex.exp_mul_I Complex.cos_neg Complex.sin_neg add_sub_add_left_eq_sub Complex.ofReal_sin sub_mul mul_assoc two_mul Complex.I_mul_I mul_one neg_neg neg_sub sub_neg_eq_add
integral_exp_mul_I_eq_sinc 📖	mathematical	—	intervalIntegral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.exp Complex.instMul Complex.ofReal Complex.I Real.instNeg MeasureTheory.MeasureSpace.volume Real.measureSpace instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.sinc	—	Nat.instAtLeastTwoHAddOfNat integral_exp_mul_I_eq_sin Real.sin_zero MulZeroClass.mul_zero Real.sinc_zero mul_one Real.sinc_of_ne_zero Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf
integral_exp_mul_complex 📖	mathematical	—	intervalIntegral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.exp Complex.instMul Complex.ofReal MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instSub	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass HasDerivAt.div_const HasDerivAt.comp Complex.hasDerivAt_exp HasDerivAt.congr_simp mul_one HasDerivAt.comp_ofReal HasDerivAt.const_mul hasDerivAt_id intervalIntegral.integral_deriv_eq_sub' Complex.instCompleteSpace HasDerivAt.deriv HasDerivAt.differentiableAt ContinuousOn.cexp ContinuousOn.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuousOn_const Continuous.continuousOn Complex.continuous_ofReal Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul 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 Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one
integral_id 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	integral_pow Mathlib.Meta.NormNum.instAtLeastTwo pow_one Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_natCast Nat.cast_one
integral_inv 📖	mathematical	Real Set Set.instMembership Set.uIcc Real.lattice Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instInv MeasureTheory.MeasureSpace.volume Real.measureSpace Real.log DivInvMonoid.toDiv Real.instDivInvMonoid	—	intervalIntegral.integral_deriv_eq_sub' Real.instCompleteSpace Real.deriv_log' Real.differentiableAt_log ContinuousOn.mono continuousOn_inv₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Set.subset_compl_singleton_iff Real.log_div Set.right_mem_uIcc Set.left_mem_uIcc
integral_inv_of_neg 📖	mathematical	Real Real.instLT Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instInv MeasureTheory.MeasureSpace.volume Real.measureSpace Real.log DivInvMonoid.toDiv Real.instDivInvMonoid	—	integral_inv Set.notMem_uIcc_of_gt
integral_inv_of_pos 📖	mathematical	Real Real.instLT Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instInv MeasureTheory.MeasureSpace.volume Real.measureSpace Real.log DivInvMonoid.toDiv Real.instDivInvMonoid	—	integral_inv Set.notMem_uIcc_of_lt
integral_inv_one_add_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instInv Real.instAdd Real.instOne Monoid.toNatPow Real.instMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.arctan	—	integral_one_div_one_add_sq
integral_inv_sq_add_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instInv Real.instAdd Monoid.toNatPow Real.instMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instMul Real.instSub Real.arctan DivInvMonoid.toDiv Real.instDivInvMonoid	—	Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial intervalIntegral.integral_comp_div intervalIntegral.integral_const_mul integral_inv_one_add_sq Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.cons_ne_zero
integral_log 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instAdd Real.instSub Real.instMul	—	intervalIntegral.integral_add_adjacent_intervals intervalIntegral.intervalIntegrable_log' intervalIntegral.integral_symm integral_log_from_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
integral_log_from_zero 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log Real.instZero MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.instMul	—	lt_trichotomy Real.log_neg_eq_log intervalIntegral.integral_comp_neg intervalIntegral.integral_symm neg_zero integral_log_from_zero_of_pos Left.neg_pos_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.one_mul intervalIntegral.integral_same Real.log_zero MulZeroClass.mul_zero sub_self
integral_log_from_zero_of_pos 📖	mathematical	Real Real.instLT Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.instMul	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul intervalIntegral.integral_eq_sub_of_hasDerivAt_of_tendsto Real.instCompleteSpace intervalIntegral.intervalIntegrable_log' HasDerivAt.congr_simp add_sub_cancel_right HasDerivAt.sub Real.hasDerivAt_mul_log LT.lt.ne hasDerivAt_id Real.rpow_one mul_comm sub_self Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike tendsto_nhdsWithin_of_tendsto_nhds Filter.tendsto_id ContinuousAt.tendsto ContinuousAt.comp' ContinuousAt.sub ContinuousAt.fst continuousAt_id' ContinuousAt.snd Continuous.continuousAt Continuous.prodMk Real.continuous_mul_log continuous_id' Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add add_zero
integral_mul_cpow_one_add_sq 📖	mathematical	—	intervalIntegral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.instMul Complex.ofReal Complex.instPow Complex.instAdd Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring MeasureTheory.MeasureSpace.volume Real.measureSpace Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Mathlib.Tactic.Contrapose.contrapose₄ add_eq_zero_iff_eq_neg intervalIntegral.integral_eq_sub_of_hasDerivAt Complex.instCompleteSpace Nat.instAtLeastTwoHAddOfNat IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul pow_one HasDerivAt.const_add hasDerivAt_pow add_sub_cancel_right mul_one Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false Complex.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial HasDerivAt.div_const HasDerivAt.cpow_const hasDerivAt_id Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz HasDerivAt.comp_ofReal HasDerivAt.comp Nat.cast_one add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.mul IsTopologicalSemiring.toContinuousMul Complex.continuous_ofReal Continuous.cpow Continuous.fun_add IsTopologicalSemiring.toContinuousAdd continuous_const Continuous.comp' Continuous.pow continuous_id' Complex.ofReal_mem_slitPlane one_pos
integral_mul_rpow_one_add_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Real.instPow Real.instAdd Real.instOne Monoid.toNatPow Real.instMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.cast_one Complex.ofReal_cpow add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_le_one Real.instZeroLEOneClass sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing Complex.ofReal_add Complex.ofReal_pow Complex.ofReal_one Nat.instAtLeastTwoHAddOfNat intervalIntegral.integral_ofReal Complex.ofReal_mul Complex.ofReal_sub Complex.ofReal_div integral_mul_cpow_one_add_sq Complex.ofReal_neg
integral_one 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instOne MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub	—	intervalIntegral.integral_const Real.instCompleteSpace mul_one
integral_one_div 📖	mathematical	Real Set Set.instMembership Set.uIcc Real.lattice Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne MeasureTheory.MeasureSpace.volume Real.measureSpace Real.log	—	one_div integral_inv
integral_one_div_of_neg 📖	mathematical	Real Real.instLT Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne MeasureTheory.MeasureSpace.volume Real.measureSpace Real.log	—	one_div integral_inv_of_neg
integral_one_div_of_pos 📖	mathematical	Real Real.instLT Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne MeasureTheory.MeasureSpace.volume Real.measureSpace Real.log	—	one_div integral_inv_of_pos
integral_one_div_one_add_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instAdd Monoid.toNatPow Real.instMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.arctan	—	intervalIntegral.integral_deriv_eq_sub' Real.instCompleteSpace Real.deriv_arctan Real.differentiableAt_arctan Continuous.continuousOn Continuous.div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_const Continuous.fun_add IsTopologicalSemiring.toContinuousAdd Continuous.pow continuous_id' Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono sub_eq_zero_of_eq
integral_pow 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instAdd Real.instNatCast Real.instOne	—	zpow_natCast integral_zpow Nat.cast_nonneg IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing
integral_pow_abs_sub_uIoc 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.uIoc Real.linearOrder Monoid.toNatPow Real.instMonoid abs Real.lattice Real.instAddGroup Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd Real.instNatCast Real.instOne	—	le_or_gt Set.uIoc_of_le intervalIntegral.integral_of_le intervalIntegral.integral_comp_sub_right sub_self intervalIntegral.integral_congr abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.uIcc_of_le sub_nonneg covariant_swap_add_of_covariant_add integral_pow zero_pow sub_zero Set.uIoc_of_ge LT.lt.le abs_of_nonpos sub_nonpos intervalIntegral.integral_comp_neg neg_zero neg_sub abs_of_neg sub_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd
integral_rpow 📖	mathematical	Real Real.instLT Real.instNeg Real.instOne Set Set.instMembership Set.uIcc Real.lattice Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instPow MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instAdd	—	Complex.ofReal_re Complex.ofReal_one Complex.ofReal_neg integral_cpow intervalIntegral.intervalIntegral_eq_integral_uIoc Complex.re_ofReal_mul integral_re intervalIntegrable_iff PseudoEMetricSpace.pseudoMetrizableSpace intervalIntegral.intervalIntegrable_cpow' intervalIntegral.intervalIntegrable_cpow Real.locallyFinite_volume Complex.ofReal_add div_eq_inv_mul
integral_sin 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.sin MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.cos	—	intervalIntegral.integral_deriv_eq_sub' Real.instCompleteSpace deriv.fun_neg' Real.deriv_cos' neg_neg Real.continuousOn_sin Mathlib.Tactic.Ring.of_eq 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.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero
integral_sin_mul_cos_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Real.sin Monoid.toNatPow Real.instMonoid Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	integral_sin_pow_odd_mul_cos_pow Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat pow_one pow_zero mul_one integral_pow Mathlib.Meta.NormNum.isNat_natCast Nat.cast_one
integral_sin_mul_cos₁ 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Real.sin Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat pow_one MulZeroClass.mul_zero zero_add pow_zero mul_one integral_id integral_sin_pow_mul_cos_pow_odd
integral_sin_mul_cos₂ 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Real.sin Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat integral_sin_mul_cos₁ RCLike.charZero_rclike MulZeroClass.mul_zero zero_add pow_one pow_zero mul_one integral_id integral_sin_pow_odd_mul_cos_pow
integral_sin_pow 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.sin MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instMul Real.cos Real.instNatCast instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.instOne	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_nonneg' Real.instZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw eq_sub_iff_add_eq integral_sin_pow_aux
integral_sin_pow_antitone 📖	mathematical	—	Antitone Real Nat.instPreorder Real.instPreorder intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.sin Real.instZero Real.pi MeasureTheory.MeasureSpace.volume Real.measureSpace	—	antitone_nat_of_succ_le integral_sin_pow_succ_le
integral_sin_pow_aux 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.sin MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.instAdd Real.instMul Real.cos Real.instNatCast Real.instOne	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.congr_simp mul_right_comm HasDerivAt.pow Real.hasDerivAt_sin neg_neg HasDerivAt.neg Real.hasDerivAt_cos intervalIntegral.integral_mul_deriv_eq_deriv_mul Real.instCompleteSpace Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.comp' continuous_mul IsTopologicalSemiring.toContinuousMul Continuous.prodMk Continuous.fun_mul continuous_const continuous_id' Real.continuous_cos Continuous.pow Real.continuous_sin pow_succ mul_neg sub_neg_eq_add Nat.cast_add Nat.cast_one intervalIntegral.integral_neg intervalIntegral.integral_const_mul sq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero 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.sub_congr Mathlib.Tactic.Ring.sub_pf Real.cos_sq' sub_mul one_mul add_comm intervalIntegral.integral_sub mul_sub add_sub_assoc
integral_sin_pow_even 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.sin Real.instZero Real.pi MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instMul Finset.prod Real.instCommMonoid Finset.range DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instOne	—	Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero pow_zero intervalIntegral.integral_const Real.instCompleteSpace sub_zero mul_one Finset.prod_div_distrib div_self NeZero.charZero_one RCLike.charZero_rclike Finset.prod_range_succ_comm mul_left_comm integral_sin_pow Nat.cast_zero Nat.cast_one Nat.cast_add Nat.cast_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat zero_le Nat.instCanonicallyOrderedAdd one_ne_zero NeZero.one GroupWithZero.toNontrivial Real.sin_zero zero_pow IsStrictOrderedRing.noZeroDivisors StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.instCharZero Real.cos_zero Real.sin_pi Real.cos_pi mul_neg neg_zero sub_self zero_add
integral_sin_pow_even_mul_cos_pow_even 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Monoid.toNatPow Real.instMonoid Real.sin Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instAdd	—	Nat.instAtLeastTwoHAddOfNat pow_mul Real.sin_sq Real.cos_sq one_div Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.subst_add one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Nat.cast_one
integral_sin_pow_mul_cos_pow_odd 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Monoid.toNatPow Real.instMonoid Real.sin Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.instOne	—	Continuous.comp' continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.prodMk Continuous.pow continuous_id' Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_const pow_succ pow_mul pow_zero one_mul mul_assoc sq Real.cos_sq' intervalIntegral.integral_comp_mul_deriv Real.hasDerivAt_sin Real.continuousOn_cos
integral_sin_pow_odd 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.sin Real.instZero Real.pi MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Finset.prod Real.instCommMonoid Finset.range DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat pow_one integral_sin Real.cos_zero Real.cos_pi sub_neg_eq_add Nat.cast_one Finset.prod_div_distrib div_self Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Nat.cast_zero mul_one Finset.prod_range_succ_comm mul_left_comm integral_sin_pow Nat.cast_add Nat.cast_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one add_pos' Nat.instIsOrderedAddMonoid Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Nat.instNontrivial zero_le Nat.instCanonicallyOrderedAdd one_ne_zero NeZero.one GroupWithZero.toNontrivial Real.sin_zero zero_pow IsStrictOrderedRing.noZeroDivisors StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.instCharZero Real.sin_pi mul_neg neg_zero sub_self zero_add
integral_sin_pow_odd_mul_cos_pow 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Monoid.toNatPow Real.instMonoid Real.sin Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.instOne	—	Continuous.comp' continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.prodMk Continuous.pow continuous_id' Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_const intervalIntegral.integral_symm pow_succ pow_mul pow_zero one_mul mul_neg neg_mul intervalIntegral.integral_neg sq Real.sin_sq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one intervalIntegral.integral_comp_mul_deriv Real.hasDerivAt_cos ContinuousOn.neg IsTopologicalRing.toContinuousNeg Real.continuousOn_sin
integral_sin_pow_pos 📖	mathematical	—	Real Real.instLT Real.instZero intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.sin Real.pi MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Nat.even_or_odd' Nat.instAtLeastTwoHAddOfNat integral_sin_pow_even mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Finset.prod_pos Real.instZeroLEOneClass Real.instNontrivial div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Nat.cast_zero Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid RCLike.charZero_rclike integral_sin_pow_odd Real.instIsOrderedRing
integral_sin_pow_succ_le 📖	mathematical	—	Real Real.instLE intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.sin Real.instZero Real.pi MeasureTheory.MeasureSpace.volume Real.measureSpace	—	pow_le_pow_of_le_one IsOrderedRing.toPosMulMono Real.instIsOrderedRing Real.sin_nonneg_of_mem_Icc Real.sin_le_one intervalIntegral.integral_mono_on LT.lt.le Real.pi_pos Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.continuous_sin
integral_sin_pow_three 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.sin MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	integral_sin_pow_odd_mul_cos_pow Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat pow_zero mul_one pow_one one_mul intervalIntegral.integral_sub Real.locallyFinite_volume Nat.cast_one enorm_one NormedDivisionRing.to_normOneClass intervalIntegral.integral_const Real.instCompleteSpace integral_pow Mathlib.Meta.NormNum.isNat_natCast
integral_sin_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.sin MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instAdd Real.instMul Real.cos instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat integral_sin_pow zero_add pow_one CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike one_div pow_zero intervalIntegral.integral_const Real.instCompleteSpace mul_one add_sub_assoc Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
integral_sin_sq_mul_cos 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Monoid.toNatPow Real.instMonoid Real.sin Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	integral_sin_pow_mul_cos_pow_odd Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat pow_one pow_zero mul_one integral_pow Mathlib.Meta.NormNum.isNat_natCast Nat.cast_one
integral_sin_sq_mul_cos_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Monoid.toNatPow Real.instMonoid Real.sin Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat 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.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Continuous.comp' Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_id' Real.continuous_cos Continuous.fun_mul continuous_const Real.sin_two_mul Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul pow_one intervalIntegral.integral_div intervalIntegral.integral_sub Real.locallyFinite_volume enorm_one NormedDivisionRing.to_normOneClass Continuous.intervalIntegrable intervalIntegral.integral_const Real.instCompleteSpace mul_one intervalIntegral.integral_comp_mul_left integral_cos_sq Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf integral_sin_pow_even_mul_cos_pow_even
integral_sqrt_one_sub_sq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.sqrt Real.instSub Real.instOne Monoid.toNatPow Real.instMonoid Real.instNeg MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Real.sin_neg Real.sin_pi_div_two intervalIntegral.integral_comp_mul_deriv Real.hasDerivAt_sin Real.continuousOn_cos Continuous.sqrt Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_const Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_id' intervalIntegral.integral_congr_ae MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass Real.cos_eq_sqrt_one_sub_sin_sq le_of_lt Set.mem_Ioc Set.uIoc_of_le neg_le_self IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.pi_pos pow_two integral_cos_sq Real.cos_pi_div_two mul_one Real.cos_neg mul_neg neg_zero sub_self zero_add sub_neg_eq_add add_halves CharZero.NeZero.two RCLike.charZero_rclike
integral_zpow 📖	mathematical	Real Set Set.instMembership Set.uIcc Real.lattice Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toZPow Real.instDivInvMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace DivInvMonoid.toDiv Real.instSub Real.instAdd Real.instIntCast Real.instOne	—	Nat.cast_zero Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.rpow_intCast Int.cast_one integral_rpow

intervalIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_mul_integral_comp_add_div 📖	mathematical	—	Real Real.instMul Real.instInv intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace	—	inv_smul_integral_comp_add_div
inv_mul_integral_comp_div 📖	mathematical	—	Real Real.instMul Real.instInv intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace	—	inv_smul_integral_comp_div
inv_mul_integral_comp_div_add 📖	mathematical	—	Real Real.instMul Real.instInv intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace	—	inv_smul_integral_comp_div_add
inv_mul_integral_comp_div_sub 📖	mathematical	—	Real Real.instMul Real.instInv intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace	—	inv_smul_integral_comp_div_sub
inv_mul_integral_comp_sub_div 📖	mathematical	—	Real Real.instMul Real.instInv intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace	—	inv_smul_integral_comp_sub_div
mul_integral_comp_add_mul 📖	mathematical	—	Real Real.instMul intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instAdd MeasureTheory.MeasureSpace.volume Real.measureSpace	—	smul_integral_comp_add_mul
mul_integral_comp_mul_add 📖	mathematical	—	Real Real.instMul intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instAdd MeasureTheory.MeasureSpace.volume Real.measureSpace	—	smul_integral_comp_mul_add
mul_integral_comp_mul_left 📖	mathematical	—	Real Real.instMul intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace	—	smul_integral_comp_mul_left
mul_integral_comp_mul_right 📖	mathematical	—	Real Real.instMul intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.volume Real.measureSpace	—	smul_integral_comp_mul_right
mul_integral_comp_mul_sub 📖	mathematical	—	Real Real.instMul intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instSub MeasureTheory.MeasureSpace.volume Real.measureSpace	—	smul_integral_comp_mul_sub
mul_integral_comp_sub_mul 📖	mathematical	—	Real Real.instMul intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instSub MeasureTheory.MeasureSpace.volume Real.measureSpace	—	smul_integral_comp_sub_mul

---

← Back to Index