SmoothedBilinear.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Triangular smoothing of finite bilinear sums

lemma OAI.JointDickman.interval_energy_le_convolution line 13

Source documentation

Every point of an interval occurs at least Y times in the convolution of the two intervals of length 2Y.

lemma interval_energy_le_convolution (F : ℤ → ℂ) (a : ℤ) (Y : ℕ) :
    (Y : ℝ) * (∑ n ∈ Ico a (a+Y), ‖F n‖^2) ≤
      ∑ u ∈ Ico (0:ℤ) (2*Y), ∑ v ∈ Ico (0:ℤ) (2*Y),
        ‖F (a-Y+u+v)‖^2 := by
…

lemma OAI.JointDickman.additivePhase_mul_conj line 40

lemma OAI.JointDickman.convolution_phase_norm line 45

Source documentation

The smoothed correlation is a squared geometric sum.

lemma convolution_phase_norm (s : Finset ℤ) (a : ℤ) (t : ℝ) :
    ‖∑ u ∈ s, ∑ v ∈ s, additivePhase (t*(a+u+v))‖ =
      ‖∑ u ∈ s, additivePhase (t*u)‖^2 := by
…

Mentions: OAI.JointDickman.additivePhase

theorem OAI.JointDickman.smoothed_bilinear_energy line 63

Source documentation

Squared interval energy is controlled by the smoothed prime correlations.

theorem smoothed_bilinear_energy (P : Finset ℕ) (b : ℕ → ℂ)
    (θ : ℝ) (a : ℤ) (Y : ℕ) :
    (Y : ℝ) * (∑ n ∈ Ico a (a+Y),
      ‖∑ p ∈ P, b p * additivePhase (θ*p*n)‖^2) ≤
      ∑ p ∈ P, ∑ r ∈ P, ‖b p‖*‖b r‖*
        ‖∑ u ∈ Ico (0:ℤ) (2*Y), additivePhase (θ*((p:ℝ)-r)*u)‖^2 := by
…

Mentions: OAI.JointDickman.additivePhase

theorem OAI.JointDickman.smoothed_bilinear_bound line 98

Source documentation

Cauchy--Schwarz and triangular smoothing for a bounded integer coefficient.

theorem smoothed_bilinear_bound (P : Finset ℕ) (b : ℕ → ℂ)
    (c : ℤ → ℂ) (θ : ℝ) (a : ℤ) (Y : ℕ)
    (hc : ∀ n ∈ Ico a (a+Y), ‖c n‖ ≤ 1) :
    ‖∑ n ∈ Ico a (a+Y), c n *
      ∑ p ∈ P, b p * additivePhase (θ*p*n)‖^2 ≤
      ∑ p ∈ P, ∑ r ∈ P, ‖b p‖*‖b r‖*
        ‖∑ u ∈ Ico (0:ℤ) (2*Y), additivePhase (θ*((p:ℝ)-r)*u)‖^2 := by
…

Mentions: OAI.JointDickman.additivePhase