Orthogonality

📁 Source: Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean

Statistics

Metric	Count
Definitions measureT	1
Theorems integrable_measureT, integral_T_real_mul_self_measureT_of_ne_zero, integral_eval_T_real_measureT_of_ne_zero, integral_eval_T_real_measureT_zero, integral_eval_T_real_mul_eval_T_real_measureT, integral_eval_T_real_mul_eval_T_real_measureT_of_ne, integral_eval_T_real_mul_self_measureT_zero, integral_measureT, integral_measureT_eq_integral_cos, integral_measureT_eq_integral_cos_of_continuous, intervalIntegrable_sqrt_one_sub_sq_inv	11
Total	12

Polynomial.Chebyshev

Definitions

Name	Category	Theorems
measureT 📖	CompOp	10 math math: integral_measureT_eq_integral_cos, integral_T_real_mul_self_measureT_of_ne_zero, integral_measureT, integral_measureT_eq_integral_cos_of_continuous, integrable_measureT, integral_eval_T_real_measureT_zero, integral_eval_T_real_mul_eval_T_real_measureT, integral_eval_T_real_measureT_of_ne_zero, integral_eval_T_real_mul_eval_T_real_measureT_of_ne, integral_eval_T_real_mul_self_measureT_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_measureT 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder Real.instNeg Real.instOne	MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.measurableSpace measureT	—	Set.uIcc_of_lt Mathlib.Meta.NormNum.isInt_lt_true Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one IntervalIntegrable.continuousOn_mul intervalIntegrable_sqrt_one_sub_sq_inv MeasureTheory.restrict_withDensity BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.integrable_withDensity_iff Real.sqrt_inv Measurable.inv ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Measurable.sqrt Measurable.const_sub ContinuousSub.measurableSub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Measurable.pow_const Monoid.measurablePow ContinuousMul.measurableMul₂ instSecondCountableTopologyReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal measurable_id' MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_eq Set.uIoc_of_le Mathlib.Meta.NormNum.isInt_le_true intervalIntegrable_iff PseudoEMetricSpace.pseudoMetrizableSpace
integral_T_real_mul_self_measureT_of_ne_zero 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace measureT Real.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat integral_eval_T_real_mul_eval_T_real_measureT integral_eval_T_real_measureT_of_ne_zero sub_self integral_eval_T_real_measureT_zero zero_add
integral_eval_T_real_measureT_of_ne_zero 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace measureT Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.instZero	—	Int.cast_ne_zero RCLike.charZero_rclike intervalIntegral.integral_congr Real.deriv_sin intervalIntegral.integral_deriv_of_contDiffOn_Icc Real.instCompleteSpace ContDiff.contDiffOn Real.contDiff_sin le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Int.cast_pos IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Real.instIsOrderedRing IsOrderedRing.toZeroLEOneClass NeZero.one Real.instNontrivial lt_of_le_of_ne' Real.pi_pos Real.sin_int_mul_pi Real.sin_zero sub_self intervalIntegral.integral_symm mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono Int.cast_nonpos Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one Real.pi_nonneg neg_zero integral_measureT_eq_integral_cos_of_continuous Polynomial.continuousOn IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal T_real_cos intervalIntegral.integral_comp_mul_left smul_eq_zero_iff_right instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero MulZeroClass.mul_zero
integral_eval_T_real_measureT_zero 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace measureT Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.pi	—	integral_measureT_eq_integral_cos_of_continuous Polynomial.continuousOn IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal T_zero Polynomial.eval_one intervalIntegral.integral_const Real.instCompleteSpace sub_zero mul_one
integral_eval_T_real_mul_eval_T_real_measureT 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace measureT Real.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat T_mul_T Polynomial.eval_add MeasureTheory.integral_add integrable_measureT Polynomial.continuousOn IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.integral_const_mul mul_assoc Polynomial.eval_ofNat Polynomial.eval_mul
integral_eval_T_real_mul_eval_T_real_measureT_of_ne 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace measureT Real.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.instZero	—	Nat.instAtLeastTwoHAddOfNat integral_eval_T_real_mul_eval_T_real_measureT integral_eval_T_real_measureT_of_ne_zero add_zero zero_div
integral_eval_T_real_mul_self_measureT_zero 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace measureT Real.instMul Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing T Real.pi	—	T_zero mul_one integral_eval_T_real_measureT_zero
integral_measureT 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace measureT intervalIntegral Real.instMul Real.sqrt Real.instInv Real.instSub Real.instOne Monoid.toNatPow Real.instMonoid Real.instNeg MeasureTheory.MeasureSpace.volume Real.measureSpace	—	intervalIntegral.integral_of_le Mathlib.Meta.NormNum.isInt_le_true Real.instIsOrderedRing Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one MeasureTheory.restrict_withDensity BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid integral_withDensity_eq_integral_smul Real.sqrt_inv Measurable.inv ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Measurable.sqrt Measurable.const_sub ContinuousSub.measurableSub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Measurable.pow_const Monoid.measurablePow ContinuousMul.measurableMul₂ instSecondCountableTopologyReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal measurable_id' mul_comm
integral_measureT_eq_integral_cos 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.cos Set.Ioo Real.instPreorder Real.instZero Real.pi MeasureTheory.IntegrableOn MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Set.Icc MeasureTheory.MeasureSpace.volume Real.instMul Real.sqrt Real.instInv Real.instSub Real.instOne Monoid.toNatPow Real.instMonoid Real.instNeg	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace measureT intervalIntegral	—	integral_measureT intervalIntegral.integral_symm intervalIntegral.integral_neg Real.sqrt_inv mul_neg intervalIntegral.integral_comp_mul_deriv''' Continuous.continuousOn Real.continuous_arccos HasDerivAt.hasDerivWithinAt Real.hasDerivAt_arccos inf_of_le_right Real.instIsOrderedAddMonoid Real.instZeroLEOneClass sup_of_le_left ContinuousOn.mono Real.arccos_one Real.arccos_neg_one StrictAntiOn.image_Ioo_subset Real.strictAntiOn_arccos Set.uIcc_of_ge Real.arccos_image_Icc MeasureTheory.IntegrableOn.congr_fun MeasureTheory.Integrable.neg Real.cos_arccos one_div BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal intervalIntegral.integral_congr
integral_measureT_eq_integral_cos_of_continuous 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc Real.instPreorder Real.instNeg Real.instOne	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace measureT intervalIntegral Real.cos Real.instZero Real.pi MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Continuous.continuousOn ContinuousOn.comp_continuous Real.continuous_cos Real.instIsOrderedAddMonoid Real.abs_cos_le_one integral_measureT_eq_integral_cos ContinuousOn.mono Set.Ioo_subset_Icc_self ContinuousOn.integrableOn_Icc BorelSpace.opensMeasurable Real.borelSpace MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Real.sqrt_inv Set.uIcc_of_le Real.instZeroLEOneClass intervalIntegrable_iff' PseudoEMetricSpace.pseudoMetrizableSpace Real.noAtoms_volume enorm_ne_top IntervalIntegrable.continuousOn_mul intervalIntegrable_sqrt_one_sub_sq_inv
intervalIntegrable_sqrt_one_sub_sq_inv 📖	mathematical	—	IntervalIntegrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup Real.sqrt Real.instInv Real.instSub Real.instOne Monoid.toNatPow Real.instMonoid MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instNeg	—	intervalIntegrable_iff PseudoEMetricSpace.pseudoMetrizableSpace intervalIntegral.integrableOn_deriv_of_nonneg Continuous.continuousOn Continuous.neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal Real.continuous_arccos IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring HasDerivAt.congr_simp Real.sqrt_inv IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul one_div neg_neg HasDerivAt.neg Real.hasDerivAt_arccos inf_of_le_left Real.instIsOrderedAddMonoid Real.instZeroLEOneClass sup_of_le_right PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing

---

← Back to Index