def RayClassField.halfPlane (K : Type u) [Field K] [NumberField K] : Set ℂ

noncomputable def RayClassField.nonzeroIdealToFracIdealCoprime (K : Type u_1) [Field K] [NumberField K] (𝔪 : Modulus K) (I : Ideal (NumberField.RingOfIntegers K)) (_hI : I ≠ ⊥) (hcop : IsCoprime I 𝔪.finitePartIdeal) : FracIdealsCoprime K 𝔪

noncomputable def RayClassField.idealInRayClass {K : Type u} [Field K] [NumberField K] (𝔪 : Modulus K) (I : Ideal (NumberField.RingOfIntegers K)) : RayClassGroup K 𝔪

noncomputable def RayClassField.rayClassPartialZeta_coeffs {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : ℕ → ℂ

noncomputable def RayClassField.rayClassPartialZeta {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : ℂ → ℂ

noncomputable def RayClassField.rayClassPartialZeta_residue_val {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (_γ : RayClassGroup K 𝔪) : ℂ

theorem RayClassField.rayClassPartialZeta_residue_val_ne_zero {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : rayClassPartialZeta_residue_val γ ≠ 0

theorem RayClassField.ray_class_lattice_data (K : Type u_1) [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : ∃ (Λ : Submodule ℤ (Fin (Module.finrank ℚ K) → ℝ)) (x : DiscreteTopology ↥Λ) (_ : IsZLattice ℝ Λ) (S : Set (Fin (Module.finrank ℚ K) → ℝ)), MeasurableSet S ∧ Section19.IsLipschitzParametrizable (frontier S) (Module.finrank ℚ K - 1) ∧ (∃ (w_𝔪 : ℕ), 0 < w_𝔪 ∧ ∀ᶠ (t : ℝ) in Filter.atTop, ↑w_𝔪 * ↑(Nat.card { I : Ideal (NumberField.RingOfIntegers K) // I ≠ ⊥ ∧ IsCoprime I 𝔪.finitePartIdeal ∧ ↑(Ideal.absNorm I) ≤ t ∧ idealInRayClass 𝔪 I = γ }) = ↑(Nat.card ↑{x : ↥Λ | ↑x ∈ (fun (v : Fin (Module.finrank ℚ K) → ℝ) => t ^ (1 / ↑(Module.finrank ℚ K)) • v) '' S})) ∧ (MeasureTheory.volume S).toReal / ZLattice.covolume Λ MeasureTheory.volume = NumberField.dedekindZeta_residue K / ↑(Fintype.card (RayClassGroup K 𝔪)) ∧ MeasureTheory.volume S ≠ ⊤ ∧ Bornology.IsBounded S

theorem RayClassField.rayClassPartialZeta_coeffs_sum_eq_count {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) (t : ℕ) : ∑ i ∈ Finset.range t, rayClassPartialZeta_coeffs γ (i + 1) = ↑(Nat.card { I : Ideal (NumberField.RingOfIntegers K) // I ≠ ⊥ ∧ IsCoprime I 𝔪.finitePartIdeal ∧ Ideal.absNorm I ≤ t ∧ idealInRayClass 𝔪 I = γ })

theorem RayClassField.ray_class_count_error {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℕ), ‖↑(Nat.card { I : Ideal (NumberField.RingOfIntegers K) // I ≠ ⊥ ∧ IsCoprime I 𝔪.finitePartIdeal ∧ Ideal.absNorm I ≤ t ∧ idealInRayClass 𝔪 I = γ }) - rayClassPartialZeta_residue_val γ * ↑t‖ ≤ C * ↑t ^ (1 - 1 / ↑(Module.finrank ℚ K))

theorem RayClassField.rayClassPartialZeta_asymptotic {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : ∃ (C : ℝ), ∀ (t : ℕ), ‖∑ i ∈ Finset.range t, rayClassPartialZeta_coeffs γ (i + 1) - rayClassPartialZeta_residue_val γ * ↑t‖ ≤ C * ↑t ^ (1 - 1 / ↑(Module.finrank ℚ K))

noncomputable def RayClassField.rayClassPartialZeta_ext {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : ℂ → ℂ

theorem RayClassField.rayClassPartialZeta_summable {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) (s : ℂ) (hs : 1 < s.re) : LSeriesSummable (rayClassPartialZeta_coeffs γ) s

theorem RayClassField.rayClassPartialZeta_ext_eq {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) (s : ℂ) (hs : 1 < s.re) : rayClassPartialZeta_ext γ s = rayClassPartialZeta γ s

theorem RayClassField.halfPlane_exponent_nonneg {K : Type u} [Field K] [NumberField K] : 0 ≤ 1 - 1 / ↑(Module.finrank ℚ K)

theorem RayClassField.halfPlane_exponent_lt_one {K : Type u} [Field K] [NumberField K] : 1 - 1 / ↑(Module.finrank ℚ K) < 1

theorem RayClassField.rayClassPartialZeta_ext_meromorphicOn {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : MeromorphicOn (rayClassPartialZeta_ext γ) (halfPlane K)

theorem RayClassField.rayClassPartialZeta_ext_residue {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : Filter.Tendsto (fun (s : ℂ) => (s - 1) * rayClassPartialZeta_ext γ s) (nhdsWithin 1 {1}ᶜ) (nhds (rayClassPartialZeta_residue_val γ))

noncomputable def RayClassField.rayClassPartialZeta_residue {K : Type u} [Field K] [NumberField K] (𝔪 : Modulus K) : ℂ

noncomputable def RayClassField.rayClassPartialZeta_regularPart {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : ℂ → ℂ

theorem RayClassField.rayClassPartialZeta_regularPart_analyticAt {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : AnalyticAt ℂ (rayClassPartialZeta_regularPart γ) 1

theorem RayClassField.rayClassPartialZeta_ext_eq_decomp {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) : ∀ᶠ (s : ℂ) in nhds 1, rayClassPartialZeta_ext γ s = rayClassPartialZeta_residue 𝔪 * riemannZeta s + rayClassPartialZeta_regularPart γ s

noncomputable def RayClassField.weberLFunction_combinedCoeffs {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) : ℕ → ℂ

theorem RayClassField.weberLFunction_combinedCoeffs_eq_sum {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) : weberLFunction_combinedCoeffs χ = ∑ γ : RayClassGroup K 𝔪, ↑(χ γ) • rayClassPartialZeta_coeffs γ

theorem RayClassField.evalIdealExt_eq_char_idealInRayClass {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (I : Ideal (NumberField.RingOfIntegers K)) (hne : I ≠ ⊥) (hcop : IsCoprime I 𝔪.finitePartIdeal) : χ.evalIdealExt I = ↑(χ (idealInRayClass 𝔪 I))

theorem RayClassField.summand_fiber_eq {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (γ : RayClassGroup K 𝔪) (s : ℂ) (𝔞 : { I : Ideal (NumberField.RingOfIntegers K) // I ≠ ⊥ }) (hmem : idealInRayClass 𝔪 ↑𝔞 = γ) : χ.evalIdealExt ↑𝔞 * ↑(Ideal.absNorm ↑𝔞) ^ (-s) = if IsCoprime (↑𝔞) 𝔪.finitePartIdeal then ↑(χ γ) * ↑(Ideal.absNorm ↑𝔞) ^ (-s) else 0

theorem RayClassField.fiber_tsum_eq_LSeries {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) (s : ℂ) : ∑' (𝔞 : { I : Ideal (NumberField.RingOfIntegers K) // I ≠ ⊥ ∧ IsCoprime I 𝔪.finitePartIdeal ∧ idealInRayClass 𝔪 I = γ }), ↑(Ideal.absNorm ↑𝔞) ^ (-s) = LSeries (rayClassPartialZeta_coeffs γ) s

theorem RayClassField.dirichletSeries_eq_sum_rayClass_LSeries (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassChar K 𝔪) (s : ℂ) (hs : 1 < s.re) : ∑' (𝔞 : { I : Ideal (NumberField.RingOfIntegers K) // I ≠ ⊥ }), χ.evalIdealExt ↑𝔞 * ↑(Ideal.absNorm ↑𝔞) ^ (-s) = ∑ γ : RayClassGroup K 𝔪, ↑(χ γ) * LSeries (rayClassPartialZeta_coeffs γ) s

theorem RayClassField.WeberLFunction_eq_LSeries_combinedCoeffs {K : Type u} [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassChar K 𝔪) (s : ℂ) (hs : 1 < s.re) : WeberLFunction K 𝔪 χ s = LSeries (weberLFunction_combinedCoeffs χ) s

theorem RayClassField.rayClassPartialZeta_coeffs_summable {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (γ : RayClassGroup K 𝔪) (s : ℂ) (hs : 1 < s.re) : LSeriesSummable (rayClassPartialZeta_coeffs γ) s

theorem RayClassField.WeberLFunction_eq_sum_rayClassPartialZeta {K : Type u} [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassChar K 𝔪) (s : ℂ) (hs : 1 < s.re) : WeberLFunction K 𝔪 χ s = ∑ γ : RayClassGroup K 𝔪, ↑(χ γ) * rayClassPartialZeta γ s

theorem RayClassField.sum_nonprincipal_char_eq_zero {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (hχ : ¬χ.IsPrincipal) : ∑ γ : RayClassGroup K 𝔪, ↑(χ γ) = 0

theorem RayClassField.WeberLFunction_ext_continuousAt_one_of_nonprincipal {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (hχ : ¬χ.IsPrincipal) : ContinuousAt (fun (s : ℂ) => ∑ γ : RayClassGroup K 𝔪, ↑(χ γ) * rayClassPartialZeta_ext γ s) 1

structure RayClassField.WeberLFunction_MeromorphicExtension {K : Type u} [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassChar K 𝔪) : Type

• toFun : ℂ → ℂ
• eq_on_convergence (s : ℂ) : 1 < s.re → self.toFun s = WeberLFunction K 𝔪 χ s
• meromorphicOn : MeromorphicOn self.toFun (halfPlane K)
• simple_pole_at_one : ∃ (v : ℂ), AnalyticAt ℂ (Function.update (fun (s : ℂ) => (s - 1) * self.toFun s) 1 v) 1
• holomorphic_at_one_of_nonprincipal : ¬χ.IsPrincipal → AnalyticAt ℂ self.toFun 1

noncomputable def RayClassField.WeberLFunction_ext {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (s : ℂ) : ℂ

theorem RayClassField.WeberLFunction_ext_eq {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (s : ℂ) (hs : 1 < s.re) : WeberLFunction_ext χ s = WeberLFunction K 𝔪 χ s

theorem RayClassField.WeberLFunction_ext_meromorphicOn {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) : MeromorphicOn (WeberLFunction_ext χ) (halfPlane K)

theorem RayClassField.WeberLFunction_ext_simple_pole {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) : ∃ (v : ℂ), AnalyticAt ℂ (Function.update (fun (s : ℂ) => (s - 1) * WeberLFunction_ext χ s) 1 v) 1

theorem RayClassField.WeberLFunction_ext_holomorphic_at_one_of_nonprincipal {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (hχ : ¬χ.IsPrincipal) : AnalyticAt ℂ (WeberLFunction_ext χ) 1

noncomputable def RayClassField.Proposition_22_19 {K : Type u} [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassChar K 𝔪) : WeberLFunction_MeromorphicExtension 𝔪 χ