noncomputable def MathlibNt.SieveTheory.suzukiSupportedBelowPowerReal (S : BoundingSieve) (x : ℝ) : Finset ℕ

The supported prime carrier cut out by a strict real cutoff.

Equations

• MathlibNt.SieveTheory.suzukiSupportedBelowPowerReal S x = {p ∈ S.prodPrimes.primeFactors | ↑p < x}

noncomputable def MathlibNt.SieveTheory.suzukiSourceOuterCarrierPowerReal (n D : ℕ) (x : ℝ) (P : Finset ℕ) : Finset ℕ

The source outer carrier with its strict upper cutoff expressed in ℝ.

Equations

• MathlibNt.SieveTheory.suzukiSourceOuterCarrierPowerReal n D x P = {p ∈ {p ∈ P | ↑p < x} | D ≤ p ^ (n + 2) ∧ (Odd n → p ^ 3 < D)}

theorem MathlibNt.SieveTheory.nat_lt_natCeil_iff_lt_real {x : ℝ} {z p : ℕ} (_hx : 0 < x) (hz : z = ⌈x⌉₊) : p < z ↔ ↑p < x

Naturals below a positive real cutoff are exactly naturals below its natural ceiling. The positivity hypothesis records the power-cutoff use case.

theorem MathlibNt.SieveTheory.suzukiSupportedBelow_natCeil_eq_powerReal (S : BoundingSieve) {x : ℝ} {z : ℕ} (hx : 0 < x) (hz : z = ⌈x⌉₊) : SwitchingPrinciple.suzukiSupportedBelow S z = suzukiSupportedBelowPowerReal S x

Exact carrier transport from an arbitrary positive real cutoff to its natural ceiling.

theorem MathlibNt.SieveTheory.suzukiSupportedBelow_filter_natCeil_eq_powerReal (S : BoundingSieve) (P : ℕ → Prop) [DecidablePred P] {x : ℝ} {z : ℕ} (hx : 0 < x) (hz : z = ⌈x⌉₊) : Finset.filter P (SwitchingPrinciple.suzukiSupportedBelow S z) = Finset.filter P (suzukiSupportedBelowPowerReal S x)

Carrier transport remains exact after any additional recurrence filter.

theorem MathlibNt.SieveTheory.suzukiSourceBaseCarrier_natCeil_eq_powerReal (S : BoundingSieve) (D : ℕ) {x : ℝ} {z : ℕ} (hx : 0 < x) (hz : z = ⌈x⌉₊) : {p ∈ SwitchingPrinciple.suzukiSupportedBelow S z | D ≤ p ^ 3} = {p ∈ suzukiSupportedBelowPowerReal S x | D ≤ p ^ 3}

In particular, the terminal filter in the base source layer is unchanged.

theorem MathlibNt.SieveTheory.suzukiSourceOuterCarrier_natCeil_eq_powerReal (n D : ℕ) (P : Finset ℕ) {x : ℝ} {z : ℕ} (hx : 0 < x) (hz : z = ⌈x⌉₊) : suzukiSourceOuterCarrier n D z P = suzukiSourceOuterCarrierPowerReal n D x P

The complete source-recurrence outer carrier is unchanged by replacing a positive real cutoff by its natural ceiling.

theorem MathlibNt.SieveTheory.suzukiSourceV_succ_natCeil_eq_powerReal (S : BoundingSieve) {n D z : ℕ} {x : ℝ} (hn : 0 < n) (hx : 0 < x) (hz : z = ⌈x⌉₊) : suzukiSourceV S (n + 1) D z = ∑ p ∈ suzukiSourceOuterCarrierPowerReal (n + 1) D x S.prodPrimes.primeFactors, S.nu p * suzukiSourceV S n (D ⌈/⌉ p) p

Exact successor recurrence with an arbitrary positive real power cutoff.

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

Suzuki's finite Euler product is literally invariant under natural-ceiling transport of any positive real cutoff.

theorem MathlibNt.SieveTheory.suzukiSuffixCarrier_natCeil_eq_power (S : BoundingSieve) (p : ℕ) {x : ℝ} {z : ℕ} (hx : 0 < x) (hz : z = ⌈x⌉₊) : {q ∈ S.prodPrimes.primeFactors | p ≤ q ∧ ↑q < ↑z} = {q ∈ S.prodPrimes.primeFactors | p ≤ q ∧ ↑q < x}

Every Euler suffix carrier is exactly invariant under natural-ceiling transport.

theorem MathlibNt.SieveTheory.suzukiSuffixProduct_natCeil_eq_power (S : BoundingSieve) (p : ℕ) {x : ℝ} {z : ℕ} (hx : 0 < x) (hz : z = ⌈x⌉₊) : ∏ q ∈ S.prodPrimes.primeFactors with p ≤ q ∧ ↑q < ↑z, (1 - S.nu q)⁻¹ = ∏ q ∈ S.prodPrimes.primeFactors with p ≤ q ∧ ↑q < x, (1 - S.nu q)⁻¹

Consequently every inverse Euler suffix product is exactly invariant.

theorem MathlibNt.SieveTheory.natCast_rpow_one_div_pos {D : ℕ} (hD : 0 < D) (s : ℝ) : 0 < ↑D ^ (1 / s)

A positive natural base has a positive real 1/s power cutoff, for every real power parameter s.

theorem MathlibNt.SieveTheory.suzukiSupportedBelow_natCeil_rpow_eq (S : BoundingSieve) {D z : ℕ} {s : ℝ} (hD : 0 < D) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : SwitchingPrinciple.suzukiSupportedBelow S z = suzukiSupportedBelowPowerReal S (↑D ^ (1 / s))

Convenient exact supported-carrier specialization to D^(1/s).

theorem MathlibNt.SieveTheory.suzukiVProduct_natCeil_rpow_eq (S : BoundingSieve) {D z : ℕ} {s : ℝ} (hD : 0 < D) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : SwitchingPrinciple.suzukiVProduct S ↑z = SwitchingPrinciple.suzukiVProduct S (↑D ^ (1 / s))

Convenient exact Euler-product specialization to D^(1/s).

theorem MathlibNt.SieveTheory.suzukiSourceV_succ_natCeil_rpow_eq (S : BoundingSieve) {n D z : ℕ} {s : ℝ} (hn : 0 < n) (hD : 0 < D) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : suzukiSourceV S (n + 1) D z = ∑ p ∈ suzukiSourceOuterCarrierPowerReal (n + 1) D (↑D ^ (1 / s)) S.prodPrimes.primeFactors, S.nu p * suzukiSourceV S n (D ⌈/⌉ p) p

Convenient exact source-successor recurrence specialization to D^(1/s).

theorem MathlibNt.SieveTheory.suzukiSuffixProduct_natCeil_rpow_eq (S : BoundingSieve) (p : ℕ) {D z : ℕ} {s : ℝ} (hD : 0 < D) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : ∏ q ∈ S.prodPrimes.primeFactors with p ≤ q ∧ ↑q < ↑z, (1 - S.nu q)⁻¹ = ∏ q ∈ S.prodPrimes.primeFactors with p ≤ q ∧ ↑q < ↑D ^ (1 / s), (1 - S.nu q)⁻¹

Convenient exact inverse-suffix specialization to D^(1/s).

theorem MathlibNt.SieveTheory.rpow_one_div_mono_of_le {D s t : ℝ} (hD : 1 ≤ D) (hs : 0 < s) (hst : s ≤ t) : D ^ (1 / t) ≤ D ^ (1 / s)

For a base at least one, decreasing the positive power parameter increases D^(1/s).

theorem MathlibNt.SieveTheory.natCeil_rpow_one_div_mono_of_le {D s t : ℝ} (hD : 1 ≤ D) (hs : 0 < s) (hst : s ≤ t) : ⌈D ^ (1 / t)⌉₊ ≤ ⌈D ^ (1 / s)⌉₊

Natural ceilings preserve the preceding power-cutoff order.

theorem MathlibNt.SieveTheory.natCeil_cuberoot_le_natCeil_power {D s : ℝ} (hD : 1 ≤ D) (hs : 0 < s) (hs3 : s ≤ 3) : ⌈D ^ (1 / 3)⌉₊ ≤ ⌈D ^ (1 / s)⌉₊

The cubic natural cutoff lies below every s-power natural cutoff with 0 < s ≤ 3.

theorem MathlibNt.SieveTheory.caseII_hyz_of_natCeil_powerCutoffs {D : ℕ} {s : ℝ} {y z : ℕ} (hD : 1 ≤ D) (hs : 0 < s) (hs3 : s ≤ 3) (hy : y = ⌈↑D ^ (1 / 3)⌉₊) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : y ≤ z

Named y ≤ z bridge used by the cubic/source Case-II assembly.

theorem MathlibNt.SieveTheory.supported_cube_lt_of_eq_natCeil_cuberoot (S : BoundingSieve) {D y : ℕ} (hD : 0 < D) (hy : y = ⌈↑D ^ (1 / 3)⌉₊) (p : ℕ) : p ∈ SwitchingPrinciple.suzukiSupportedBelow S y → p ^ 3 < D

Every supported prime below the cubic natural ceiling satisfies Suzuki's strict cubic source cutoff.

theorem MathlibNt.SieveTheory.cubicSupport_and_caseII_hyz_of_natCeil_powerCutoffs (S : BoundingSieve) {D : ℕ} {s : ℝ} {y z : ℕ} (hD : 1 ≤ D) (hs : 0 < s) (hs3 : s ≤ 3) (hy : y = ⌈↑D ^ (1 / 3)⌉₊) (hz : z = ⌈↑D ^ (1 / s)⌉₊) : (∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S y, p ^ 3 < D) ∧ y ≤ z

One packet supplies both Case-II cutoff obligations: cubic support at y and the natural-cutoff order y ≤ z.