theorem MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct_natCeil_eq (S : BoundingSieve) {x : ℝ} {z : ℕ} (hz : z = ⌈x⌉₊) : suzukiVProduct S ↑z = suzukiVProduct S x

theorem MathlibNt.SieveTheory.cube_carrier_bridge (Dnat p : ℕ) : Dnat ≤ p ^ 3 ↔ ↑Dnat ^ (1 / 3) ≤ ↑p

@[simp]

theorem MathlibNt.SieveTheory.suzukiYOne_two (D : ℝ) : SwitchingPrinciple.suzukiYOne D 2 = D ^ (1 / 3)

theorem MathlibNt.SieveTheory.suzukiVProduct_mul_localRatio_eq_sourceDiscreteEuler (S : BoundingSieve) {p : ℕ} {z : ℝ} (hpz : ↑p < z) : SwitchingPrinciple.suzukiVProduct S z * SwitchingPrinciple.suzukiLocalRatio S (↑p) z = sourceDiscreteEuler S p

theorem MathlibNt.SieveTheory.section14ExtendedV_one_eq_suzukiVOne (S : BoundingSieve) {Dnat znat : ℕ} {z s : ℝ} (hD : 1 < ↑Dnat) (hs : 1 ≤ s) (hz : z = ↑Dnat ^ (1 / s)) (hznat : znat = ⌈z⌉₊) : section14ExtendedV S 1 Dnat znat = SwitchingPrinciple.suzukiVOne S (↑Dnat) 2 z

theorem MathlibNt.SieveTheory.section14ExtendedV_one_normalized_eq_suzukiVOneNormalized (S : BoundingSieve) {Dnat znat : ℕ} {z s : ℝ} (hD : 1 < ↑Dnat) (hs : 1 ≤ s) (hz : z = ↑Dnat ^ (1 / s)) (hznat : znat = ⌈z⌉₊) : section14ExtendedV S 1 Dnat znat / SwitchingPrinciple.suzukiVProduct S z = SwitchingPrinciple.suzukiVOneNormalized S (↑Dnat) 2 z

theorem MathlibNt.SieveTheory.section14ExtendedV_one_le_of_suzukiVOne_le (S : BoundingSieve) {Dnat znat : ℕ} {z s E : ℝ} (hD : 1 < ↑Dnat) (hs : 1 ≤ s) (hz : z = ↑Dnat ^ (1 / s)) (hznat : znat = ⌈z⌉₊) (hbase : SwitchingPrinciple.suzukiVOne S (↑Dnat) 2 z ≤ E) : section14ExtendedV S 1 Dnat znat ≤ E