LiouvilleWith

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

Statistics

Metric	Count
Definitions LiouvilleWith	1
Theorems frequently_exists_num, liouvilleWith, add_int, add_int_iff, add_nat, add_nat_iff, add_rat, add_rat_iff, exists_pos, frequently_lt_rpow_neg, int_add, int_add_iff, int_mul, int_mul_iff, int_sub, int_sub_iff, irrational, mono, mul_int, mul_int_iff, mul_nat, mul_nat_iff, mul_rat, mul_rat_iff, nat_add, nat_add_iff, nat_mul, nat_mul_iff, nat_sub, nat_sub_iff, ne_cast_int, neg, neg_iff, rat_add, rat_add_iff, rat_mul, rat_mul_iff, rat_sub, rat_sub_iff, sub_int, sub_int_iff, sub_nat, sub_nat_iff, sub_rat, sub_rat_iff, forall_liouvilleWith_iff, liouvilleWith_one	47
Total	48

Liouville

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frequently_exists_num 📖	mathematical	Liouville	Filter.Frequently Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instIntCast Real.instNatCast Real.instLT abs Real.lattice Real.instAddGroup Real.instSub Real.instOne Monoid.toNatPow Real.instMonoid Filter.atTop Nat.instPreorder	—	instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Mathlib.Tactic.Push.not_and_eq Nat.one_lt_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike one_div Filter.Tendsto.comp tendsto_inv_atTop_zero Real.instIsStrictOrderedRing instOrderTopologyReal tendsto_pow_atTop_atTop_of_one_lt AddGroup.existsAddOfLE Real.instArchimedean Filter.Eventually.mono Filter.Tendsto.eventually Irrational.eventually_forall_le_dist_cast_div irrational Set.Finite.eventually_all Set.finite_lt_nat Filter.eventually_imp_distrib_left Filter.Eventually.exists Filter.atTop_neBot Filter.Eventually.and Filter.eventually_ge_atTop CanLift.prf instCanLiftIntNatCastLeOfNat LE.le.trans zero_le_one Int.instZeroLEOneClass LT.lt.le le_or_gt LE.le.not_gt Int.cast_natCast LT.lt.trans_le div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one le_refl pow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' NeZero.charZero_one lt_trans Nat.instNontrivial Int.instAddLeftMono Int.instCharZero pow_le_pow_right₀ IsOrderedRing.toPosMulMono
liouvilleWith 📖	mathematical	Liouville	LiouvilleWith	—	Real.instIsStrictOrderedRing Filter.Frequently.mono Filter.Eventually.and_frequently Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder frequently_exists_num Real.rpow_natCast LiouvilleWith.mono Nat.le_ceil

LiouvilleWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_int 📖	mathematical	LiouvilleWith	Real Real.instAdd Real.instIntCast	—	add_int_iff
add_int_iff 📖	mathematical	—	LiouvilleWith Real Real.instAdd Real.instIntCast	—	Rat.cast_intCast add_rat_iff
add_nat 📖	mathematical	LiouvilleWith	Real Real.instAdd Real.instNatCast	—	add_int
add_nat_iff 📖	mathematical	—	LiouvilleWith Real Real.instAdd Real.instNatCast	—	Rat.cast_natCast add_rat_iff
add_rat 📖	mathematical	LiouvilleWith	Real Real.instAdd Real.instRatCast	—	exists_pos Filter.Tendsto.frequently Filter.Tendsto.nsmul_atTop Nat.instIsOrderedAddMonoid Filter.tendsto_id Rat.pos Filter.Frequently.mono smul_eq_mul Rat.num_div_den Int.cast_add Int.cast_mul Int.cast_natCast Nat.cast_mul Rat.cast_div RCLike.charZero_rclike Rat.cast_intCast Rat.cast_natCast add_div mul_div_mul_left ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one mul_div_mul_right lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat add_sub_add_right_eq_sub AddRightCancelSemigroup.toIsRightCancelAdd LT.lt.trans_le le_of_eq Real.rpow_pos_of_pos Real.mul_rpow Real.instIsOrderedRing
add_rat_iff 📖	mathematical	—	LiouvilleWith Real Real.instAdd Real.instRatCast	—	Rat.cast_neg add_neg_cancel_right add_rat
exists_pos 📖	mathematical	LiouvilleWith	Filter.Frequently Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instIntCast Real.instNatCast Real.instLT abs Real.lattice Real.instAddGroup Real.instSub Real.instPow Filter.atTop Nat.instPreorder	—	LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike le_max_right Filter.Frequently.mono Filter.Eventually.and_frequently Filter.eventually_ge_atTop div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing le_max_left le_of_lt Real.rpow_pos_of_pos Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat
frequently_lt_rpow_neg 📖	mathematical	LiouvilleWith Real Real.instLT	Filter.Frequently DivInvMonoid.toDiv Real.instDivInvMonoid Real.instIntCast Real.instNatCast abs Real.lattice Real.instAddGroup Real.instSub Real.instPow Real.instNeg Filter.atTop Nat.instPreorder	—	exists_pos Filter.Tendsto.eventually Filter.Tendsto.comp tendsto_rpow_atTop sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instNontrivial Filter.Frequently.mono Filter.Eventually.and_frequently Nat.cast_pos LT.lt.trans div_lt_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Real.rpow_pos_of_pos mul_comm Real.rpow_add sub_eq_add_neg
int_add 📖	mathematical	LiouvilleWith	Real Real.instAdd Real.instIntCast	—	int_add_iff
int_add_iff 📖	mathematical	—	LiouvilleWith Real Real.instAdd Real.instIntCast	—	add_comm add_int_iff
int_mul 📖	mathematical	LiouvilleWith	Real Real.instMul Real.instIntCast	—	int_mul_iff
int_mul_iff 📖	mathematical	—	LiouvilleWith Real Real.instMul Real.instIntCast	—	mul_comm mul_int_iff
int_sub 📖	mathematical	LiouvilleWith	Real Real.instSub Real.instIntCast	—	int_sub_iff
int_sub_iff 📖	mathematical	—	LiouvilleWith Real Real.instSub Real.instIntCast	—	sub_eq_add_neg
irrational 📖	mathematical	LiouvilleWith Real Real.instLT Real.instOne	Irrational	—	eq_or_ne ne_cast_int Rat.cast_zero Int.cast_zero mul_rat inv_ne_zero Rat.cast_inv RCLike.charZero_rclike mul_inv_cancel₀ Rat.cast_ne_zero Int.cast_one
mono 📖	—	LiouvilleWith Real Real.instLE	—	—	exists_pos Filter.Frequently.mono LT.lt.trans_le div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono le_of_lt le_refl Real.rpow_pos_of_pos Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Real.rpow_le_rpow_of_exponent_le Nat.cast_one
mul_int 📖	mathematical	LiouvilleWith	Real Real.instMul Real.instIntCast	—	mul_int_iff
mul_int_iff 📖	mathematical	—	LiouvilleWith Real Real.instMul Real.instIntCast	—	Rat.cast_intCast mul_rat_iff Int.cast_ne_zero Rat.instCharZero
mul_nat 📖	mathematical	LiouvilleWith	Real Real.instMul Real.instNatCast	—	mul_nat_iff
mul_nat_iff 📖	mathematical	—	LiouvilleWith Real Real.instMul Real.instNatCast	—	Rat.cast_natCast mul_rat_iff Nat.cast_ne_zero Rat.instCharZero
mul_rat 📖	mathematical	LiouvilleWith	Real Real.instMul Real.instRatCast	—	exists_pos Filter.Tendsto.frequently Filter.Tendsto.nsmul_atTop Nat.instIsOrderedAddMonoid Filter.tendsto_id Rat.pos Filter.Frequently.mono mul_comm Int.cast_mul Nat.cast_mul Rat.cast_def IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain RCLike.charZero_rclike sub_mul abs_mul Real.instIsOrderedRing mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.abs_pos_of_ne_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Rat.cast_ne_zero Real.mul_rpow le_of_lt Nat.cast_pos' Real.instZeroLEOneClass NeZero.charZero_one lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat mul_div_mul_left ne_of_gt Real.rpow_pos_of_pos mul_div_assoc Rat.cast_abs
mul_rat_iff 📖	mathematical	—	LiouvilleWith Real Real.instMul Real.instRatCast	—	mul_assoc RCLike.charZero_rclike mul_inv_cancel₀ Rat.cast_one mul_one mul_rat inv_ne_zero
nat_add 📖	mathematical	LiouvilleWith	Real Real.instAdd Real.instNatCast	—	int_add
nat_add_iff 📖	mathematical	—	LiouvilleWith Real Real.instAdd Real.instNatCast	—	add_comm add_nat_iff
nat_mul 📖	mathematical	LiouvilleWith	Real Real.instMul Real.instNatCast	—	mul_comm mul_nat
nat_mul_iff 📖	mathematical	—	LiouvilleWith Real Real.instMul Real.instNatCast	—	mul_comm mul_nat_iff
nat_sub 📖	mathematical	LiouvilleWith	Real Real.instSub Real.instNatCast	—	nat_sub_iff
nat_sub_iff 📖	mathematical	—	LiouvilleWith Real Real.instSub Real.instNatCast	—	sub_eq_add_neg
ne_cast_int 📖	—	LiouvilleWith Real Real.instLT Real.instOne	—	—	Filter.Frequently.exists Filter.Eventually.and_frequently Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder frequently_lt_rpow_neg LT.lt.not_ge Real.instIsOrderedRing Real.instNontrivial Real.rpow_neg_one one_div sub_div' LT.lt.ne' abs_div Real.instIsStrictOrderedRing Nat.abs_cast div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.cast_one Int.cast_natCast Int.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike zero_add abs_pos Int.instAddLeftMono sub_ne_zero eq_div_iff le_of_lt Nat.cast_pos'
neg 📖	mathematical	LiouvilleWith	Real Real.instNeg	—	Filter.Frequently.mono Int.cast_neg neg_div abs_sub_comm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.sub_pf Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt
neg_iff 📖	mathematical	—	LiouvilleWith Real Real.instNeg	—	neg neg_neg
rat_add 📖	mathematical	LiouvilleWith	Real Real.instAdd Real.instRatCast	—	add_rat add_comm
rat_add_iff 📖	mathematical	—	LiouvilleWith Real Real.instAdd Real.instRatCast	—	add_comm add_rat_iff
rat_mul 📖	mathematical	LiouvilleWith	Real Real.instMul Real.instRatCast	—	rat_mul_iff
rat_mul_iff 📖	mathematical	—	LiouvilleWith Real Real.instMul Real.instRatCast	—	mul_comm mul_rat_iff
rat_sub 📖	mathematical	LiouvilleWith	Real Real.instSub Real.instRatCast	—	rat_sub_iff
rat_sub_iff 📖	mathematical	—	LiouvilleWith Real Real.instSub Real.instRatCast	—	sub_eq_add_neg
sub_int 📖	mathematical	LiouvilleWith	Real Real.instSub Real.instIntCast	—	sub_int_iff
sub_int_iff 📖	mathematical	—	LiouvilleWith Real Real.instSub Real.instIntCast	—	Rat.cast_intCast sub_rat_iff
sub_nat 📖	mathematical	LiouvilleWith	Real Real.instSub Real.instNatCast	—	sub_nat_iff
sub_nat_iff 📖	mathematical	—	LiouvilleWith Real Real.instSub Real.instNatCast	—	Rat.cast_natCast sub_rat_iff
sub_rat 📖	mathematical	LiouvilleWith	Real Real.instSub Real.instRatCast	—	sub_rat_iff
sub_rat_iff 📖	mathematical	—	LiouvilleWith Real Real.instSub Real.instRatCast	—	sub_eq_add_neg Rat.cast_neg add_rat_iff

(root)

Definitions

Name	Category	Theorems
LiouvilleWith 📖	MathDef	24 math math: LiouvilleWith.nat_sub_iff, volume_iUnion_setOf_liouvilleWith, LiouvilleWith.rat_sub_iff, LiouvilleWith.rat_add_iff, LiouvilleWith.mul_int_iff, LiouvilleWith.neg_iff, setOf_liouvilleWith_subset_aux, LiouvilleWith.int_sub_iff, LiouvilleWith.add_rat_iff, LiouvilleWith.add_int_iff, Liouville.liouvilleWith, LiouvilleWith.int_add_iff, LiouvilleWith.sub_int_iff, forall_liouvilleWith_iff, LiouvilleWith.rat_mul_iff, LiouvilleWith.mul_rat_iff, LiouvilleWith.int_mul_iff, LiouvilleWith.sub_nat_iff, liouvilleWith_one, LiouvilleWith.sub_rat_iff, LiouvilleWith.mul_nat_iff, LiouvilleWith.nat_add_iff, LiouvilleWith.add_nat_iff, LiouvilleWith.nat_mul_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_liouvilleWith_iff 📖	mathematical	—	LiouvilleWith Liouville	—	Filter.Frequently.exists Filter.Eventually.and_frequently Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder LiouvilleWith.frequently_lt_rpow_neg lt_add_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_one Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero Int.cast_natCast one_div Real.rpow_neg Real.instIsOrderedRing Real.rpow_natCast Liouville.liouvilleWith
liouvilleWith_one 📖	mathematical	—	LiouvilleWith Real Real.instOne	—	Nat.instAtLeastTwoHAddOfNat Filter.Eventually.frequently Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Eventually.mono Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Real.instIsOrderedRing Real.instNontrivial lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Int.cast_add Int.cast_one Int.lt_floor_add_one LT.lt.ne abs_sub_comm abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Real.rpow_one sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd add_div_eq_mul_add_div LT.lt.ne' div_lt_div_of_pos_right add_le_add_left Int.floor_le lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.sub_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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul 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 Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Nat.cast_pos' Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike

---

← Back to Index