Behrend

📁 Source: Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

Statistics

Metric	Count
Definitions box, dValue, map, nValue, sphere	5
Theorems bound_aux, bound_aux', box_zero, card_box, card_sphere_le_rothNumberNat, ceil_lt_mul, dValue_pos, div_lt_floor, exists_large_sphere, exists_large_sphere_aux, exp_four_lt, exp_neg_two_mul_le, four_zero_nine_six_lt_exp_sixteen, le_N, le_sqrt_log, log_two_mul_two_le_sqrt_log_eight, lower_bound_le_one, lower_bound_le_one', map_apply, map_eq_iff, map_injOn, map_le_of_mem_box, map_mod, map_monotone, map_succ, map_succ', map_zero, mem_box, nValue_pos, norm_of_mem_sphere, roth_lower_bound, roth_lower_bound_explicit, sphere_subset_box, sphere_subset_preimage_metric_sphere, sphere_zero_right, sphere_zero_subset, sum_eq, sum_lt, sum_sq_le_of_mem_box, threeAPFree_image_sphere, threeAPFree_sphere, three_le_nValue, two_div_one_sub_two_div_e_le_eight, threeAPFree_frontier, threeAPFree_sphere	45
Total	50

Behrend

Definitions

Name	Category	Theorems
box 📖	CompOp	4 math math: box_zero, mem_box, card_box, sphere_subset_box
dValue 📖	CompOp	3 math math: le_N, bound, dValue_pos
map 📖	CompOp	10 math math: map_mod, map_succ, map_le_of_mem_box, map_injOn, map_apply, map_succ', map_zero, map_eq_iff, threeAPFree_image_sphere, map_monotone
nValue 📖	CompOp	4 math math: le_N, nValue_pos, three_le_nValue, bound
sphere 📖	CompOp	9 math math: sphere_subset_preimage_metric_sphere, sphere_zero_right, sphere_zero_subset, card_sphere_le_rothNumberNat, threeAPFree_image_sphere, exists_large_sphere_aux, sphere_subset_box, threeAPFree_sphere, exists_large_sphere

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound_aux 📖	mathematical	—	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.instNatCast DFunLike.coe OrderHom Nat.instPreorder OrderHom.instFunLike rothNumberNat Nat.instMonoid	—	Nat.cast_mul Nat.cast_pow mul_comm div_div pow_sub₀ Nat.cast_ne_zero RCLike.charZero_rclike div_eq_mul_inv bound_aux'
bound_aux' 📖	mathematical	—	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Monoid.toNatPow Nat.instMonoid DFunLike.coe OrderHom Nat.instPreorder OrderHom.instFunLike rothNumberNat	—	exists_large_sphere LE.le.trans Nat.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike card_sphere_le_rothNumberNat
box_zero 📖	mathematical	—	box Finset Finset.instEmptyCollection	—	Fintype.piFinset_empty
card_box 📖	mathematical	—	Finset.card box Monoid.toNatPow Nat.instMonoid	—	Fintype.card_piFinset Finset.prod_congr Finset.card_range Finset.prod_const Fintype.card_fin
card_sphere_le_rothNumberNat 📖	mathematical	—	Finset.card sphere DFunLike.coe OrderHom Nat.instPreorder OrderHom.instFunLike rothNumberNat Monoid.toNatPow Nat.instMonoid	—	LE.le.trans_eq Fin.isEmpty' Finset.card_le_univ sphere_zero_right MulZeroClass.mul_zero zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub zero_pow ThreeAPFree.le_rothNumberNat threeAPFree_image_sphere LE.le.trans_lt map_le_of_mem_box sum_lt Finset.card_image_of_injOn Set.InjOn.mono two_mul LT.lt.trans_le le_self_add map_injOn
ceil_lt_mul 📖	mathematical	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Real.instLT Nat.ceil Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing Real.instMul NNRatCast.toOfScientific Real.instNNRatCast	—	Nat.instAtLeastTwoHAddOfNat LT.lt.trans_le Real.instIsStrictOrderedRing Nat.ceil_lt_add_one LE.le.trans' 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_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike le_sub_iff_add_le' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_one_mul Mathlib.Meta.NormNum.isNNRat_eq_true Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero Mathlib.Meta.NormNum.isRat_sub Nat.cast_one div_eq_inv_mul one_le_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero
dValue_pos 📖	mathematical	—	dValue	—	Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial LT.lt.trans_le Nat.succ_pos' Real.instIsStrictOrderedRing dValue.eq_1 Nat.floor_pos Real.log_le_log_iff zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.rpow_pos_of_pos zero_lt_two IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.log_one Nat.instAtLeastTwoHAddOfNat Real.log_div LT.lt.ne' two_ne_zero CharZero.NeZero.two Real.log_rpow inv_mul_eq_div sub_nonneg covariant_swap_add_of_covariant_add le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono nValue_pos LE.le.trans' LE.le.trans LT.lt.le Nat.ceil_lt_add_one Real.sqrt_nonneg two_mul add_le_add_iff_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.le_sqrt_of_sq_le one_pow Real.le_log_iff_exp_le Real.exp_one_lt_d9 Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Nat.cast_le mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.log_nonneg one_le_two mul_assoc Real.sqrt_pos Real.log_pos Nat.one_lt_cast LE.le.trans_lt' Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Real.div_sqrt log_two_mul_two_le_sqrt_log_eight Real.sqrt_le_sqrt Real.log_le_log
div_lt_floor 📖	mathematical	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne Real.exp	Real.instLT Nat.floor Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing	—	Nat.instAtLeastTwoHAddOfNat lt_of_le_of_lt Real.instIsStrictOrderedRing sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.exp_pos Real.exp_one_gt_two le_sub_comm div_eq_mul_one_div mul_sub div_sub' two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike mul_div_assoc' one_le_div zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.sub_one_lt_floor
exists_large_sphere 📖	mathematical	—	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Monoid.toNatPow Nat.instMonoid Finset.card sphere	—	exists_large_sphere_aux pow_zero Nat.cast_one MulZeroClass.zero_mul CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike div_zero Real.instIsOrderedRing Nat.cast_pow zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero LE.le.trans div_le_div_of_nonneg_left PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.cast_nonneg Nat.cast_add_one_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one Nat.cast_mul Nat.cast_sub sub_sq mul_one one_pow sub_add sub_sub_self one_le_mul_of_one_le_of_one_le IsOrderedRing.toPosMulMono Nat.one_le_cast le_sub_iff_add_le covariant_swap_add_of_covariant_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_lt_true Nat.cast_zero Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass
exists_large_sphere_aux 📖	mathematical	—	Finset Finset.instMembership Finset.range Monoid.toNatPow Nat.instMonoid Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast Real.instAdd Real.instOne Finset.card sphere	—	Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to Real.instIsStrictOrderedRing Finset.mem_range sum_sq_le_of_mem_box Finset.nonempty_range_add_one Finset.card_range nsmul_eq_mul mul_div_assoc' Nat.cast_add_one mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass LT.lt.ne' Nat.cast_add_one_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike card_box le_refl
exp_four_lt 📖	mathematical	—	Real Real.instLT Real.exp instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Real.rpow_natCast Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit0 Real.lt_log_iff_exp_lt Real.rpow_pos_of_pos zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.log_rpow div_lt_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing Real.instNontrivial LT.lt.trans_le' Real.log_two_gt_d9 Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero
exp_neg_two_mul_le 📖	mathematical	Real Real.instLT Real.instZero	Real.exp Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Nat.ceil Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing	—	Real.instIsStrictOrderedRing Nat.ceil_lt_add_one LT.lt.le Nat.instAtLeastTwoHAddOfNat le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero 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_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike le_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.exp_pos Real.exp_sub neg_mul sub_neg_eq_add two_mul sub_add_add_cancel add_comm le_trans le_add_of_nonneg_right zero_le_one Real.add_one_le_exp div_le_div_of_nonneg_right Real.exp_monotone le_of_lt add_pos' Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial div_lt_div_of_pos_left Nat.cast_pos' Mathlib.Meta.Positivity.nat_ceil_pos
four_zero_nine_six_lt_exp_sixteen 📖	mathematical	—	Real Real.instLT instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.exp	—	Nat.instAtLeastTwoHAddOfNat Real.log_lt_iff_lt_exp Real.instIsOrderedRing Real.instNontrivial RCLike.charZero_rclike Real.rpow_natCast Real.log_rpow zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_ofNat lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo 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.Tactic.Ring.neg_congr 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Tactic.Linarith.sub_neg_of_lt Real.log_two_lt_d9
le_N 📖	mathematical	—	Monoid.toNatPow Nat.instMonoid dValue nValue	—	LE.le.trans Nat.instAtLeastTwoHAddOfNat le_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.floor_le div_nonneg Real.rpow_nonneg Nat.cast_nonneg Real.instIsOrderedRing zero_le_two Real.rpow_natCast Real.rpow_le_rpow mul_nonneg IsOrderedRing.toPosMulMono Real.rpow_mul inv_mul_cancel₀ Nat.cast_ne_zero LT.lt.ne' nValue_pos Real.rpow_one le_refl
le_sqrt_log 📖	mathematical	—	Real Real.instLE Real.instMul Real.log DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne Real.exp Real.sqrt	—	Nat.instAtLeastTwoHAddOfNat mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing Real.log_le_log Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Real.exp_pos Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' zero_lt_one Real.instZeroLEOneClass NeZero.one GroupWithZero.toNontrivial mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1 two_div_one_sub_two_div_e_le_eight le_of_lt div_pos Real.log_pow Real.le_sqrt_of_sq_le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.sub_congr Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul 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_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.mul_subst Mathlib.Meta.NormNum.isNat_eq_true CancelDenoms.pow_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero Real.log_two_lt_d9 Real.log_two_gt_d9 Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le sq_nonneg IsOrderedRing.toPosMulMono mul_pos_of_neg_of_neg IsStrictOrderedRing.toMulPosStrictMono Real.sqrt_monotone pow_pos IsStrictOrderedRing.toZeroLEOneClass
log_two_mul_two_le_sqrt_log_eight 📖	mathematical	—	Real Real.instLE Real.instMul Real.log instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.sqrt	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1 Real.log_pow Nat.cast_ofNat Real.le_sqrt_of_sq_le mul_pow sq mul_assoc mul_comm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_congr 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_neg_of_lt CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le LT.lt.le Real.log_two_lt_d9 le_of_lt Mathlib.Meta.Positivity.log_pos_of_isNat
lower_bound_le_one 📖	mathematical	—	Real Real.instLE Real.instMul Real.instNatCast Real.exp Real.instNeg instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.sqrt Real.log Real.instOne	—	Nat.instAtLeastTwoHAddOfNat LE.le.eq_or_lt Nat.cast_one Real.log_one Real.sqrt_zero MulZeroClass.mul_zero Real.exp_zero mul_one lower_bound_le_one'
lower_bound_le_one' 📖	mathematical	—	Real Real.instLE Real.instMul Real.instNatCast Real.exp Real.instNeg instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.sqrt Real.log Real.instOne	—	Nat.instAtLeastTwoHAddOfNat Real.log_le_log_iff mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial LT.lt.trans_le zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Real.exp_pos zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.log_one Real.log_mul LT.lt.ne' Real.log_exp neg_mul sub_eq_add_neg sub_nonpos covariant_swap_add_of_covariant_add Real.instIsOrderedAddMonoid div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.sqrt_pos Real.log_pos Nat.one_lt_cast one_lt_two IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Real.div_sqrt Real.sqrt_le_left zero_le_four Real.log_le_iff_le_exp Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 le_trans LT.lt.le four_zero_nine_six_lt_exp_sixteen
map_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidHom.instFunLike map Finset.sum Nat.instAddCommMonoid Finset.univ Fin.fintype Monoid.toNatPow Nat.instMonoid	—	—
map_eq_iff 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidHom.instFunLike map	—	map_mod mul_eq_mul_right_iff IsCancelMulZero.toIsRightCancelMulZero Nat.instIsCancelMulZero AddLeftCancelSemigroup.toIsLeftCancelAdd map_succ LT.lt.ne' pos_of_gt Nat.instCanonicallyOrderedAdd map_succ'
map_injOn 📖	mathematical	—	Set.InjOn DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidHom.instFunLike map setOf	—	Unique.instSubsingleton Fin.isEmpty' map_eq_iff
map_le_of_mem_box 📖	mathematical	Finset Finset.instMembership box	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidHom.instFunLike map Finset.sum Nat.instAddCommMonoid Finset.univ Fin.fintype Monoid.toNatPow Nat.instMonoid	—	map_monotone mem_box
map_mod 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidHom.instFunLike map	—	map_succ
map_monotone 📖	mathematical	—	Monotone Pi.preorder Nat.instPreorder DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidHom.instFunLike map	—	Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
map_succ 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidHom.instFunLike map Finset.sum Nat.instAddCommMonoid Finset.univ Fin.fintype Monoid.toNatPow Nat.instMonoid	—	Fin.sum_univ_succ pow_zero mul_one Finset.sum_congr pow_succ
map_succ' 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidHom.instFunLike map	—	map_succ
map_zero 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidHom.instFunLike map	—	Finset.sum_congr Finset.univ_eq_empty Fin.isEmpty'
mem_box 📖	mathematical	—	Finset Finset.instMembership box	—	—
nValue_pos 📖	mathematical	—	nValue	—	Real.instIsStrictOrderedRing Nat.ceil_pos Real.sqrt_pos Real.log_pos Nat.one_lt_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike
norm_of_mem_sphere 📖	mathematical	Finset Finset.instMembership sphere	Norm.norm WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat PiLp.instNorm Real Fin.fintype Real.norm WithLp.toLp Real.instNatCast Real.sqrt	—	Nat.instAtLeastTwoHAddOfNat EuclideanSpace.norm_eq Finset.sum_congr Nat.abs_cast Real.instIsOrderedRing Finset.mem_filter
roth_lower_bound 📖	mathematical	—	Real Real.instLE Real.instMul Real.instNatCast Real.exp Real.instNeg instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.sqrt Real.log DFunLike.coe OrderHom Nat.instPreorder OrderHom.instFunLike rothNumberNat	—	Nat.instAtLeastTwoHAddOfNat CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike Real.log_zero Real.sqrt_zero MulZeroClass.mul_zero Real.exp_zero mul_one le_or_gt LT.lt.le roth_lower_bound_explicit LE.le.trans lower_bound_le_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass zero_add OrderHom.monotone
roth_lower_bound_explicit 📖	mathematical	—	Real Real.instLT Real.instMul Real.instNatCast Real.exp Real.instNeg instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.sqrt Real.log DFunLike.coe OrderHom Nat.instPreorder OrderHom.instFunLike rothNumberNat	—	Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial nValue_pos LE.le.trans' Mathlib.Meta.NormNum.isNat_le_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Mathlib.Meta.NormNum.isNat_ofNat dValue_pos Mathlib.Meta.NormNum.isNat_natSucc three_le_nValue le_N Nat.instAtLeastTwoHAddOfNat Real.rpow_natCast Real.div_rpow Real.rpow_nonneg LT.lt.le Real.exp_pos Real.rpow_mul inv_mul_eq_div Nat.cast_sub Nat.cast_two same_sub_div LT.lt.ne' Real.exp_one_rpow div_div Real.rpow_sub Real.rpow_one div_eq_mul_inv mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono mul_inv Real.exp_neg Real.rpow_neg Nat.cast_nonneg neg_sub Real.exp_add add_mul Distrib.rightDistribClass Mathlib.Meta.NormNum.instAtLeastTwo neg_mul Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt mul_le_mul IsOrderedRing.toMulPosMono Real.le_log_iff_exp_le Real.rpow_pos_of_pos Real.log_rpow le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Real.sqrt_pos Real.log_pos Nat.one_lt_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike LE.le.trans_lt' Mathlib.Meta.NormNum.isNat_lt_true Nat.instCharZero mul_div_assoc Real.div_sqrt neg_le_neg_iff covariant_swap_add_of_covariant_add div_mul_eq_mul_div div_le_iff₀ Nat.le_ceil le_of_lt Mathlib.Meta.Positivity.pos_of_isNat exp_neg_two_mul_le Nat.cast_pos' NeZero.charZero_one lt_of_lt_of_le Nat.instNontrivial div_lt_div_of_pos_right pow_lt_pow_left₀ IsStrictOrderedRing.toPosMulStrictMono bound div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE tsub_pos_of_lt Nat.instCanonicallyOrderedAdd Nat.instOrderedSub lt_trans bound_aux OrderHom.mono
sphere_subset_box 📖	mathematical	—	Finset Finset.instHasSubset sphere box	—	Finset.filter_subset
sphere_subset_preimage_metric_sphere 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike sphere Set.preimage WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat WithLp.toLp Real Real.instNatCast Metric.sphere PiLp.instPseudoMetricSpace fact_one_le_two_ennreal Fin.fintype Real.pseudoMetricSpace PiLp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup Real.instAddCommGroup Real.sqrt	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal Set.mem_preimage mem_sphere_zero_iff_norm norm_of_mem_sphere
sphere_zero_right 📖	mathematical	—	sphere Finset Finset.instEmptyCollection	—	Finset.filter.congr_simp box_zero Finset.filter_empty
sphere_zero_subset 📖	mathematical	—	Finset Finset.instHasSubset sphere Finset.zero Pi.instZero MulZeroClass.toZero Nat.instMulZeroClass	—	Finset.filter.congr_simp Unique.instSubsingleton Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
sum_eq 📖	mathematical	—	Finset.sum Nat.instAddCommMonoid Finset.univ Fin.fintype Monoid.toNatPow Nat.instMonoid	—	Nat.instAtLeastTwoHAddOfNat zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Finset.sum_range Finset.mul_sum mul_right_comm mul_comm geom_sum_mul_add add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
sum_lt 📖	mathematical	—	Finset.sum Nat.instAddCommMonoid Finset.univ Fin.fintype Monoid.toNatPow Nat.instMonoid	—	Eq.trans_lt sum_eq LE.le.trans_lt LT.lt.ne' pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass
sum_sq_le_of_mem_box 📖	mathematical	Finset Finset.instMembership box	Finset.sum Nat.instAddCommMonoid Finset.univ Fin.fintype Monoid.toNatPow Nat.instMonoid	—	mem_box LE.le.trans Finset.sum_le_card_nsmul IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Finset.card_fin smul_eq_mul le_refl
threeAPFree_image_sphere 📖	mathematical	—	ThreeAPFree Nat.instAddMonoid SetLike.coe Finset Finset.instSetLike Finset.image DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass AddMonoidHom.instFunLike map sphere	—	Finset.coe_image ThreeAPFree.image' AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass Set.InjOn.mono Set.add_subset_iff mem_box sphere_subset_box lt_tsub_iff_right Nat.instOrderedSub Nat.instAtLeastTwoHAddOfNat two_mul Eq.trans_le add_add_add_comm add_le_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add map_injOn threeAPFree_sphere
threeAPFree_sphere 📖	mathematical	—	ThreeAPFree Pi.addMonoid Nat.instAddMonoid SetLike.coe Finset Finset.instSetLike sphere	—	fact_one_le_two_ennreal Nat.instAtLeastTwoHAddOfNat PiLp.ext Nat.cast_zero Nat.cast_add ThreeAPFree.of_image AddMonoidHomClass.isAddFreimanHom AddMonoidHom.instAddMonoidHomClass Set.mapsTo_image Function.Injective.comp_injOn WithLp.toLp_injective Function.Injective.injOn Function.Injective.comp_left Nat.cast_injective RCLike.charZero_rclike Set.subset_univ ThreeAPFree.mono Set.image_subset_iff Set.mem_preimage mem_sphere_zero_iff_norm norm_of_mem_sphere threeAPFree_sphere UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace
three_le_nValue 📖	mathematical	—	nValue	—	Real.instIsStrictOrderedRing nValue.eq_1 Nat.lt_ceil Nat.instAtLeastTwoHAddOfNat Nat.cast_two Real.lt_sqrt_of_sq_lt Real.rpow_natCast LE.le.trans' Nat.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_le_true Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.isNat_natCast lt_of_lt_of_le Real.log_rpow zero_lt_two NeZero.charZero_one div_lt_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.NormNum.isNat_lt_true Nat.cast_zero LT.lt.trans_le' Real.log_two_gt_d9 Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero Real.log_le_log Real.rpow_pos_of_pos
two_div_one_sub_two_div_e_le_eight 📖	mathematical	—	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne Real.exp	—	Nat.instAtLeastTwoHAddOfNat div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono LT.lt.trans' Real.exp_one_gt_d9 Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast RCLike.charZero_rclike Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Mathlib.Meta.NormNum.instAtLeastTwo mul_sub mul_one mul_div_assoc' le_sub_comm Real.exp_pos le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_congr 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.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf 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_zero_add Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
threeAPFree_frontier 📖	mathematical	StrictConvex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	ThreeAPFree frontier	—	Nat.instAtLeastTwoHAddOfNat StrictConvex.eq IsClosed.frontier_subset one_half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono add_halves CharZero.NeZero.two IsStrictOrderedRing.toCharZero one_div Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 add_zero one_smul smul_add inv_smul_eq_iff₀ two_smul
threeAPFree_sphere 📖	mathematical	—	ThreeAPFree ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Metric.sphere	—	eq_or_ne Metric.sphere_zero threeAPFree_singleton frontier_closedBall threeAPFree_frontier Real.instIsStrictOrderedRing Metric.isClosed_closedBall strictConvex_closedBall

---

← Back to Index