OAI/NumberTheory/JointDickman/Counting/ShortIntervalConsequences.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Finite interpolation and the published real short-interval input

The multiplicative interpolants used for a centered label have separate short-average errors. Cauchy–Schwarz combines these errors; the input is explicitly the published RealShortIntervalInput.

  1. theorem OAI.JointDickman.PublishedInputs.measurable_realShortAverage line 21
  2. theorem OAI.JointDickman.PublishedInputs.abs_realShortAverage_le line 28
  3. theorem OAI.JointDickman.PublishedInputs.realShortAverage_sub_sq_integrable line 44
  4. def OAI.JointDickman.PublishedInputs.centeredCombination line 58

    Source documentation

    The centered linear combination appearing after interpolation.

    noncomputable def centeredCombination {ι : Type*} (s : Finset ι)
    (c : ι → ℝ) (f : ι → ArithmeticFunction ℝ) (H X z : ℝ) : ℝ :=
…
  5. def OAI.JointDickman.PublishedInputs.shortCombination line 63

    Source documentation

    The uncentered interpolated short average.

    noncomputable def shortCombination {ι : Type*} (s : Finset ι)
    (c : ι → ℝ) (f : ι → ArithmeticFunction ℝ) (H z : ℝ) : ℝ :=
…
  6. def OAI.JointDickman.PublishedInputs.longCombination line 68

    Source documentation

    Its combined long mean. Individual means need not vanish.

    noncomputable def longCombination {ι : Type*} (s : Finset ι)
    (c : ι → ℝ) (f : ι → ArithmeticFunction ℝ) (X : ℝ) : ℝ :=
…
  7. theorem OAI.JointDickman.PublishedInputs.shortCombination_eq_centered_add_long line 72
  8. theorem OAI.JointDickman.PublishedInputs.centeredCombination_sq_le line 80
  9. theorem OAI.JointDickman.PublishedInputs.measurable_centeredCombination line 88
  10. theorem OAI.JointDickman.PublishedInputs.centeredCombination_sq_integrable line 94
  11. theorem OAI.JointDickman.PublishedInputs.real_input_finite_combination_bound line 117

    Source documentation

    Finite linear interpolation preserves the uniform mean-square estimate. The same witness r works for every fixed finite family.

    theorem real_input_finite_combination_bound (hMR : RealShortIntervalInput) :
    ∃ r : ℝ → ℝ, Tendsto r atTop (𝓝 0) ∧
      ∀ {ι : Type*} (s : Finset ι) (c : ι → ℝ) (f : ι → ArithmeticFunction ℝ),
      (∀ i ∈ s, (f i).IsMultiplicative) →
      (∀ i ∈ s, ∀ n : ℕ, |f i n| ≤ 1) →
      ∀ H X : ℝ, 2 ≤ H → H ≤ X →
        (1 / X) * (∫ z in X..2 * X, (centeredCombination s c f H X z) ^ 2) ≤
          (∑ i ∈ s, c i ^ 2) * (s.card : ℝ) * r H := by
…

    Mentions: OAI.JointDickman.PublishedInputs.RealShortIntervalInput, OAI.JointDickman.PublishedInputs.centeredCombination

  12. theorem OAI.JointDickman.PublishedInputs.centeredCombination_tendsto_zero line 165

    Source documentation

    A fixed finite number of multiplicative interpolants has vanishing combined centered short-average energy as the length tends to infinity. The functions themselves may vary with the scale, as the paper's bin interpolants do.

    theorem centeredCombination_tendsto_zero (hMR : RealShortIntervalInput)
    {ι : Type*} (s : Finset ι) (c : ι → ℝ) (f : ℕ → ι → ArithmeticFunction ℝ)
    (hmult : ∀ k, ∀ i ∈ s, (f k i).IsMultiplicative)
    (hf : ∀ k, ∀ i ∈ s, ∀ n : ℕ, |f k i n| ≤ 1)
    (H X : ℕ → ℝ) (hH : Tendsto H atTop atTop)
    (hHX : ∀ᶠ n in atTop, H n ≤ X n) :
    Tendsto (fun n => (1 / X n) *
      (∫ z in X n..2 * X n, (centeredCombination s c (f n) (H n) (X n) z) ^ 2))
      atTop (𝓝 0) := by
…

    Mentions: OAI.JointDickman.PublishedInputs.RealShortIntervalInput, OAI.JointDickman.PublishedInputs.centeredCombination

  13. theorem OAI.JointDickman.PublishedInputs.meanSquare_add_const_le line 189
  14. theorem OAI.JointDickman.PublishedInputs.shortCombination_tendsto_zero line 214

    Source documentation

    The application needed after interpolating a centered label: only the combined long mean must vanish; its individual multiplicative summands may have nonzero long means.

    theorem shortCombination_tendsto_zero (hMR : RealShortIntervalInput)
    {ι : Type*} (s : Finset ι) (c : ι → ℝ) (f : ℕ → ι → ArithmeticFunction ℝ)
    (hmult : ∀ k, ∀ i ∈ s, (f k i).IsMultiplicative)
    (hf : ∀ k, ∀ i ∈ s, ∀ n : ℕ, |f k i n| ≤ 1)
    (H X : ℕ → ℝ) (hH : Tendsto H atTop atTop)
    (hHX : ∀ᶠ n in atTop, H n ≤ X n)
    (hlong : Tendsto (fun n => longCombination s c (f n) (X n)) atTop (𝓝 0)) :
    Tendsto (fun n => (1 / X n) *
      (∫ z in X n..2 * X n, (shortCombination s c (f n) (H n) z) ^ 2))
      atTop (𝓝 0) := by
…

    Mentions: OAI.JointDickman.PublishedInputs.RealShortIntervalInput, OAI.JointDickman.PublishedInputs.longCombination, OAI.JointDickman.PublishedInputs.shortCombination

  15. theorem OAI.JointDickman.PublishedInputs.shortCombination_eventually_eventually line 249

    Source documentation

    The iterated-limit form used when the short length is fixed in the inner scale limit. This is the principal-character part of labels-short.

    theorem shortCombination_eventually_eventually (hMR : RealShortIntervalInput)
    {ι : Type*} (s : Finset ι) (c : ι → ℝ)
    (f : ℕ → ℕ → ι → ArithmeticFunction ℝ)
    (hmult : ∀ B n, ∀ i ∈ s, (f B n i).IsMultiplicative)
    (hf : ∀ B n, ∀ i ∈ s, ∀ k : ℕ, |f B n i k| ≤ 1)
    (H : ℕ → ℝ) (X : ℕ → ℕ → ℝ) (hH : Tendsto H atTop atTop)
    (hHX : ∀ B, ∀ᶠ n in atTop, H B ≤ X B n)
    (hlong : ∀ B, Tendsto (fun n => longCombination s c (f B n) (X B n))
      atTop (𝓝 0)) :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ B in atTop, ∀ᶠ n in atTop,
      (1 / X B n) * (∫ z in X B n..2 * X B n,
        (shortCombination s c (f B n) (H B) z) ^ 2) < ε := by
…

    Mentions: OAI.JointDickman.PublishedInputs.RealShortIntervalInput, OAI.JointDickman.PublishedInputs.longCombination, OAI.JointDickman.PublishedInputs.shortCombination

  16. theorem OAI.JointDickman.PublishedInputs.shortCombination_sq_integrable line 283
  17. def OAI.JointDickman.PublishedInputs.complexShortCombination line 305

    Source documentation

    The coefficients in the manuscript's real multiplicative interpolation are complex, even for the principal-character term.

    noncomputable def complexShortCombination {ι : Type*} (s : Finset ι)
    (c : ι → ℂ) (f : ι → ArithmeticFunction ℝ) (H z : ℝ) : ℂ :=
…
  18. def OAI.JointDickman.PublishedInputs.complexLongCombination line 309
  19. theorem OAI.JointDickman.PublishedInputs.complexShortCombination_norm_sq line 313
  20. theorem OAI.JointDickman.PublishedInputs.complexShortCombination_energy line 322
  21. theorem OAI.JointDickman.PublishedInputs.complexShortCombination_eventually_eventually line 337

    Source documentation

    Complex coefficients require no complex multiplicative input for the principal-character part: apply the real input to both coefficient parts.

    theorem complexShortCombination_eventually_eventually (hMR : RealShortIntervalInput)
    {ι : Type*} (s : Finset ι) (c : ι → ℂ)
    (f : ℕ → ℕ → ι → ArithmeticFunction ℝ)
    (hmult : ∀ B n, ∀ i ∈ s, (f B n i).IsMultiplicative)
    (hf : ∀ B n, ∀ i ∈ s, ∀ k : ℕ, |f B n i k| ≤ 1)
    (H : ℕ → ℝ) (X : ℕ → ℕ → ℝ) (hH : Tendsto H atTop atTop)
    (hHX : ∀ B, ∀ᶠ n in atTop, H B ≤ X B n)
    (hlong : ∀ B, Tendsto (fun n => complexLongCombination s c (f B n) (X B n))
      atTop (𝓝 0)) :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ B in atTop, ∀ᶠ n in atTop,
      (1 / X B n) * (∫ z in X B n..2 * X B n,
        ‖complexShortCombination s c (f B n) (H B) z‖ ^ 2) < ε := by
…

    Mentions: OAI.JointDickman.PublishedInputs.RealShortIntervalInput, OAI.JointDickman.PublishedInputs.complexLongCombination, OAI.JointDickman.PublishedInputs.complexShortCombination