def Mathlib.Meta.Positivity.tmp : PositivityExt

The positivity extension which proves that ⨆ i, f i is nonnegative for a real-valued function f, provided each f i is nonnegative. This also handles the bounded supremum ⨆ i ∈ s, f i, which unfolds to a nested iSup.

class Flat.FG : Type

• f : ArithmeticFunction ℂ
• g : ArithmeticFunction ℂ
• M : ℝ
• hM_pos : 0 < M
• N : ℝ
• hN_pos : 0 < N
• hf (n : ℕ) : ↑n > M → f n = 0
• hg (n : ℕ) : ↑n > N → g n = 0

class Flat.Bump : Type

• ν : ℝ → ℝ
• diffν : ContDiff ℝ (↑⊤) ν
• suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2
• νpos (x : ℝ) : 0 ≤ ν x
• mass_one : ∫ (x : ℝ) in Set.Ici 0, ν x / x = 1

class Flat.ProofData : Type

• x : ℝ
• hx : 2 ≤ x
• Q : ℝ
• hQ_pos : 0 < Q

theorem Flat.ProofData.hx_pos [ProofData] : 0 < x

theorem Flat.ProofData.hlogx_succ_pos [ProofData] : 0 < Real.log (x + 1)

@[reducible]

noncomputable def Flat.ProofData.ε [ProofData] : ℝ

Equations

• Flat.ProofData.ε = (6 * Real.log 2)⁻¹ * Flat.ProofData.x⁻¹

theorem Flat.ProofData.hε_pos [ProofData] : 0 < ε

theorem Flat.ProofData.hε_lt_one [ProofData] : ε < 1

def Flat.ProofData.C_log_ε : NNReal

Equations

• Flat.ProofData.C_log_ε = 3

theorem Flat.ProofData.log_ε_inv_le_log_x [ProofData] : Real.log ε⁻¹ ≤ ↑C_log_ε * Real.log (x + 1)

noncomputable def Flat.ProofData.σ [ProofData] : ℝ

Equations

• Flat.ProofData.σ = 1 / Real.log (Flat.ProofData.x + 1)

theorem Flat.ProofData.hσ_pos [ProofData] : 0 < σ

theorem Flat.ProofData.hσ_le_one [ProofData] : σ ≤ 1

theorem Flat.ProofData.hσ_le_two [ProofData] : σ ≤ 2

noncomputable def Flat.T [Bump] [FG] {q : ℕ} (ε y : ℝ) (χ : DirichletCharacter ℂ q) : ℂ

Equations

• Flat.T ε y χ = summatory (fun (m : ℕ) => summatory (fun (n : ℕ) => Flat.FG.f m * χ ↑m * Flat.FG.g n * χ ↑n * ↑(Smooth1 Flat.Bump.ν ε (↑m * ↑n / y))) Flat.FG.N) Flat.FG.M

theorem Flat.T_eq_sum_integral [Bump] [FG] [ProofData] {q : ℕ} {χ : DirichletCharacter ℂ q} (y : ℝ) (hy : 1 ≤ y) : T ProofData.ε y χ = summatory (fun (m : ℕ) => summatory (fun (n : ℕ) => FG.f m * χ ↑m * FG.g n * χ ↑n * (1 / (2 * Real.pi)) • ∫ (t : ℝ), (↑m * ↑n / ↑y) ^ (-(↑ProofData.σ + ↑t * Complex.I)) • mellin (fun (x : ℝ) => ↑(Smooth1 Bump.ν ProofData.ε x)) (↑ProofData.σ + ↑t * Complex.I)) FG.N) FG.M

theorem Flat.integrable_term [Bump] [FG] [ProofData] {q : ℕ} {χ : DirichletCharacter ℂ q} {y : ℝ} (hy : 1 ≤ y) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : MeasureTheory.Integrable (fun (t : ℝ) => FG.f m * χ ↑m * ↑m ^ (-(↑ProofData.σ + ↑t * Complex.I)) * (FG.g n * χ ↑n * ↑n ^ (-(↑ProofData.σ + ↑t * Complex.I))) * (1 / ↑y) ^ (-(↑ProofData.σ + ↑t * Complex.I)) • mellin (fun (x : ℝ) => ↑(Smooth1 Bump.ν ProofData.ε x)) (↑ProofData.σ + ↑t * Complex.I)) MeasureTheory.volume

Written by Claude: A single term f m χ(m) m^{-s} · g n χ(n) n^{-s} · (1/y)^{-s} · 𝓜(Smooth1 ν ε)(s) is integrable along the vertical line s = σ + t·I. The r^{-(σ+t·I)} factors all have constant norm r^{-σ}, so the integrand is a bounded (in t) multiple of 𝓜(Smooth1 ν ε)(σ + t·I), which is integrable by Smooth1_verticalIntegrable. This is the common engine behind the two integrability side-goals in T_eq_integral_sum.

theorem Flat.T_eq_integral_sum [Bump] [FG] [ProofData] {q : ℕ} {χ : DirichletCharacter ℂ q} (y : ℝ) (hy : 1 ≤ y) : T ProofData.ε y χ = (1 / (2 * Real.pi)) • ∫ (t : ℝ), summatory (fun (m : ℕ) => FG.f m * χ ↑m * ↑m ^ (-(↑ProofData.σ + ↑t * Complex.I))) FG.M * summatory (fun (n : ℕ) => FG.g n * χ ↑n * ↑n ^ (-(↑ProofData.σ + ↑t * Complex.I))) FG.N * (1 / ↑y) ^ (-(↑ProofData.σ + ↑t * Complex.I)) • mellin (fun (x : ℝ) => ↑(Smooth1 Bump.ν ProofData.ε x)) (↑ProofData.σ + ↑t * Complex.I)

noncomputable def Flat.dirichletPoly {q : ℕ} (s : ℂ) (f : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (N : ℝ) : ℂ

Equations

• Flat.dirichletPoly s f χ N = summatory (fun (n : ℕ) => f n * χ ↑n * ↑n ^ (-s)) N

theorem Flat.Measurable_twistedLSum {q : ℕ} (f : ℕ → ℂ) (χ : DirichletCharacter ℂ q) (N : ℝ) : Measurable fun (t : ℂ) => dirichletPoly t f χ N

theorem Flat.dirichletAverage_twistedLSum_sq_le (s : ℂ) (f : ℕ → ℂ) (N Q : ℝ) : ∫⁻ (qχ : (q : ℕ) × DirichletCharacter ℂ q), ‖dirichletPoly s f qχ.snd N‖ₑ ^ 2 ∂dirichletMeas Q ≤ ENNReal.ofReal (C_LS * (N + Q ^ 2)) * summatory (fun (n : ℕ) => ‖f n‖ₑ ^ 2) N

@[reducible]

noncomputable def Flat.F [FG] {q : ℕ} (σ t : ℝ) (χ : DirichletCharacter ℂ q) : ℂ

Equations

• Flat.F σ t χ = Flat.dirichletPoly (↑σ + ↑t * Complex.I) (⇑Flat.FG.f) χ Flat.FG.M

theorem Flat.dirichletAverage_F_sq_le [FG] (σ t Q : ℝ) : ∫⁻ (qχ : (q : ℕ) × DirichletCharacter ℂ q), ‖F σ t qχ.snd‖ₑ ^ 2 ∂dirichletMeas Q ≤ ENNReal.ofReal (C_LS * (FG.M + Q ^ 2)) * summatory (fun (n : ℕ) => ‖FG.f n‖ₑ ^ 2) FG.M

@[reducible]

noncomputable def Flat.G [FG] {q : ℕ} (σ t : ℝ) (χ : DirichletCharacter ℂ q) : ℂ

Equations

• Flat.G σ t χ = Flat.dirichletPoly (↑σ + ↑t * Complex.I) (⇑Flat.FG.g) χ Flat.FG.N

noncomputable def Flat.C_TB : NNReal

Equations

• Flat.C_TB = ⟨Real.exp 1 * Real.pi⁻¹ * 2⁻¹, Flat.C_TB._proof_1⟩

theorem Flat.C_TB_def : ↑C_TB = ‖Real.exp 1 * Real.pi⁻¹ * 2⁻¹‖ₑ

@[simp]

theorem Flat.Complex.enorm_ofReal (r : ℝ) : ‖↑r‖ₑ = ‖r‖ₑ

@[simp]

theorem Flat.Complex.arg_ofReal_eq_pi_iff (x : ℝ) : (↑x).arg = Real.pi ↔ x < 0

theorem Flat.sup_T_le_lintegral_B [Bump] [FG] [ProofData] {q : ℕ} (χ : DirichletCharacter ℂ q) : ⨆ y ∈ Set.Icc 1 (ProofData.x + 1), ‖T ProofData.ε y χ‖ₑ ≤ ↑C_TB * ∫⁻ (t : ℝ), ‖F ProofData.σ t χ‖ₑ * ‖G ProofData.σ t χ‖ₑ * ‖mellin (fun (x : ℝ) => ↑(Smooth1 Bump.ν ProofData.ε x)) (↑ProofData.σ + ↑t * Complex.I)‖ₑ

theorem Flat.CS (f g : {q : ℕ} → DirichletCharacter ℂ q → ENNReal) (Q : ℝ) : ∫⁻ (a : (q : ℕ) × DirichletCharacter ℂ q), f a.snd * g a.snd ∂dirichletMeas Q ≤ (∫⁻ (a : (q : ℕ) × DirichletCharacter ℂ q), f a.snd ^ 2 ∂dirichletMeas Q) ^ (1 / 2) * (∫⁻ (a : (q : ℕ) × DirichletCharacter ℂ q), g a.snd ^ 2 ∂dirichletMeas Q) ^ (1 / 2)

theorem Flat.dirichletAverage_FG_le [Bump] [FG] [ProofData] {y : ℝ} : ∫⁻ (a : (q : ℕ) × DirichletCharacter ℂ q), ‖F ProofData.σ y a.snd‖ₑ * ‖G ProofData.σ y a.snd‖ₑ ∂dirichletMeas ProofData.Q ≤ ENNReal.ofReal ((√(FG.N * FG.M) + √FG.M * ProofData.Q + √FG.N * ProofData.Q + ProofData.Q ^ 2) * √(summatory (fun (m : ℕ) => ‖FG.f m‖ ^ 2) FG.M) * √(summatory (fun (n : ℕ) => ‖FG.g n‖ ^ 2) FG.N))

def Flat.C_Center : NNReal

Equations

• Flat.C_Center = sorry

theorem Flat.mellin_center_bound [Bump] {ε σ : ℝ} : ∫⁻ (a : ℝ) in Set.Icc (-ε⁻¹) ε⁻¹, ‖mellin (fun (x : ℝ) => ↑(Smooth1 Bump.ν ε x)) (↑σ + ↑a * Complex.I)‖ₑ ≤ ↑C_Center * ENNReal.ofReal (Real.log ε⁻¹)

noncomputable def Flat.C_Tail [Bump] : NNReal

Equations

• Flat.C_Tail = ⟨2 * ⋯.choose, ⋯⟩

theorem Flat.mellin_tail_bound [Bump] {ε σ : ℝ} (hε_pos : 0 < ε) (hε_lt_one : ε < 1) (hσ_pos : 0 < σ) (hσ_le_two : σ ≤ 2) : ∫⁻ (a : ℝ) in (Set.Icc (-ε⁻¹) ε⁻¹)ᶜ, ‖mellin (fun (x : ℝ) => ↑(Smooth1 Bump.ν ε x)) (↑σ + ↑a * Complex.I)‖ₑ ≤ ↑C_Tail

noncomputable def Flat.C_mellin [Bump] : NNReal

Equations

• Flat.C_mellin = Flat.C_Center + 2 * Flat.C_Tail

theorem Flat.lintegral_mellin_bdd [Bump] {ε σ : ℝ} (hσ_pos : 0 < σ) (hσ_le_two : σ ≤ 2) (hε_pos : 0 < ε) (hε_lt_one : ε < 1) : ∫⁻ (a : ℝ), ‖mellin (fun (x : ℝ) => ↑(Smooth1 Bump.ν ε x)) (↑σ + ↑a * Complex.I)‖ₑ ≤ ↑C_mellin * ENNReal.ofReal (Real.log ε⁻¹)

noncomputable def Flat.C_LSC [Bump] : NNReal

Equations

• Flat.C_LSC = Flat.C_TB * Flat.C_mellin * Flat.ProofData.C_log_ε

theorem Flat.summatory_T_ll [Bump] [FG] [ProofData] : summatory (fun (q : ℕ) => ↑q * (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ⨆ y ∈ Set.Icc 1 (ProofData.x + 1), ‖T ProofData.ε y χ‖ₑ) ProofData.Q ≤ ENNReal.ofReal (↑C_LSC * (√(FG.N * FG.M) + √FG.M * ProofData.Q + √FG.N * ProofData.Q + ProofData.Q ^ 2) * √(summatory (fun (m : ℕ) => ‖FG.f m‖ ^ 2) FG.M) * √(summatory (fun (n : ℕ) => ‖FG.g n‖ ^ 2) FG.N) * Real.log (ProofData.x + 1))

theorem Flat.sup_summatory_eq_sup_nat {f : ℕ → ℂ} {x : ℝ} (hx : 2 ≤ x) : ⨆ y ∈ Set.Icc 1 x, ‖summatory f y‖ₑ = ⨆ K ∈ Set.Icc 1 ⌊x⌋₊, ‖summatory f (↑K + 2⁻¹)‖ₑ

theorem Flat.temp [fg : FG] {x Q : ℝ} (hx : 2 ≤ x) : summatory (fun (q : ℕ) => ↑q * (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ⨆ y ∈ Set.Icc 1 x, ‖summatory (fun (n : ℕ) => (FG.f * FG.g) n * χ ↑n) y‖ₑ) Q = summatory (fun (q : ℕ) => ↑q * (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ⨆ K ∈ Set.Icc 1 ⌊x⌋₊, ‖summatory (fun (n : ℕ) => (FG.f * FG.g) n * χ ↑n) (↑K + 2⁻¹)‖ₑ) Q

theorem Flat.summatory_T_ll_nat [Bump] [FG] [data : ProofData] : summatory (fun (q : ℕ) => ↑q * (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ⨆ K ∈ Set.Icc 1 ⌊ProofData.x⌋₊, ‖T ProofData.ε (↑K + 2⁻¹) χ‖ₑ) ProofData.Q ≤ ENNReal.ofReal (↑C_LSC * (√(FG.N * FG.M) + √FG.M * ProofData.Q + √FG.N * ProofData.Q + ProofData.Q ^ 2) * √(summatory (fun (m : ℕ) => ‖FG.f m‖ ^ 2) FG.M) * √(summatory (fun (n : ℕ) => ‖FG.g n‖ ^ 2) FG.N) * Real.log (ProofData.x + 1))

theorem Flat.Nat.le_of_le_add_real {m n : ℕ} {x : ℝ} (hx_nonneg : 0 ≤ x) (hx : x < 1) (h : ↑m ≤ ↑n + x) : m ≤ n

theorem Flat.Nat.le_of_add_real_le {m n : ℕ} {x : ℝ} (hx_pos : 0 < x) (hx : x ≤ 1) (h : ↑m + x ≤ ↑n) : m + 1 ≤ n

theorem Flat.T_eq_sharp {x : ℝ} (hx : 1 ≤ x) [Bump] [FG] {q : ℕ} {ε : ℝ} (hε_pos : 0 < ε) {χ : DirichletCharacter ℂ q} (K : ℕ) (hK : ↑K ≤ x) (hε : ε ≤ (6 * Real.log 2)⁻¹ * x⁻¹) : T ε (↑K + 2⁻¹) χ = summatory (fun (m : ℕ) => summatory (fun (n : ℕ) => if ↑m * ↑n ≤ ↑K + 2⁻¹ then FG.f m * χ ↑m * FG.g n * χ ↑n else 0) FG.N) FG.M

theorem Flat.FG.summatory_mul [fg : FG] {y : ℝ} : summatory (fun (n : ℕ) => (f * g) n) y = summatory (fun (m : ℕ) => summatory (fun (n : ℕ) => if ↑m * ↑n ≤ y then f m * g n else 0) N) M

theorem Flat.FG.summatory_mul_char [fg : FG] {q : ℕ} {χ : DirichletCharacter ℂ q} {y : ℝ} : summatory (fun (n : ℕ) => (f * g) n * χ ↑n) y = summatory (fun (m : ℕ) => summatory (fun (n : ℕ) => if ↑m * ↑n ≤ y then f m * χ ↑m * g n * χ ↑n else 0) N) M

@[instance_reducible]

noncomputable instance Flat.instBump : Bump

Equations

• Flat.instBump = match Flat.instBump._proof_1 with | ⋯ => { ν := Classical.choose SmoothExistence, diffν := diffν, suppν := suppν, νpos := νpos, mass_one := mass_one }

theorem Flat.LargeSieve_convolution [fg : FG] {x Q : ℝ} (hx : 2 ≤ x) (hQ : 1 ≤ Q) : summatory (fun (q : ℕ) => ↑q * (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ⨆ y ∈ Set.Icc 1 x, ‖summatory (fun (n : ℕ) => (FG.f * FG.g) n * χ ↑n) y‖ₑ) Q ≤ ENNReal.ofReal (↑C_LSC * (√(FG.N * FG.M) + √FG.M * Q + √FG.N * Q + Q ^ 2) * √(summatory (fun (m : ℕ) => ‖FG.f m‖ ^ 2) FG.M) * √(summatory (fun (n : ℕ) => ‖FG.g n‖ ^ 2) FG.N) * Real.log (x + 1))