Documentation Verification Report

Approximations

📁 Source: Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

Statistics

Metric	Count
Definitions `of`, `of`	2
Theorems `nth_stream_fr_lt_one`, `nth_stream_fr_nonneg`, `nth_stream_fr_nonneg_lt_one`, `one_le_succ_nth_stream_b`, `succ_nth_stream_b_le_nth_stream_fr_inv`, `abs_sub_convergents_le'`, `abs_sub_convs_le`, `exists_int_eq_of_partDen`, `fib_le_of_contsAux_b`, `le_of_succ_get?_den`, `le_of_succ_succ_get?_contsAux_b`, `of_den_mono`, `of_isSimpContFract`, `of_one_le_get?_partDen`, `of_partNum_eq_one`, `of_partNum_eq_one_and_exists_int_partDen_eq`, `sub_convs_eq`, `succ_nth_fib_le_of_nth_den`, `zero_le_of_contsAux_b`, `zero_le_of_den`, `of_isContFract`	21
Total	23

ContFract

Definitions

Name	Category	Theorems
`of` 📖	CompOp	—

GenContFract

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_sub_convergents_le'` 📖	mathematical	`Stream'.Seq.get?` `partDens` `of` `Field.toDivisionRing`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `convs` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `dens`	—	`LE.le.trans` `abs_sub_convs_le` `LE.le.eq_or_lt'` `zero_le_of_den` `MulZeroClass.zero_mul` `div_zero` `MulZeroClass.mul_zero` `one_div_le_one_div_of_le` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `LT.lt.trans_le` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `of_one_le_get?_partDen` `mul_pos` `mul_comm` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `le_of_succ_get?_den` `le_of_lt`
`abs_sub_convs_le` 📖	mathematical	`TerminatedAt` `of` `Field.toDivisionRing`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `convs` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `dens`	—	`of_partNum_eq_one` `partNum_eq_s_a` `contsAux_recurrence` `one_mul` `add_comm` `IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some` `IntFractPair.succ_nth_stream_eq_some_iff` `fib_le_of_contsAux_b` `terminated_stable` `LE.le.trans_lt'` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Nat.fib_pos` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IntFractPair.succ_nth_stream_b_le_nth_stream_fr_inv` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `le_of_lt` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `add_le_add_right` `div_le_div_of_nonneg_left` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `zero_le_one` `le_trans` `inv_pos` `lt_of_le_of_ne` `IntFractPair.nth_stream_fr_nonneg` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `abs_of_pos` `abs_div` `abs_neg_one_pow`
`exists_int_eq_of_partDen` 📖	mathematical	`Stream'.Seq.get?` `partDens` `of` `Field.toDivisionRing`	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`exists_s_b_of_partDen` `of_partNum_eq_one_and_exists_int_partDen_eq`
`fib_le_of_contsAux_b` 📖	mathematical	`TerminatedAt` `of` `Field.toDivisionRing`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Nat.fib` `Pair.b` `contsAux`	—	`Nat.strong_induction_on` `Nat.cast_zero` `zero_add` `Nat.cast_one` `of_h_eq_floor` `terminated_stable` `lt_trans` `of_one_le_get?_partDen` `partDen_eq_s_b` `mul_le_mul` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toMulPosMono` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toZeroLEOneClass` `le_of_lt` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `one_mul` `add_le_add` `covariant_swap_add_of_covariant_add` `of_partNum_eq_one` `partNum_eq_s_a` `Nat.fib_add_two` `Nat.cast_add` `contsAux_recurrence` `add_comm`
`le_of_succ_get?_den` 📖	mathematical	`Stream'.Seq.get?` `partDens` `of` `Field.toDivisionRing`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `dens`	—	`den_eq_conts_b` `nth_cont_eq_succ_nth_contAux` `le_of_succ_succ_get?_contsAux_b`
`le_of_succ_succ_get?_contsAux_b` 📖	mathematical	`Stream'.Seq.get?` `partDens` `of` `Field.toDivisionRing`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Pair.b` `contsAux`	—	`exists_s_b_of_partDen` `contsAux_recurrence` `of_partNum_eq_one` `partNum_eq_s_a` `one_mul` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`of_den_mono` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `dens` `Field.toDivisionRing` `of`	—	`Stream'.Seq.TerminatedAt.eq_1` `terminatedAt_iff_partDen_none` `dens_stable_of_terminated` `le_refl` `of_one_le_get?_partDen` `one_mul` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `zero_le_of_den` `le_of_succ_get?_den`
`of_isSimpContFract` 📖	mathematical	—	`IsSimpContFract` `of` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`of_partNum_eq_one`
`of_one_le_get?_partDen` 📖	mathematical	`Stream'.Seq.get?` `partDens` `of` `Field.toDivisionRing`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`exists_s_b_of_partDen` `IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some` `Nat.cast_one` `Int.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `IntFractPair.one_le_succ_nth_stream_b`
`of_partNum_eq_one` 📖	mathematical	`Stream'.Seq.get?` `partNums` `of` `Field.toDivisionRing`	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`exists_s_a_of_partNum` `of_partNum_eq_one_and_exists_int_partDen_eq`
`of_partNum_eq_one_and_exists_int_partDen_eq` 📖	mathematical	`Stream'.Seq.get?` `Pair` `s` `of` `Field.toDivisionRing`	`Pair.a` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Pair.b` `AddGroupWithOne.toIntCast`	—	`IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some` `get?_of_eq_some_of_succ_get?_intFractPair_stream` `IsStrictOrderedRing.toCharZero`
`sub_convs_eq` 📖	mathematical	`IntFractPair.stream` `Field.toDivisionRing` `IntFractPair`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `convs` `of` `IntFractPair.fr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `LinearOrder.toDecidableEq` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Pair.b` `contsAux` `Distrib.toAdd` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`compExactValue_correctness_of_stream_eq_some` `eq_or_ne` `sub_eq_zero` `one_mul` `add_comm` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none` `SimpContFract.determinant_aux` `fib_le_of_contsAux_b` `terminated_stable` `zero_add` `Nat.instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Nat.instCharZero` `LE.le.trans_lt'` `Nat.cast_pos` `IsStrictOrderedRing.toIsOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Nat.fib_pos` `LE.le.trans` `Nat.cast_nonneg` `Ne.lt_of_le'` `IntFractPair.nth_stream_fr_nonneg` `ne_of_gt` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedRing.toIsOrderedAddMonoid` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE`
`succ_nth_fib_le_of_nth_den` 📖	mathematical	`TerminatedAt` `of` `Field.toDivisionRing`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Nat.fib` `dens`	—	`den_eq_conts_b` `nth_cont_eq_succ_nth_contAux` `le_refl` `fib_le_of_contsAux_b`
`zero_le_of_contsAux_b` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Pair.b` `contsAux` `Field.toDivisionRing` `of`	—	`le_refl` `zero_add` `of_h_eq_floor` `IsStrictOrderedRing.toZeroLEOneClass` `contsAux_stable_step_of_terminated` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toCharZero` `fib_le_of_contsAux_b`
`zero_le_of_den` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `dens` `Field.toDivisionRing` `of`	—	`den_eq_conts_b` `nth_cont_eq_succ_nth_contAux` `zero_le_of_contsAux_b`

GenContFract.IntFractPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nth_stream_fr_lt_one` 📖	mathematical	`stream` `Field.toDivisionRing` `GenContFract.IntFractPair`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `fr` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`nth_stream_fr_nonneg_lt_one`
`nth_stream_fr_nonneg` 📖	mathematical	`stream` `Field.toDivisionRing` `GenContFract.IntFractPair`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `fr`	—	`nth_stream_fr_nonneg_lt_one`
`nth_stream_fr_nonneg_lt_one` 📖	mathematical	`stream` `Field.toDivisionRing` `GenContFract.IntFractPair`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `fr` `Preorder.toLT` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`of.eq_1` `Int.fract_nonneg` `Int.fract_lt_one` `succ_nth_stream_eq_some_iff`
`one_le_succ_nth_stream_b` 📖	mathematical	`stream` `Field.toDivisionRing` `GenContFract.IntFractPair`	`b`	—	`succ_nth_stream_eq_some_iff` `of.eq_1` `Int.le_floor` `Int.cast_one` `one_le_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `LE.le.lt_of_ne'` `nth_stream_fr_nonneg` `LT.lt.le` `nth_stream_fr_lt_one`
`succ_nth_stream_b_le_nth_stream_fr_inv` 📖	mathematical	`stream` `Field.toDivisionRing` `GenContFract.IntFractPair`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `b` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `fr`	—	`Int.floor_le` `Option.bind_congr'`

SimpContFract

Definitions

Name	Category	Theorems
`of` 📖	CompOp	1 math math: `of_isContFract`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isContFract` 📖	mathematical	—	`IsContFract` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `of`	—	`lt_of_lt_of_le` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `GenContFract.of_one_le_get?_partDen`

---

← Back to Index