StoppingProductSlice.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact product slices for the original finite support. Divisibility supplies the norm bound needed by the stopping construction.

def OAI.CubicFirstMoment.primaryProductSlice line 13
lemma OAI.CubicFirstMoment.mem_primaryProductSlice_iff line 17
lemma OAI.CubicFirstMoment.primaryProductSlice_support line 30
theorem OAI.CubicFirstMoment.roughProduct_slice_pairs line 41
Source documentation
Reindex the literal rough-product divisor expansion with the complementary factor first. No condition is imposed on the kernel.
```
theorem roughProduct_slice_pairs (S : Finset Eisenstein) (X : ℝ)
    (hS : ∀ n ∈ S, primary n ∧ Squarefree n ∧ norm n ≤ X)
    (r : Eisenstein) (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    (∑ n ∈ primaryProductSlice S X r, (roughProduct ψ w n:ℂ)*K (r*n)) =
      ∑ u ∈ primaryElementBall X, ∑ m ∈ primaryProductSlice S X (r*u),
        cutoffMoebius ψ w m*K (r*(m*u)) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryProductSlice, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.cutoffMoebius

theorem OAI.CubicFirstMoment.stopping_product_slice_split line 63

Source documentation

A fixed complementary-factor row has an exact no-stop and stopped split. The only support predicate on the collected pair is the original total product membership.

theorem stopping_product_slice_split (S : Finset Eisenstein)
    {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2) (hX : 1 ≤ X)
    (hS : ∀ n ∈ S, primary n ∧ Squarefree n ∧ norm n ≤ X)
    {r : Eisenstein} (hr : primary r) (u : Eisenstein)
    {Z : ℝ} (hstart : norm r < Z)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    (∑ m ∈ primaryProductSlice S X (r*u), cutoffMoebius ψ w m*K (r*(m*u))) =
      (∑ m ∈ primaryProductSlice S X (r*u) with
          norm r*primeSurrogate (primaryPrimeFactors m)
            (geometricPrimeBin ρ X) (geometricBinLower ρ X) < Z,
        cutoffMoebius ψ w m*K (r*(m*u))) +
      ∑ q ∈ stoppingLabelBox ρ X, (Nat.choose (q.2.1+q.2.2) q.2.1:ℂ)⁻¹ *
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryProductSlice, OAI.CubicFirstMoment.cutoffMoebius, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower, OAI.CubicFirstMoment.stoppingLabelBox

theorem OAI.CubicFirstMoment.roughProduct_slice_stopping line 100

Source documentation

The genuine rough product on one distinguished row, with the un-stopped term retained explicitly.

theorem roughProduct_slice_stopping (S : Finset Eisenstein)
    {ρ X : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2) (hX : 1 ≤ X)
    (hS : ∀ n ∈ S, primary n ∧ Squarefree n ∧ norm n ≤ X)
    {r : Eisenstein} (hr : primary r) {Z : ℝ} (hstart : norm r < Z)
    (ψ : ℝ → ℝ) (w : ℝ) (K : Eisenstein → ℂ) :
    (∑ n ∈ primaryProductSlice S X r, (roughProduct ψ w n:ℂ)*K (r*n)) =
      (∑ u ∈ primaryElementBall X,
        ∑ m ∈ primaryProductSlice S X (r*u) with
          norm r*primeSurrogate (primaryPrimeFactors m)
            (geometricPrimeBin ρ X) (geometricBinLower ρ X) < Z,
          cutoffMoebius ψ w m*K (r*(m*u))) +
      ∑ q ∈ stoppingLabelBox ρ X, (Nat.choose (q.2.1+q.2.2) q.2.1:ℂ)⁻¹ *
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryProductSlice, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower, OAI.CubicFirstMoment.cutoffMoebius, OAI.CubicFirstMoment.stoppingLabelBox