Documentation Verification Report

LiouvilleNumber

📁 Source: Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleNumber.lean

Statistics

Metric	Count
Definitions `partialSum`, `remainder`, `liouvilleNumber`	3
Theorems `aux_calc`, `partialSum_add_remainder`, `partialSum_eq_rat`, `partialSum_succ`, `remainder_lt`, `remainder_lt'`, `remainder_pos`, `remainder_summable`, `summable`, `liouville_liouvilleNumber`, `transcendental_liouvilleNumber`	11
Total	14

LiouvilleNumber

Definitions

Name	Category	Theorems
`partialSum` 📖	CompOp	3 math math: `partialSum_eq_rat`, `partialSum_succ`, `partialSum_add_remainder`
`remainder` 📖	CompOp	4 math math: `remainder_pos`, `partialSum_add_remainder`, `remainder_lt`, `remainder_lt'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aux_calc` 📖	mathematical	`Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instMul` `Real.instInv` `Real.instSub` `Real.instOne` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Nat.factorial`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `sub_one_div_inv_le_two` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `le_of_lt` `div_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `lt_of_lt_of_le` `Mathlib.Meta.NormNum.instAtLeastTwo` `mul_one_div` `mul_comm` `pow_mul` `div_le_div_iff₀` `one_mul` `mul_add_one` `Distrib.leftDistribClass` `pow_add` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `LE.le.trans` `le_self_pow₀` `Real.instZeroLEOneClass` `one_le_two` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ne_of_gt` `Nat.factorial_pos`
`partialSum_add_remainder` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Real.instAdd` `partialSum` `remainder` `liouvilleNumber`	—	`Summable.sum_add_tsum_nat_add` `instIsTopologicalAddGroupReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `summable`
`partialSum_eq_rat` 📖	mathematical	—	`partialSum` `Real` `Real.instNatCast` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Nat.instMonoid` `Nat.factorial`	—	`partialSum.eq_1` `Finset.range_one` `Finset.sum_singleton` `Nat.cast_one` `Nat.factorial.eq_1` `pow_one` `partialSum_succ` `div_add_div` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `Real.instIsStrictOrderedRing` `div_eq_div_iff` `mul_pos` `add_mul` `Distrib.rightDistribClass` `one_mul` `Nat.factorial_succ` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instIsOrderedAddMonoid` `pow_add` `mul_assoc` `mul_one`
`partialSum_succ` 📖	mathematical	—	`partialSum` `Real` `Real.instAdd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Monoid.toNatPow` `Real.instMonoid` `Nat.factorial`	—	`Finset.sum_range_succ`
`remainder_lt` 📖	mathematical	`Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Real.instLT` `remainder` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Monoid.toNatPow` `Real.instMonoid` `Nat.factorial`	—	`Nat.instAtLeastTwoHAddOfNat` `LT.lt.trans_le` `remainder_lt'` `one_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `aux_calc`
`remainder_lt'` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`remainder` `Real.instMul` `Real.instInv` `Real.instSub` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Nat.factorial`	—	`LT.lt.trans` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `div_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Summable.tsum_lt_tsum` `Real.instIsOrderedAddMonoid` `instIsTopologicalAddGroupReal` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `one_div_pow_le_one_div_pow_of_le` `LT.lt.le` `Nat.add_factorial_succ_le_factorial_add_succ` `one_div_pow_strictAnti` `Nat.add_factorial_succ_lt_factorial_add_succ` `le_rfl` `remainder_summable` `summable_one_div_pow_of_le` `le_self_add` `Nat.instCanonicallyOrderedAdd` `pow_add` `one_div` `mul_inv` `inv_pow` `tsum_mul_right` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `tsum_geometric_of_lt_one` `le_of_lt` `div_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `lt_trans`
`remainder_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Real.instZero` `remainder`	—	`Summable.tsum_pos` `Real.instIsOrderedAddMonoid` `instIsTopologicalAddGroupReal` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instLeAtTopUnconditional` `SummationFilter.instNeBotUnconditional` `remainder_summable` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `lt_trans`
`remainder_summable` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Nat.factorial` `SummationFilter.unconditional`	—	`summable_nat_add_iff` `instIsTopologicalAddGroupReal` `summable`
`summable` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Nat.factorial` `SummationFilter.unconditional`	—	`summable_one_div_pow_of_le` `Nat.self_le_factorial`

(root)

Definitions

Name	Category	Theorems
`liouvilleNumber` 📖	CompOp	3 math math: `transcendental_liouvilleNumber`, `LiouvilleNumber.partialSum_add_remainder`, `liouville_liouvilleNumber`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`liouville_liouvilleNumber` 📖	mathematical	—	`Liouville` `liouvilleNumber` `Real` `Real.instNatCast`	—	`Nat.cast_one` `Int.instAddLeftMono` `Int.instZeroLEOneClass` `Int.instCharZero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `LiouvilleNumber.partialSum_eq_rat` `LT.lt.trans_le` `Nat.instAtLeastTwoHAddOfNat` `zero_lt_two` `Nat.instZeroLEOneClass` `Nat.instIsOrderedAddMonoid` `one_lt_pow₀` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Nat.factorial_ne_zero` `Int.cast_natCast` `Int.cast_pow` `LiouvilleNumber.partialSum_add_remainder` `Nat.cast_pow` `LiouvilleNumber.remainder_pos` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `LT.lt.ne'` `add_sub_cancel_left` `abs_of_pos` `one_div` `LiouvilleNumber.remainder_lt`
`transcendental_liouvilleNumber` 📖	mathematical	—	`Transcendental` `Real` `Int.instCommRing` `Real.instRing` `Ring.toIntAlgebra` `liouvilleNumber` `Real.instNatCast`	—	`Liouville.transcendental` `liouville_liouvilleNumber`

---

← Back to Index