MathlibNt.Wu2004MeanValue.MovingIntegral

source

theorem Wu2004MeanValue.movingPerronIntegral_eq_integral {q : ℕ} (S V : Finset ℕ) (A B : ℕ → ℂ) (v : ℕ → ℕ) (x : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (σ T : ℝ) (hσ : 0 < σ) (hS : ∀ a ∈ S, 0 < a) (hV : ∀ n ∈ V, 0 < n) :

Exact finite-sum interchange and common-power factorization. The profile is shared across all characters; no modulus-dependent coefficients occur.

Inspect dependencies

Wu2004MeanValue.movingPerronIntegral_eq_integral · compiled type and proof/definition references.

source

noncomputable def Wu2004MeanValue.movingShortKernel {q : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (x m H A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (s : ℂ) :

ℂ

Equations

Wu2004MeanValue.movingShortKernel f v x m H A₁ A₂ k χ s = Wu2004MeanValue.movingG f v x m A₁ A₂ k χ s * AnalyticNumberTheory.LargeSieve.panShortF₁ m H χ s * ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep x) ^ s / s

Instances For

Inspect dependencies

Wu2004MeanValue.movingShortKernel · compiled type and proof/definition references.

source

noncomputable def Wu2004MeanValue.movingLongKernel {q : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (x m H A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (T : ℝ) (s : ℂ) :

ℂ

Equations

Wu2004MeanValue.movingLongKernel f v x m H A₁ A₂ k χ T s = Wu2004MeanValue.movingG f v x m A₁ A₂ k χ s * AnalyticNumberTheory.LargeSieve.ChenLiuCoprimeProducer.longF₂ m H T χ s * ↑(MathlibNt.SieveTheory.LiuWeight.liuPanPerronHalfStep x) ^ s / s

Instances For

Inspect dependencies

Wu2004MeanValue.movingLongKernel · compiled type and proof/definition references.

source

noncomputable def Wu2004MeanValue.movingShortIntegral {q : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (x m H A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (σ T : ℝ) :

ℂ

Equations

Wu2004MeanValue.movingShortIntegral f v x m H A₁ A₂ k χ σ T = (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, Wu2004MeanValue.movingShortKernel f v x m H A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t)

Instances For

Inspect dependencies

Wu2004MeanValue.movingShortIntegral · compiled type and proof/definition references.

source

noncomputable def Wu2004MeanValue.movingLongIntegral {q : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (x m H A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (σ T : ℝ) :

ℂ

Equations

Wu2004MeanValue.movingLongIntegral f v x m H A₁ A₂ k χ σ T = (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, Wu2004MeanValue.movingLongKernel f v x m H A₁ A₂ k χ T (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t)

Instances For

Inspect dependencies

Wu2004MeanValue.movingLongIntegral · compiled type and proof/definition references.

source

theorem Wu2004MeanValue.movingShortKernel_differentiableOn {q : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (x m H A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) :

DifferentiableOn ℂ (movingShortKernel f v x m H A₁ A₂ k χ) {s : ℂ | 0 < s.re}

Inspect dependencies

Wu2004MeanValue.movingShortKernel_differentiableOn · compiled type and proof/definition references.

source

theorem Wu2004MeanValue.movingShortKernel_line_continuous {q : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (x m H A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (σ : ℝ) (hσ : 0 < σ) :

Continuous fun (t : ℝ) => movingShortKernel f v x m H A₁ A₂ k χ (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t)

Inspect dependencies

Wu2004MeanValue.movingShortKernel_line_continuous · compiled type and proof/definition references.

source

theorem Wu2004MeanValue.movingLongKernel_line_continuous {q : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (x m H A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) (T σ : ℝ) (hσ : 0 < σ) :

Continuous fun (t : ℝ) => movingLongKernel f v x m H A₁ A₂ k χ T (MathlibNt.SieveTheory.LiuWeight.liuPanPerronLine σ t)

Inspect dependencies

Wu2004MeanValue.movingLongKernel_line_continuous · compiled type and proof/definition references.

source

theorem Wu2004MeanValue.moving_perron_eq_short_add_long {q : ℕ} (f : ℕ → ℂ) (v : ℕ → ℕ) (x m H A₁ A₂ k : ℕ) (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) {σ T : ℝ} (hσ : 0 < σ) (hH : H ≤ ⌊T⌋₊) :

movingPerronIntegral (Finset.Ioc (2 ^ k * A₁) (min (2 ^ (k + 1) * A₁) A₂)) (Finset.Icc 1 ⌊T⌋₊) (AnalyticNumberTheory.LargeSieve.panSourceG f m) (AnalyticNumberTheory.LargeSieve.panSourceD m) v χ σ T = movingShortIntegral f v x m H A₁ A₂ k χ σ T + movingLongIntegral f v x m H A₁ A₂ k χ σ T

Both finite prime polynomials are retained in the actual moving integral.

Inspect dependencies

Wu2004MeanValue.moving_perron_eq_short_add_long · compiled type and proof/definition references.