Lcm

📁 Source: PrimeNumberTheoremAnd/Lcm.lean

Statistics

Metric	Count
Definitions Criterion, L', M, m, mk', n, p, q, r, HighlyAbundant, L, X₀, σ, σnorm	14
Theorems L'_pos, L_eq_prod_q_mul_L', L_pos, Ln_div_M_gt, Ln_div_M_lt, M_lt, M_pos, h_crit, h_ord_1, h_ord_2, h_ord_3, hn, hp, hp_mono, hq, hq_mono, ln_eq, m_pos, not_highlyAbundant, not_highlyAbundant_1, not_highlyAbundant_2, p_gt_two, prod_p_le_prod_q, prod_q_dvd_L, prod_q_eq, q_gt_two, q_not_dvd_L', r_ge, r_le, val_p_L', val_p_M_ge_two, val_two_L', val_two_M_ge_L', σnorm_M_ge_σnorm_L'_mul, σnorm_ln_eq, L_eq_prod, L_not_HA_of_ge, exists_p_primes, exists_q_primes, final_comparison, hlog, hsqrt_ge, hε_pos, inv_cube_log_sqrt_le, inv_n_add_sqrt_ge, inv_n_pow_3_div_2_le, log_L_eq_psi, log_X₀_gt, log_X₀_pos, pq_ratio_ge, prod_epsilon_ge, prod_epsilon_le, prod_p_ge, prod_q_ge, psi_eq_prod	55
Total	69
⚠️ With sorry L_eq_prod, log_L_eq_psi, psi_eq_prod	3

Lcm

Definitions

Name	Category	Theorems
Criterion 📖	CompData	—
HighlyAbundant 📖	MathDef	4 math math: Criterion.not_highlyAbundant_2, Criterion.not_highlyAbundant, Criterion.not_highlyAbundant_1, L_not_HA_of_ge
L 📖	CompOp	13 math math: Criterion.Ln_div_M_lt, Criterion.not_highlyAbundant_2, Criterion.σnorm_ln_eq, Criterion.not_highlyAbundant, Criterion.L_eq_prod_q_mul_L', log_L_eq_psi, L_not_HA_of_ge, Criterion.L_pos, Criterion.M_lt, Criterion.prod_q_dvd_L, Criterion.ln_eq, Criterion.Ln_div_M_gt, L_eq_prod
X₀ 📖	CompOp	2 math math: log_X₀_pos, log_X₀_gt
σ 📖	CompOp	—
σnorm 📖	CompOp	2 math math: Criterion.σnorm_ln_eq, Criterion.σnorm_M_ge_σnorm_L'_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
L_eq_prod 📖 ⚠️	mathematical	—	L	—	—
L_not_HA_of_ge 📖	mathematical	—	HighlyAbundant L	—	Criterion.not_highlyAbundant
exists_p_primes 📖	—	X₀	—	—	hsqrt_ge hlog Dusart.proposition_5_4
exists_q_primes 📖	—	X₀	—	—	hsqrt_ge hlog Dusart.proposition_5_4
final_comparison 📖	—	—	—	—	—
hlog 📖	—	X₀	—	—	hsqrt_ge log_X₀_gt
hsqrt_ge 📖	—	X₀	—	—	—
hε_pos 📖	—	X₀	—	—	hlog
inv_cube_log_sqrt_le 📖	—	X₀	—	—	log_X₀_gt
inv_n_add_sqrt_ge 📖	—	X₀	—	—	—
inv_n_pow_3_div_2_le 📖	—	X₀	—	—	—
log_L_eq_psi 📖 ⚠️	mathematical	—	L	—	—
log_X₀_gt 📖	mathematical	—	X₀	—	—
log_X₀_pos 📖	mathematical	—	X₀	—	log_X₀_gt
pq_ratio_ge 📖	mathematical	X₀	exists_p_primes exists_q_primes	—	hε_pos exists_p_primes exists_q_primes
prod_epsilon_ge 📖	—	—	—	—	—
prod_epsilon_le 📖	—	—	—	—	—
prod_p_ge 📖	mathematical	X₀	exists_p_primes	—	exists_p_primes hlog
prod_q_ge 📖	mathematical	X₀	exists_q_primes	—	exists_q_primes hlog hε_pos
psi_eq_prod 📖 ⚠️	—	—	—	—	—

Lcm.Criterion

Definitions

Name	Category	Theorems
L' 📖	CompOp	9 math math: σnorm_ln_eq, val_two_M_ge_L', L_eq_prod_q_mul_L', L'_pos, val_two_L', q_not_dvd_L', val_p_L', σnorm_M_ge_σnorm_L'_mul, ln_eq
M 📖	CompOp	7 math math: Ln_div_M_lt, val_p_M_ge_two, val_two_M_ge_L', M_pos, M_lt, σnorm_M_ge_σnorm_L'_mul, Ln_div_M_gt
m 📖	CompOp	2 math math: prod_q_eq, m_pos
mk' 📖	CompOp	—
n 📖	CompOp	15 math math: Ln_div_M_lt, σnorm_ln_eq, not_highlyAbundant, L_eq_prod_q_mul_L', h_crit, h_ord_3, h_ord_1, hn, L_pos, val_two_L', M_lt, prod_q_dvd_L, σnorm_M_ge_σnorm_L'_mul, ln_eq, Ln_div_M_gt
p 📖	CompOp	13 math math: prod_q_eq, hp, p_gt_two, r_le, Ln_div_M_lt, val_p_M_ge_two, prod_p_le_prod_q, h_crit, hp_mono, h_ord_2, h_ord_1, val_p_L', σnorm_M_ge_σnorm_L'_mul
q 📖	CompOp	14 math math: prod_q_eq, hq, Ln_div_M_lt, q_gt_two, prod_p_le_prod_q, σnorm_ln_eq, L_eq_prod_q_mul_L', h_crit, h_ord_3, h_ord_2, hq_mono, q_not_dvd_L', prod_q_dvd_L, ln_eq
r 📖	CompOp	3 math math: prod_q_eq, r_le, r_ge

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
L'_pos 📖	mathematical	—	L'	—	L_pos prod_q_dvd_L hq
L_eq_prod_q_mul_L' 📖	mathematical	—	Lcm.L n q L'	—	L'.eq_1 prod_q_dvd_L
L_pos 📖	mathematical	—	Lcm.L n	—	—
Ln_div_M_gt 📖	mathematical	—	Lcm.L n M	—	M_pos M_lt
Ln_div_M_lt 📖	mathematical	—	Lcm.L n M p q	—	hq L_eq_prod_q_mul_L' L'_pos prod_q_eq hp m_pos prod_p_le_prod_q r_le
M_lt 📖	mathematical	—	M Lcm.L n	—	r_ge L'_pos prod_q_eq L_eq_prod_q_mul_L'
M_pos 📖	mathematical	—	M	—	hp m_pos L'_pos
h_crit 📖	mathematical	—	q p n	—	—
h_ord_1 📖	mathematical	—	n p	—	—
h_ord_2 📖	mathematical	—	p q	—	—
h_ord_3 📖	mathematical	—	q n	—	—
hn 📖	mathematical	—	n	—	—
hp 📖	mathematical	—	p	—	—
hp_mono 📖	mathematical	—	p	—	—
hq 📖	mathematical	—	q	—	—
hq_mono 📖	mathematical	—	q	—	—
ln_eq 📖	mathematical	—	Lcm.L n q L'	—	L'.eq_1 hq hq_mono h_ord_3
m_pos 📖	mathematical	—	m	—	prod_p_le_prod_q hp
not_highlyAbundant 📖	mathematical	—	Lcm.HighlyAbundant Lcm.L n	—	not_highlyAbundant_2 σnorm_M_ge_σnorm_L'_mul
not_highlyAbundant_1 📖	mathematical	Lcm.σnorm M p q Lcm.L n	Lcm.HighlyAbundant	—	M_pos L_pos Lcm.σnorm.eq_1 Lcm.σ.eq_1 hq prod_p_le_prod_q Ln_div_M_lt M_lt
not_highlyAbundant_2 📖	mathematical	Lcm.σnorm M L' p n	Lcm.HighlyAbundant Lcm.L	—	not_highlyAbundant_1 Lcm.σnorm.eq_1 Lcm.σ.eq_1 L'_pos hq prod_p_le_prod_q h_crit σnorm_ln_eq
p_gt_two 📖	mathematical	—	p	—	hp h_ord_1 h_ord_2 h_ord_3 hp_mono hq_mono
prod_p_le_prod_q 📖	mathematical	—	p q	—	h_crit hq
prod_q_dvd_L 📖	mathematical	—	q Lcm.L n	—	hq hq_mono h_ord_3
prod_q_eq 📖	mathematical	—	q p m r	—	—
q_gt_two 📖	mathematical	—	q	—	h_ord_2 hq_mono
q_not_dvd_L' 📖	mathematical	—	q L'	—	h_ord_1 hp_mono h_ord_2 hq_mono hq ln_eq
r_ge 📖	mathematical	—	r	—	hp hq h_ord_2 hq_mono
r_le 📖	mathematical	—	r p	—	hp
val_p_L' 📖	mathematical	—	L' p	—	hp h_ord_1 hp_mono h_ord_2 h_ord_3 hq_mono L'_pos hq L_eq_prod_q_mul_L'
val_p_M_ge_two 📖	mathematical	—	M p	—	hp m_pos L'_pos val_p_L'
val_two_L' 📖	mathematical	—	L' n	—	prod_q_dvd_L hn hq q_gt_two
val_two_M_ge_L' 📖	mathematical	—	M L'	—	hp m_pos L'_pos
σnorm_M_ge_σnorm_L'_mul 📖	mathematical	—	Lcm.σnorm M L' p n	—	M_pos L'_pos M.eq_1 val_p_L' val_two_M_ge_L' hn val_two_L' hp p_gt_two hp_mono
σnorm_ln_eq 📖	mathematical	—	Lcm.σnorm Lcm.L n L' q	—	hq hq_mono q_not_dvd_L' L_eq_prod_q_mul_L' L'_pos

---

← Back to Index