Rayleigh

📁 Source: Mathlib/NumberTheory/Rayleigh.lean

Statistics

Metric	Count
Definitions beattySeq, beattySeq'	2
Theorems beattySeq'_pos_eq, beattySeq_symmDiff_beattySeq_pos, beattySeq'_symmDiff_beattySeq_pos, beattySeq_symmDiff_beattySeq'_pos, compl_beattySeq, compl_beattySeq'	6
Total	8

Irrational

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
beattySeq'_pos_eq 📖	mathematical	Irrational	setOf beattySeq' beattySeq	—	sub_eq_iff_eq_add Int.ceil_eq_iff Int.cast_add Int.cast_one add_sub_cancel_right LE.le.lt_of_ne Int.floor_le ne_int intCast_mul LT.lt.ne' LT.lt.le Int.lt_floor_add_one
beattySeq_symmDiff_beattySeq_pos 📖	mathematical	Real.HolderConjugate Irrational	symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff setOf beattySeq	—	beattySeq'_pos_eq beattySeq'_symmDiff_beattySeq_pos

(root)

Definitions

Name	Category	Theorems
beattySeq 📖	CompOp	6 math math: beattySeq'_symmDiff_beattySeq_pos, beattySeq_symmDiff_beattySeq'_pos, Irrational.beattySeq_symmDiff_beattySeq_pos, compl_beattySeq', compl_beattySeq, Irrational.beattySeq'_pos_eq
beattySeq' 📖	CompOp	5 math math: beattySeq'_symmDiff_beattySeq_pos, beattySeq_symmDiff_beattySeq'_pos, compl_beattySeq', compl_beattySeq, Irrational.beattySeq'_pos_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
beattySeq'_symmDiff_beattySeq_pos 📖	mathematical	Real.HolderConjugate	symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff setOf beattySeq' beattySeq	—	symmDiff_comm beattySeq_symmDiff_beattySeq'_pos Real.HolderConjugate.symm
beattySeq_symmDiff_beattySeq'_pos 📖	mathematical	Real.HolderConjugate	symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff setOf beattySeq beattySeq'	—	Set.eq_of_subset_of_subset Set.mem_setOf_eq beattySeq.eq_1 Int.floor_pos one_le_mul_of_one_le_of_one_le Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing Nat.cast_one Int.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing LT.lt.le Real.HolderTriple.lt beattySeq'.eq_1 sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.instAddLeftMono Int.lt_ceil one_lt_mul_of_le_of_lt IsOrderedRing.toMulPosMono Real.HolderConjugate.symm Nat.cast_zero Int.cast_zero pos_of_mul_pos_left MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono LT.lt.trans_le zero_lt_one LT.lt.trans Set.mem_symmDiff Real.HolderTriple.nonneg compl_beattySeq Set.notMem_compl_iff Set.mem_compl_iff or_not
compl_beattySeq 📖	mathematical	Real.HolderConjugate	Compl.compl Set Set.instCompl setOf beattySeq beattySeq'	—	Set.ext Set.not_disjoint_iff Real.HolderTriple.pos Real.HolderConjugate.symm
compl_beattySeq' 📖	mathematical	Real.HolderConjugate	Compl.compl Set Set.instCompl setOf beattySeq' beattySeq	—	compl_beattySeq Real.HolderConjugate.symm compl_compl

---

← Back to Index