Wallis

📁 Source: Mathlib/Analysis/Real/Pi/Wallis.lean

Statistics

Metric	Count
Definitions	0
Theorems W_eq_factorial_ratio, W_eq_integral_sin_pow_div_integral_sin_pow, W_le, W_pos, W_succ, le_W, tendsto_W_nhds_pi_div_two, tendsto_prod_pi_div_two	8
Total	8

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_prod_pi_div_two 📖	mathematical	—	Filter.Tendsto Real Finset.prod instCommMonoid Finset.range instMul DivInvMonoid.toDiv instDivInvMonoid instAdd instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace pi	—	Wallis.tendsto_W_nhds_pi_div_two

Real.Wallis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
W_eq_factorial_ratio 📖	mathematical	—	W Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Nat.factorial Real.instAdd Real.instOne	—	Nat.instAtLeastTwoHAddOfNat Finset.prod_range_zero MulZeroClass.mul_zero pow_zero Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.instAtLeastTwo Finset.prod_range_succ div_mul_div_comm div_eq_div_iff ne_of_gt mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing pow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one Nat.factorial_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Nat.cast_nonneg' add_pos' Nat.instIsOrderedAddMonoid zero_le Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial pow_succ Nat.cast_mul Nat.cast_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right 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.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one add_zero Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.add_assoc_rev
W_eq_integral_sin_pow_div_integral_sin_pow 📖	mathematical	—	Real Real.instMul Real.instInv DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat W intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.sin Real.instZero MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Nat.instAtLeastTwoHAddOfNat integral_sin_pow_even integral_sin_pow_odd mul_div_mul_comm Finset.prod_div_distrib inv_div Finset.prod_congr div_div_div_comm div_div_eq_mul_div mul_div_assoc
W_le 📖	mathematical	—	Real Real.instLE W DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat div_le_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.pi_div_two_pos div_eq_inv_mul W_eq_integral_sin_pow_div_integral_sin_pow integral_sin_pow_pos integral_sin_pow_succ_le
W_pos 📖	mathematical	—	Real Real.instLT Real.instZero W	—	Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Nat.instAtLeastTwoHAddOfNat W_succ mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_nonneg' Nat.cast_one
W_succ 📖	mathematical	—	W Real Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instOne	—	Finset.prod_range_succ
le_W 📖	mathematical	—	Real Real.instLE Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instOne Real.pi W	—	Nat.instAtLeastTwoHAddOfNat le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Real.pi_div_two_pos div_eq_inv_mul W_eq_integral_sin_pow_div_integral_sin_pow integral_sin_pow_pos integral_sin_pow Real.sin_zero zero_pow IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.instCharZero Real.cos_zero mul_one Real.sin_pi Real.cos_pi mul_neg neg_zero sub_self Nat.cast_mul zero_div zero_add integral_sin_pow_succ_le
tendsto_W_nhds_pi_div_two 📖	mathematical	—	Filter.Tendsto Real W Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	tendsto_of_tendsto_of_tendsto_of_le_of_le instOrderTopologyReal Nat.instAtLeastTwoHAddOfNat sub_zero one_mul Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal sub_div' ne_of_gt add_pos_of_nonneg_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Nat.cast_nonneg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Filter.Tendsto.const_sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Filter.Tendsto.div_atTop Real.instIsStrictOrderedRing tendsto_const_nhds Filter.Tendsto.atTop_add Filter.Tendsto.const_mul_atTop tendsto_natCast_atTop_atTop Real.instArchimedean le_W W_le

---

← Back to Index