The even continuous-layer limit at the lower source

The available source theory proves nonnegativity of every dimension-one layer, but does not yet prove summability of the lower even layers. Accordingly this module defines the unconditional limit honestly in ℝ≥0∞, as the supremum of the even partial sums. This allows the production depth to vary with the finite carrier: no fixed-depth diagonal argument is used.

noncomputable def MathlibNt.SieveTheory.suzukiEvenSourceLowerPartialSum (m : ℕ) (s : ℝ) : ℝ

The sum of the first m even dimension-one continuous source layers at β = 2.

Equations

• MathlibNt.SieveTheory.suzukiEvenSourceLowerPartialSum m s = ∑ k ∈ Finset.range m, MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1)) s

theorem MathlibNt.SieveTheory.suzukiEvenSourceLowerPartialSum_eq_finiteSourceLayer (m : ℕ) (s : ℝ) : suzukiEvenSourceLowerPartialSum m s = SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (2 * m) s

The explicit even partial sum is exactly the finite source layer at depth 2*m.

theorem MathlibNt.SieveTheory.suzukiLayer_one_two_even_nonneg {s : ℝ} (hs : 2 ≤ s) (k : ℕ) : 0 ≤ SuzukiFiniteContinuousLayers.suzukiLayer 1 2 (2 * (k + 1)) s

Every even layer is nonnegative on the lower parity domain s ≥ 2.

theorem MathlibNt.SieveTheory.suzukiEvenSourceLowerPartialSum_monotone {s : ℝ} (hs : 2 ≤ s) : Monotone fun (m : ℕ) => suzukiEvenSourceLowerPartialSum m s

The even lower-source partial sums increase with pair depth.

noncomputable def MathlibNt.SieveTheory.suzukiEvenSourceLowerLayerSup (s : ℝ) : ENNReal

The unconditional extended-real lower source-layer limit. The name records that this is a supremum; no finiteness or real summability assertion is hidden.

Equations

• MathlibNt.SieveTheory.suzukiEvenSourceLowerLayerSup s = ⨆ (m : ℕ), ENNReal.ofReal (MathlibNt.SieveTheory.suzukiEvenSourceLowerPartialSum m s)

theorem MathlibNt.SieveTheory.finiteSourceLayer_even_le_suzukiEvenSourceLowerLayerSup {s : ℝ} (m : ℕ) : ENNReal.ofReal (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (2 * m) s) ≤ suzukiEvenSourceLowerLayerSup s

Every finite even source layer, including one whose depth is chosen after inspecting arithmetic data, is controlled by the extended-real limit.

theorem MathlibNt.SieveTheory.finiteSourceLayer_adaptive_card_le_suzukiEvenSourceLowerLayerSup {α : Type u_1} {s : ℝ} (carrier : Finset α) : ENNReal.ofReal (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (2 * (carrier.card + 1)) s) ≤ suzukiEvenSourceLowerLayerSup s

Production-facing adaptive-depth bound. In particular, the pair depth may be the cardinality of a carrier plus one; it is not fixed before the data.

theorem MathlibNt.SieveTheory.finiteSourceLayer_supportedBelow_adaptive_le_suzukiEvenSourceLowerLayerSup (S : BoundingSieve) (z : ℕ) (s : ℝ) : ENNReal.ofReal (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (2 * ((SwitchingPrinciple.suzukiSupportedBelow S z).card + 1)) s) ≤ suzukiEvenSourceLowerLayerSup s

The exact adaptive depth used by the production lower-Rosser theorem is controlled by the same limit, uniformly in the sieve and cutoff.

theorem MathlibNt.SieveTheory.tendsto_suzukiEvenSourceLowerPartialSum_ofReal {s : ℝ} (hs : 2 ≤ s) : Filter.Tendsto (fun (m : ℕ) => ENNReal.ofReal (suzukiEvenSourceLowerPartialSum m s)) Filter.atTop (nhds (suzukiEvenSourceLowerLayerSup s))

Genuine monotone convergence of the even partial sums to their extended-real supremum. This theorem remains valid when the supremum is infinite.