ArithmeticGeometricMean

📁 Source: Mathlib/Analysis/SpecialFunctions/ArithmeticGeometricMean.lean

Statistics

Metric	Count
Definitions `agm`, `agmSequences`	2
Theorems `agmSequences_comm`, `agmSequences_fst_le_agm`, `agmSequences_fst_le_snd`, `agmSequences_fst_lt_agm_of_pos_of_ne`, `agmSequences_fst_lt_snd_of_ne`, `agmSequences_fst_monotone`, `agmSequences_min_max`, `agmSequences_monotone_and_antitone`, `agmSequences_snd_antitone`, `agmSequences_succ`, `agmSequences_succ'`, `agmSequences_zero`, `agm_comm`, `agm_eq_agm_agmSequences_fst_agmSequences_snd`, `agm_eq_agm_gm_am`, `agm_eq_ciInf`, `agm_eq_ciSup`, `agm_le_agmSequences_snd`, `agm_le_max`, `agm_lt_agmSequences_snd_of_ne`, `agm_lt_max_of_ne`, `agm_mul_distrib`, `agm_pos`, `agm_self`, `agm_zero_left`, `agm_zero_right`, `bddAbove_range_agmSequences_fst`, `dist_agmSequences_fst_snd`, `dist_gm_am_le`, `le_gm_and_am_le`, `min_le_agm`, `min_lt_agm_of_pos_of_ne`, `sqrt_mul_le_half_add`, `sqrt_mul_lt_half_add_of_ne`, `tendsto_agmSequences_fst_agm`, `tendsto_agmSequences_snd_agm`, `tendsto_dist_agmSequences_atTop_zero`	37
Total	39

NNReal

Definitions

Name	Category	Theorems
`agm` 📖	CompOp	20 math math: `tendsto_agmSequences_fst_agm`, `agm_lt_max_of_ne`, `agm_le_agmSequences_snd`, `agmSequences_fst_le_agm`, `tendsto_agmSequences_snd_agm`, `agm_comm`, `agm_mul_distrib`, `agm_eq_ciSup`, `agm_eq_agm_gm_am`, `min_le_agm`, `agm_self`, `agmSequences_fst_lt_agm_of_pos_of_ne`, `agm_eq_agm_agmSequences_fst_agmSequences_snd`, `min_lt_agm_of_pos_of_ne`, `agm_pos`, `agm_zero_left`, `agm_zero_right`, `agm_eq_ciInf`, `agm_lt_agmSequences_snd_of_ne`, `agm_le_max`
`agmSequences` 📖	CompOp	22 math math: `tendsto_agmSequences_fst_agm`, `tendsto_dist_agmSequences_atTop_zero`, `agmSequences_zero`, `agm_le_agmSequences_snd`, `agmSequences_fst_le_agm`, `dist_agmSequences_fst_snd`, `tendsto_agmSequences_snd_agm`, `bddAbove_range_agmSequences_fst`, `agm_eq_ciSup`, `agmSequences_fst_lt_snd_of_ne`, `agmSequences_min_max`, `agmSequences_fst_monotone`, `agmSequences_monotone_and_antitone`, `agmSequences_fst_le_snd`, `agmSequences_fst_lt_agm_of_pos_of_ne`, `agm_eq_agm_agmSequences_fst_agmSequences_snd`, `agmSequences_snd_antitone`, `agmSequences_succ'`, `agm_eq_ciInf`, `agm_lt_agmSequences_snd_of_ne`, `agmSequences_succ`, `agmSequences_comm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`agmSequences_comm` 📖	mathematical	—	`agmSequences`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_comm` `add_comm`
`agmSequences_fst_le_agm` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `agmSequences` `agm`	—	`agm_eq_ciSup` `le_ciSup` `bddAbove_range_agmSequences_fst`
`agmSequences_fst_le_snd` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `agmSequences`	—	`sqrt_mul_le_half_add` `le_total` `LE.le.trans` `agmSequences_fst_monotone` `agmSequences_snd_antitone`
`agmSequences_fst_lt_agm_of_pos_of_ne` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`agmSequences` `agm`	—	`agm_eq_agm_agmSequences_fst_agmSequences_snd` `LT.lt.trans_le` `sqrt_pos_of_pos` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `agmSequences_fst_monotone` `zero_le` `Nat.instCanonicallyOrderedAdd` `agmSequences_fst_lt_snd_of_ne` `mul_self_sqrt` `sqrt_mul` `mul_lt_mul_of_pos_left` `agmSequences_fst_le_agm`
`agmSequences_fst_lt_snd_of_ne` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `agmSequences`	—	`sqrt_mul_lt_half_add_of_ne` `Nat.instAtLeastTwoHAddOfNat` `agmSequences_succ'` `LT.lt.ne` `le_total` `LE.le.trans_lt` `agmSequences_fst_monotone` `LT.lt.trans_le` `agmSequences_snd_antitone`
`agmSequences_fst_monotone` 📖	mathematical	—	`Monotone` `NNReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderNNReal` `agmSequences`	—	`agmSequences_monotone_and_antitone`
`agmSequences_min_max` 📖	mathematical	—	`agmSequences` `NNReal` `instMin` `instMax`	—	`le_total` `min_eq_left` `max_eq_right` `min_eq_right` `max_eq_left` `agmSequences_comm`
`agmSequences_monotone_and_antitone` 📖	mathematical	—	`Monotone` `NNReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderNNReal` `agmSequences` `Antitone`	—	`le_gm_and_am_le` `sqrt_mul_le_half_add` `monotone_nat_of_le_succ` `antitone_nat_of_succ_le`
`agmSequences_snd_antitone` 📖	mathematical	—	`Antitone` `NNReal` `Nat.instPreorder` `PartialOrder.toPreorder` `instPartialOrderNNReal` `agmSequences`	—	`agmSequences_monotone_and_antitone`
`agmSequences_succ` 📖	mathematical	—	`agmSequences` `DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instDiv` `Distrib.toAdd` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	—
`agmSequences_succ'` 📖	mathematical	—	`agmSequences` `NNReal` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instDiv` `Distrib.toAdd` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `agmSequences.eq_1` `Function.iterate_succ'`
`agmSequences_zero` 📖	mathematical	—	`agmSequences` `NNReal` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instDiv` `Distrib.toAdd` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	—
`agm_comm` 📖	mathematical	—	`agm`	—	`agmSequences_comm`
`agm_eq_agm_agmSequences_fst_agmSequences_snd` 📖	mathematical	—	`agm` `NNReal` `agmSequences`	—	`tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_agmSequences_snd_agm` `add_right_comm` `Filter.tendsto_add_atTop_iff_nat`
`agm_eq_agm_gm_am` 📖	mathematical	—	`agm` `DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instDiv` `Distrib.toAdd` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`agm_eq_agm_agmSequences_fst_agmSequences_snd`
`agm_eq_ciInf` 📖	mathematical	—	`agm` `iInf` `NNReal` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `agmSequences`	—	—
`agm_eq_ciSup` 📖	mathematical	—	`agm` `iSup` `NNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `agmSequences`	—	`tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.congr_dist` `tendsto_agmSequences_snd_agm` `dist_comm` `tendsto_dist_agmSequences_atTop_zero` `tendsto_atTop_ciSup` `LinearOrder.supConvergenceClass` `instOrderTopology` `agmSequences_fst_monotone` `bddAbove_range_agmSequences_fst`
`agm_le_agmSequences_snd` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `agm` `agmSequences`	—	`ciInf_le'`
`agm_le_max` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `agm` `instMax`	—	`max_eq_right` `LE.le.trans` `agm_le_agmSequences_snd` `Nat.instAtLeastTwoHAddOfNat` `agmSequences_zero` `le_gm_and_am_le` `agm_comm` `max_comm` `LT.lt.le` `not_le`
`agm_lt_agmSequences_snd_of_ne` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `agm` `agmSequences`	—	`agm_eq_agm_agmSequences_fst_agmSequences_snd` `LE.le.trans_lt` `agm_le_agmSequences_snd` `agmSequences_fst_lt_snd_of_ne` `Nat.instAtLeastTwoHAddOfNat` `add_halves` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `add_div` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `addLeftMono` `div_lt_div_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo`
`agm_lt_max_of_ne` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `agm` `instMax`	—	`max_eq_right` `LT.lt.le` `LT.lt.trans_le` `agm_lt_agmSequences_snd_of_ne` `Nat.instAtLeastTwoHAddOfNat` `agmSequences_zero` `le_gm_and_am_le` `agm_comm` `max_comm` `Ne.gt_or_lt`
`agm_mul_distrib` 📖	mathematical	—	`agm` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`mul_iInf` `Nat.instAtLeastTwoHAddOfNat` `mul_add` `Distrib.leftDistribClass` `agmSequences_succ` `mul_div_assoc` `mul_mul_mul_comm` `sq` `sqrt_mul` `sqrt_sq`
`agm_pos` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`agm`	—	`LT.lt.trans_le` `lt_min` `min_le_agm`
`agm_self` 📖	mathematical	—	`agm`	—	`le_antisymm` `max_self` `agm_le_max` `min_self` `min_le_agm`
`agm_zero_left` 📖	mathematical	—	`agm` `NNReal` `instZeroNNReal`	—	`zero_add` `Function.iterate_one` `MulZeroClass.zero_mul` `sqrt_zero` `Nat.instAtLeastTwoHAddOfNat` `agmSequences_succ'` `agm_eq_ciSup` `ciSup_const`
`agm_zero_right` 📖	mathematical	—	`agm` `NNReal` `instZeroNNReal`	—	`agm_comm` `agm_zero_left`
`bddAbove_range_agmSequences_fst` 📖	mathematical	—	`BddAbove` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Set.range` `agmSequences`	—	`bddAbove_def` `agmSequences_fst_le_snd`
`dist_agmSequences_fst_snd` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `NNReal` `PseudoMetricSpace.toDist` `instPseudoMetricSpaceNNReal` `agmSequences` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `zero_add` `pow_one` `agmSequences_succ'` `LE.le.trans` `dist_gm_am_le` `pow_succ` `div_div` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo`
`dist_gm_am_le` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `NNReal` `PseudoMetricSpace.toDist` `instPseudoMetricSpaceNNReal` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instDiv` `Distrib.toAdd` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	—	`Nat.instAtLeastTwoHAddOfNat` `dist_comm` `dist_eq` `coe_sub` `sqrt_mul_le_half_add` `abs_eq` `tsub_le_tsub` `instOrderedSub` `addLeftMono` `le_refl` `le_sqrt_iff_sq_le` `sq` `mul_le_mul_right` `mulLeftMono` `add_halves` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `add_div` `add_tsub_add_eq_tsub_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `addLeftReflectLT` `tsub_div` `instCanonicallyOrderedAdd` `coe_div` `coe_two` `mul_comm` `add_comm` `LT.lt.le` `not_le`
`le_gm_and_am_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal`	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `sqrt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instDiv` `Distrib.toAdd` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `le_sqrt_iff_sq_le` `sq` `mul_le_mul_right` `mulLeftMono` `div_le_of_le_mul'` `two_mul` `add_le_add_left` `covariant_swap_add_of_covariant_add` `addLeftMono`
`min_le_agm` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instMin` `agm`	—	`min_eq_left` `le_trans` `Nat.instAtLeastTwoHAddOfNat` `agmSequences_zero` `le_gm_and_am_le` `agmSequences_fst_le_agm` `min_comm` `agm_comm` `LT.lt.le` `not_le`
`min_lt_agm_of_pos_of_ne` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`instMin` `agm`	—	`min_eq_left` `LT.lt.le` `lt_of_le_of_lt` `Nat.instAtLeastTwoHAddOfNat` `agmSequences_zero` `le_gm_and_am_le` `agmSequences_fst_lt_agm_of_pos_of_ne` `min_comm` `agm_comm` `Ne.gt_or_lt`
`sqrt_mul_le_half_add` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `sqrt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instDiv` `Distrib.toAdd` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sqrt_le_iff_le_sq` `div_pow` `le_div_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `mul_assoc` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `four_mul_le_sq_add` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `addLeftReflectLT` `addLeftMono`
`sqrt_mul_lt_half_add_of_ne` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `sqrt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instDiv` `Distrib.toAdd` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sq_pos_iff` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `zero_lt_iff` `tsub_pos_iff_lt` `instOrderedSub` `sqrt_sq` `sqrt_lt_sqrt` `div_pow` `lt_div_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `add_sq` `add_right_comm` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `addLeftMono` `sq` `tsub_tsub` `tsub_add_eq_add_tsub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `addLeftReflectLT` `mul_le_mul_right` `mulLeftMono` `le_of_lt` `tsub_tsub_eq_add_tsub_of_le` `mul_tsub` `LE.total` `tsub_mul` `covariant_swap_mul_of_covariant_mul` `mul_comm` `add_comm` `Ne.gt_or_lt`
`tendsto_agmSequences_fst_agm` 📖	mathematical	—	`Filter.Tendsto` `NNReal` `agmSequences` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `agm`	—	`agm_eq_ciSup` `tendsto_atTop_ciSup` `LinearOrder.supConvergenceClass` `instOrderTopology` `agmSequences_fst_monotone` `bddAbove_range_agmSequences_fst`
`tendsto_agmSequences_snd_agm` 📖	mathematical	—	`Filter.Tendsto` `NNReal` `agmSequences` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `agm`	—	`tendsto_atTop_ciInf` `LinearOrder.infConvergenceClass` `instOrderTopology` `agmSequences_snd_antitone` `OrderBot.bddBelow`
`tendsto_dist_agmSequences_atTop_zero` 📖	mathematical	—	`Filter.Tendsto` `Real` `Dist.dist` `NNReal` `PseudoMetricSpace.toDist` `instPseudoMetricSpaceNNReal` `agmSequences` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`squeeze_zero` `Nat.instAtLeastTwoHAddOfNat` `dist_nonneg` `dist_agmSequences_fst_snd` `MulZeroClass.zero_mul` `pow_succ'` `div_div` `div_eq_inv_mul` `inv_pow` `Filter.Tendsto.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_pow_atTop_nhds_zero_of_lt_one` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Real.instArchimedean` `instOrderTopologyReal` `Mathlib.Meta.NormNum.isRat_le_true` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `Nat.cast_one`

---

← Back to Index