BinLabelPositiveEnergy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The positive energy forced by a nonzero mixed bin-label correlation

def OAI.JointDickman.movingBinLabel line 11
theorem OAI.JointDickman.binLabel_energy_of_amplified_limit line 15

theorem OAI.JointDickman.nonzero_binLabel_correlation_forces_energy line 57

Source documentation

The subsequence and the positive constant are constructed from the original mixed mean. The analytic assumptions are published inputs; the energy constant is independent of the later cutoff C.

theorem nonzero_binLabel_correlation_forces_energy
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput)
    {ι : Type*} [Fintype ι]
    (J : ℕ) (hJ : 0 < J) (k : ι → ℕ) (hk : ∀ i, 1 ≤ k i)
    (z : ι → ℂ) (hz : ∀ i, ‖z i‖ = 1)
    (H : ℕ → ℕ → ℂ) (hH : ∀ N n, ‖H N n‖ ≤ 2) {β : ℂ} (hβ : β ≠ 0)
    (hmean : Tendsto (fun N => (∑ n ∈ range N,
      star (movingBinLabel J k z N n) * H N n)/(N : ℂ)) atTop (nhds β)) :
    ∃ (s : ℕ → ℕ), StrictMono s ∧ ∃ e : ℝ, 0 < e ∧
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.movingBinLabel