Documentation Verification Report

TrapezoidalRule

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

Statistics

Metric	Count
Definitions `trapezoidal_error`, `trapezoidal_integral`	2
Theorems `sum_trapezoidal_error_adjacent_intervals`, `sum_trapezoidal_integral_adjacent_intervals`, `trapezoidal_error_eq`, `trapezoidal_error_le`, `trapezoidal_error_le_of_c2`, `trapezoidal_error_symm`, `trapezoidal_integral_eq`, `trapezoidal_integral_ext`, `trapezoidal_integral_one`, `trapezoidal_integral_symm`	10
Total	12

(root)

Definitions

Name	Category	Theorems
`trapezoidal_error` 📖	CompOp	5 math math: `trapezoidal_error_eq`, `trapezoidal_error_le_of_c2`, `sum_trapezoidal_error_adjacent_intervals`, `trapezoidal_error_symm`, `trapezoidal_error_le`
`trapezoidal_integral` 📖	CompOp	5 math math: `trapezoidal_integral_ext`, `trapezoidal_integral_one`, `trapezoidal_integral_symm`, `trapezoidal_integral_eq`, `sum_trapezoidal_integral_adjacent_intervals`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_trapezoidal_error_adjacent_intervals` 📖	mathematical	`IntervalIntegrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `Real.instAdd` `Real.instMul` `Real.instNatCast`	`Finset.sum` `Real.instAddCommMonoid` `Finset.range` `trapezoidal_error` `Real.instOne`	—	`Finset.sum_sub_distrib` `sum_trapezoidal_integral_adjacent_intervals` `Finset.sum_congr` `Nat.cast_one` `intervalIntegral.sum_integral_adjacent_intervals` `le_total` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `mul_le_mul_of_nonpos_right` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `Nat.cast_le` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `mul_nonpos_of_nonneg_of_nonpos` `IsOrderedRing.toPosMulMono` `Nat.cast_nonneg` `Set.mem_uIcc_of_le` `le_add_of_nonneg_right` `mul_nonneg` `Nat.cast_nonneg'` `le_imp_le_of_le_of_le` `add_le_add_right` `mul_le_mul_of_nonneg_right` `le_refl` `IntervalIntegrable.mono` `PseudoEMetricSpace.pseudoMetrizableSpace` `Set.uIcc_subset_uIcc` `LT.lt.le` `le_rfl` `CharP.cast_eq_zero` `CharP.ofCharZero` `MulZeroClass.zero_mul` `add_zero`
`sum_trapezoidal_integral_adjacent_intervals` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.range` `trapezoidal_integral` `Real.instAdd` `Real.instMul` `Real.instNatCast` `Real.instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_congr` `trapezoidal_integral_one` `add_sub_add_left_eq_sub` `add_sub_cancel_left` `one_mul` `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.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `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` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `Finset.sum_add_distrib` `Finset.sum_range_succ'` `Finset.sum_range_succ` `add_add_add_comm` `add_comm` `Nat.cast_sub` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `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_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `add_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `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.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.RingNF.add_assoc_rev` `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` `Mathlib.Tactic.RingNF.nnrat_rawCast` `Mathlib.Tactic.RingNF.mul_assoc_rev`
`trapezoidal_error_eq` 📖	mathematical	—	`trapezoidal_error` `Real` `Real.instZero`	—	`trapezoidal_integral_eq` `intervalIntegral.integral_same` `sub_self`
`trapezoidal_error_le` 📖	mathematical	`DifferentiableOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.uIcc` `Real.lattice` `derivWithin` `IntervalIntegrable` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Real.normedAddCommGroup` `iteratedDerivWithin` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `Real.instLE` `abs` `Real.instAddGroup`	`trapezoidal_error` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `lt_trichotomy` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Set.uIcc_of_lt` `trapezoidal_error_eq` `abs_zero` `sub_self` `zero_pow` `Nat.instCharZero` `MulZeroClass.zero_mul` `zero_div` `abs_of_neg` `sub_neg` `neg_sub` `trapezoidal_error_symm` `abs_neg` `Set.uIcc_of_gt` `IntervalIntegrable.symm`
`trapezoidal_error_le_of_c2` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `Set.uIcc` `Real.lattice` `Real.instLE` `abs` `Real.instAddGroup` `iteratedDerivWithin`	`trapezoidal_error` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub` `Real.instNatCast`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_or_ne` `trapezoidal_error_eq` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_self` `zero_pow` `Nat.instCharZero` `MulZeroClass.zero_mul` `zero_div` `uniqueDiffOn_Icc` `inf_lt_sup` `ContDiffOn.differentiableOn` `two_ne_zero` `CharZero.NeZero.two` `WithTop.charZero` `iteratedDerivWithin_one` `ContDiffOn.differentiableOn_iteratedDerivWithin` `WithTop.addLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `WithTop.zeroLEOneClass` `IsOrderedRing.toZeroLEOneClass` `ContinuousOn.intervalIntegrable` `Real.locallyFinite_volume` `ContDiffOn.continuousOn_iteratedDerivWithin` `le_refl` `trapezoidal_error_le`
`trapezoidal_error_symm` 📖	mathematical	—	`trapezoidal_error` `Real` `Real.instNeg`	—	`trapezoidal_integral_symm` `intervalIntegral.integral_symm` `neg_sub_neg` `neg_sub`
`trapezoidal_integral_eq` 📖	mathematical	—	`trapezoidal_integral` `Real` `Real.instZero`	—	`sub_self` `zero_div` `add_self_div_two` `CharZero.NeZero.two` `RCLike.charZero_rclike` `Finset.sum_congr` `MulZeroClass.mul_zero` `add_zero` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `MulZeroClass.zero_mul`
`trapezoidal_integral_ext` 📖	mathematical	—	`Real` `Real.instAdd` `trapezoidal_integral` `Real.instMul` `Real.instNatCast` `Real.instOne`	—	`Nat.cast_add_one` `sum_trapezoidal_integral_adjacent_intervals` `Finset.sum_range_succ`
`trapezoidal_integral_one` 📖	mathematical	—	`trapezoidal_integral` `Real` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `Nat.cast_one` `div_one` `Finset.sum_congr` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `add_zero` `mul_comm_div`
`trapezoidal_integral_symm` 📖	mathematical	—	`trapezoidal_integral` `Real` `Real.instNeg`	—	`neg_mul_eq_neg_mul` `neg_div'` `neg_sub` `add_comm` `Finset.sum_range_reflect` `Finset.sum_congr` `Nat.cast_one` `tsub_tsub` `Nat.instOrderedSub` `Nat.cast_add` `Nat.cast_sub` `Finset.mem_range` `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.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `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.mul_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `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.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_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_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_natSucc` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.sub_pf` `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_gt` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_overlap_pf_zero`

---

← Back to Index