Documentation Verification Report

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	11 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`, `integral_eq_sumZeroes`, `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` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `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` `Measurable.coe_nnreal_ennreal` `Measurable.sqrt` `Measurable.inv` `ContinuousInv₀.measurableInv` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `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` `Real.sqrt_inv` `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` `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` `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.toPow` `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` `Measurable.sqrt` `Measurable.inv` `ContinuousInv₀.measurableInv` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `Measurable.const_sub` `ContinuousSub.measurableSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `Measurable.pow_const` `Monoid.measurablePow` `ContinuousMul.measurableMul₂` `instSecondCountableTopologyReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `measurable_id'` `Real.sqrt_inv` `mul_comm`
`integral_measureT_eq_integral_cos` 📖	mathematical	—	`MeasureTheory.integral` `Real` `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`	—	`integral_measureT` `intervalIntegral.integral_symm` `intervalIntegral.integral_neg` `Real.sqrt_inv` `mul_neg` `intervalIntegral.integral_comp_mul_deriv_of_deriv_nonpos` `Continuous.continuousOn` `Real.continuous_arccos` `Real.hasDerivAt_arccos` `inf_of_le_right` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `sup_of_le_left` `one_div` `IsOrderedAddMonoid.toAddLeftMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `intervalIntegral.integral_congr` `Real.cos_arccos` `Set.uIcc_of_ge` `Real.arccos_one` `Real.arccos_neg_one`
`integral_measureT_eq_integral_cos_of_continuous` 📖	mathematical	—	`MeasureTheory.integral` `Real` `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`	—	`integral_measureT_eq_integral_cos`
`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.toPow` `Real.instMonoid` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `Real.instNeg`	—	`intervalIntegrable_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `intervalIntegral.integrableOn_deriv_of_nonneg` `Continuous.continuousOn` `Continuous.neg` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing` `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