Documentation

MathlibNt.AnalyticNumberTheory.Chen1973.Chen1973Lemma6Equation20BetaIntegral

source
theorem AnalyticNumberTheory.LargeSieve.eq20_log_height {T : ℝ} (hT : 1 ≤ T) :
1 + Real.log T ≤ 2 * √T

Height extraction preserves the conductor logarithm.

source
theorem AnalyticNumberTheory.LargeSieve.eq20_derivative_height_algebra (Q a r W D v : ℝ) (hQ : 1 ≤ Q) (ha : 0 ≤ a) (hr : 0 ≤ r) (hW : 0 ≤ W) (hD : 0 ≤ D) :
W * (21000000 * Q ^ 2 * (a + |v| + r) ^ 2 * (1 + Real.log (Q * (1 + (a + |v| + r)))) ^ 4 / D / r ^ 4) ≤ 16 * 21000000 * W * Q ^ 2 * (1 + a + r) ^ 2 * (1 + Real.log (Q * (1 + (1 + a + r)))) ^ 4 / (D * r ^ 4) * (1 + |v|) ^ 4
source
noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20BetaDerivativeCoefficient (x L level D Q : ℕ) :
ℝ
Equations
Instances For
    source
    noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20BetaLinearCoefficient (x L level B k H D Q : ℕ) :
    ℝ
    Equations
    Instances For
      source
      theorem AnalyticNumberTheory.LargeSieve.eq20_fourth_root_height {G T : ℝ} (hG : 0 ≤ G) (hT : 0 ≤ T) :
      √√(G * T ^ 4) = √√G * T
      source
      theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6B_eq20_beta_linear (x L level B k m H D Q : ℕ) (hx : 3 ≤ x) (hB : 0 < B) (hD : 0 < D) (hQ : 2 ≤ Q) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) (v : ℝ) :
      chen1973Lemma6B x L level B k m H (↑(chen1973Lemma6Beta x) + ↑v * Complex.I) ≤ chen1973Lemma6Eq20BetaLinearCoefficient x L level B k H D Q * (1 + |v|)

      Actual beta numerator, uniformly linear in height, with the S²/pair⁴/L'⁴ allocation.

      source
      theorem AnalyticNumberTheory.LargeSieve.eq20_radial_factor_quadratic {u z : ℝ} {N : ℕ} (hz : 0 ≤ z) (hzu : z ≤ u) (hN : 2 ≤ N) :
      (1 + u ^ N)⁻¹ ≤ 2 / (1 + z ^ 2)

      A scale-preserving quadratic comparison: no log(x)^(231/100) payment.

      source
      theorem AnalyticNumberTheory.LargeSieve.eq20_linear_over_corrected_kernel {x : ℕ} (hx : 3 ≤ x) {σ v : ℝ} (hσ : 1 / 2 ≤ σ) (hv : 0 ≤ v) :
      (1 + v) / chen1973Lemma6Eq17CorrectedKernel x (↑σ + ↑v * Complex.I) ≤ 6 * (1 + (v / chen1973PerronScale ↑x) ^ 2)⁻¹

      The literal radial |s| pays the linear height before scaling the integral.

      source
      theorem AnalyticNumberTheory.LargeSieve.eq20_scaled_cauchy_integrable {A : ℝ} (hA : 0 < A) :
      MeasureTheory.IntegrableOn (fun (v : ℝ) => (1 + (v / A) ^ 2)⁻¹) (Set.Ioi 0) MeasureTheory.volume
      source
      theorem AnalyticNumberTheory.LargeSieve.eq20_scaled_cauchy_integral {A : ℝ} (hA : 0 < A) :
      ∫ (v : ℝ) in Set.Ioi 0, (1 + (v / A) ^ 2)⁻¹ = A * (Real.pi / 2)
      source
      theorem AnalyticNumberTheory.LargeSieve.eq20_corrected_linear_integrable_and_bound {x : ℕ} (hx : 3 ≤ x) {σ K : ℝ} (hσ : 1 / 2 ≤ σ) (hK : 0 ≤ K) (F : ℝ → ℝ) (hcont : Continuous F) (hF0 : ∀ v ∈ Set.Ioi 0, 0 ≤ F v) (hFK : ∀ v ∈ Set.Ioi 0, F v ≤ K * (1 + v)) :
      MeasureTheory.IntegrableOn (fun (v : ℝ) => F v / chen1973Lemma6Eq17CorrectedKernel x (↑σ + ↑v * Complex.I)) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (v : ℝ) in Set.Ioi 0, F v / chen1973Lemma6Eq17CorrectedKernel x (↑σ + ↑v * Complex.I) ≤ 3 * Real.pi * chen1973PerronScale ↑x * K

      A genuine integral theorem for the unchanged corrected kernel, preserving A=(log x)^(11/10). This generic analytic helper is consumed below by the actual three-moment producer and an internally proved continuity theorem.

      source
      theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6B_eq20_beta_continuous {x L level B k m H D Q : ℕ} (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) :
      Continuous fun (v : ℝ) => chen1973Lemma6B x L level B k m H (↑(chen1973Lemma6Beta x) + ↑v * Complex.I)

      Continuity of the actual beta numerator; primitive conductors exceed one.

      source
      noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq20BetaIntegralBudget (x L level B k H D Q : ℕ) :
      ℝ

      Explicit beta half-line budget with only one Perron scale, not a spurious x normalization or a conductor-polynomial replacement of the logarithm.

      Equations
      Instances For
        source
        theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_beta_integrable_and_budget (x L level B k m H D Q : ℕ) (hx : 3 ≤ x) (hB : 0 < B) (hD : 0 < D) (hQ : 2 ≤ Q) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) :
        MeasureTheory.IntegrableOn (fun (v : ℝ) => chen1973Lemma6B x L level B k m H (↑(chen1973Lemma6Beta x) + ↑v * Complex.I) / chen1973Lemma6Eq17CorrectedKernel x (↑(chen1973Lemma6Beta x) + ↑v * Complex.I)) (Set.Ioi 0) MeasureTheory.volume ∧ chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m H ≤ chen1973Lemma6Eq20BetaIntegralBudget x L level B k H D Q

        The new three moments are wired to the literal corrected beta integral. No integrability, continuity, growth, scalar payment, or order hypothesis is supplied by the caller. H is arbitrary, including zero.

        source
        theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq20_beta_contribution_budget (x L level B k m H D Q : ℕ) (hx : 3 ≤ x) (hB : 0 < B) (hD : 0 < D) (hQ : 2 ≤ Q) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) :
        2 * ↑x ^ (1 / 2) * chen1973Lemma6Eq20CorrectedSecondIntegral x L level B k m H ≤ 6 * Real.pi * ↑x ^ (1 / 2) * Real.log ↑x ^ (11 / 10) * chen1973Lemma6Eq20BetaLinearCoefficient x L level B k H D Q

        The exact beta contribution in corrected (17)/(20), including its outer 2 sqrt x; no extra factor sqrt x is introduced.