@[instance_reducible]

def DirichletAverage.instMeasurableSpaceSigmaNatDirichletCharacterComplex_bV : MeasurableSpace ((q : ℕ) × DirichletCharacter ℂ q)

Equations

• DirichletAverage.instMeasurableSpaceSigmaNatDirichletCharacterComplex_bV = ⊤

theorem DirichletAverage.instDiscreteMeasurableSpaceSigmaNatDirichletCharacterComplex_bV : DiscreteMeasurableSpace ((q : ℕ) × DirichletCharacter ℂ q)

noncomputable def charsUpTo (Q : ℝ) : Finset ((q : ℕ) × DirichletCharacter ℂ q)

Equations

• charsUpTo Q = (Finset.Ioc 0 ⌊Q⌋₊).biUnion fun (q : ℕ) => Finset.image (fun (χ : DirichletCharacter ℂ q) => ⟨q, χ⟩) (Finset.filter DirichletCharacter.IsPrimitive Finset.univ)

theorem mem_charsUpTo {p : (q : ℕ) × DirichletCharacter ℂ q} {Q : ℝ} (hQ0 : 0 ≤ Q) : p ∈ charsUpTo Q ↔ p.snd.IsPrimitive ∧ 0 < p.fst ∧ ↑p.fst ≤ Q

theorem Finset.sum_charsUpTo {Q : ℝ} (f : (q : ℕ) → DirichletCharacter ℂ q → ENNReal) : ∑ p ∈ charsUpTo Q, f p.fst p.snd = summatory (fun (q : ℕ) => ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, f q χ) Q

noncomputable def dirichletMeas (Q : ℝ) : MeasureTheory.Measure ((q : ℕ) × DirichletCharacter ℂ q)

Equations

• dirichletMeas Q = MeasureTheory.Measure.count.withDensity ((↑(charsUpTo Q)).indicator fun (x : (q : ℕ) × DirichletCharacter ℂ q) => match x with | ⟨q, snd⟩ => ↑q * (↑q.totient)⁻¹)

theorem lintegral_dirichletMeas {Q : ℝ} (f : {q : ℕ} → DirichletCharacter ℂ q → ENNReal) : ∫⁻ (p : (q : ℕ) × DirichletCharacter ℂ q), f p.snd ∂dirichletMeas Q = summatory (fun (q : ℕ) => ↑q * (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, f χ) Q

theorem lintegral_dirichletMeas' {Q : ℝ} (f : (q : ℕ) × DirichletCharacter ℂ q → ENNReal) : ∫⁻ (p : (q : ℕ) × DirichletCharacter ℂ q), f p ∂dirichletMeas Q = summatory (fun (q : ℕ) => ↑q * (↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, f ⟨q, χ⟩) Q