Documentation Verification Report

CH2

📁 Source: PrimeNumberTheoremAnd/CH2.lean

Statistics

Metric	Count
Definitions `F`, `I'`, `Phi_circ`, `Phi_star`, `S`, `coth`, `ϕ`, `ϕ_pm`	8
Theorems `minus_l1`, `minus_minorizes_I`, `plus_l1`, `plus_majorizes_I`, `real`, `F_integrable`, `I_prime_integrable`, `I_prime_integral`, `Phi_circ_neg_conj`, `Phi_star_neg_conj`, `S_eq_I`, `cor_1_2_a`, `cor_1_2_b`, `cor_1_3_a`, `cor_1_3_b`, `integral_F_eq_phi_zero`, `phi_zero_val`, `prop_2_3`, `prop_2_3_1`, `prop_2_4_minus`, `prop_2_4_plus`, `ϕ_continuous`, `ϕ_deriv_bv`, `ϕ_integrable`	24
Total	32
⚠️ With sorry `minus_l1`, `minus_minorizes_I`, `plus_majorizes_I`, `S_eq_I`, `cor_1_2_a`, `cor_1_2_b`, `cor_1_3_a`, `cor_1_3_b`, `prop_2_3`, `prop_2_3_1`, `prop_2_4_minus`, `prop_2_4_plus`, `ϕ_continuous`, `ϕ_deriv_bv`	14

CH2

Definitions

Name	Category	Theorems
`F` 📖	CompOp	6 math math: `F_integrable`, `F.minus_minorizes_I`, `F.plus_majorizes_I`, `F.minus_l1`, `F.plus_l1`, `integral_F_eq_phi_zero`
`I'` 📖	CompOp	7 math math: `I_prime_integrable`, `S_eq_I`, `F.minus_minorizes_I`, `F.plus_majorizes_I`, `I_prime_integral`, `F.minus_l1`, `F.plus_l1`
`Phi_circ` 📖	CompOp	1 math math: `Phi_circ_neg_conj`
`Phi_star` 📖	CompOp	1 math math: `Phi_star_neg_conj`
`S` 📖	CompOp	3 math math: `S_eq_I`, `prop_2_4_minus`, `prop_2_4_plus`
`coth` 📖	CompOp	1 math math: `cor_1_2_a`
`ϕ` 📖	CompOp	6 math math: `ϕ_deriv_bv`, `ϕ_integrable`, `phi_zero_val`, `F.real`, `ϕ_continuous`, `integral_F_eq_phi_zero`
`ϕ_pm` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`F_integrable` 📖	mathematical	—	`F`	—	`ϕ_integrable` `decay_alt` `ϕ_continuous` `ϕ_deriv_bv`
`I_prime_integrable` 📖	mathematical	—	`I'`	—	`I_prime_integral`
`I_prime_integral` 📖	mathematical	—	`I'`	—	—
`Phi_circ_neg_conj` 📖	mathematical	—	`Phi_circ`	—	—
`Phi_star_neg_conj` 📖	mathematical	—	`Phi_star`	—	—
`S_eq_I` 📖 ⚠️	mathematical	—	`S` `I'`	—	—
`cor_1_2_a` 📖 ⚠️	mathematical	—	`coth`	—	—
`cor_1_2_b` 📖 ⚠️	—	—	—	—	—
`cor_1_3_a` 📖 ⚠️	—	—	—	—	—
`cor_1_3_b` 📖 ⚠️	—	—	—	—	—
`integral_F_eq_phi_zero` 📖	mathematical	—	`F` `ϕ`	—	`ϕ_continuous` `ϕ_deriv_bv` `ϕ_integrable` `F_integrable` `F.real`
`phi_zero_val` 📖	mathematical	—	`ϕ`	—	—
`prop_2_3` 📖 ⚠️	—	—	—	—	—
`prop_2_3_1` 📖 ⚠️	—	—	—	—	—
`prop_2_4_minus` 📖 ⚠️	mathematical	`I'`	`S`	—	—
`prop_2_4_plus` 📖 ⚠️	mathematical	`I'`	`S`	—	—
`ϕ_continuous` 📖 ⚠️	mathematical	—	`AbsolutelyContinuous` `ϕ`	—	—
`ϕ_deriv_bv` 📖 ⚠️	mathematical	—	`ϕ`	—	—
`ϕ_integrable` 📖	mathematical	—	`ϕ`	—	—

CH2.F

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`minus_l1` 📖 ⚠️	mathematical	—	`CH2.I'` `CH2.F`	—	—
`minus_minorizes_I` 📖 ⚠️	mathematical	—	`CH2.F` `CH2.I'`	—	—
`plus_l1` 📖	mathematical	—	`CH2.F` `CH2.I'`	—	`CH2.F_integrable` `CH2.I_prime_integrable` `CH2.integral_F_eq_phi_zero` `CH2.I_prime_integral` `CH2.phi_zero_val`
`plus_majorizes_I` 📖 ⚠️	mathematical	—	`CH2.F` `CH2.I'`	—	—
`real` 📖	mathematical	—	`CH2.ϕ`	—	—

---

← Back to Index