def Section19.IsLipschitzContinuous {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (f : X → Y) : Prop

def Section19.IsLipschitzParametrizable {X : Type u_1} [PseudoMetricSpace X] (B : Set X) (d : ℕ) : Prop

theorem Section19.IsLipschitzParametrizable.image_linearEquiv {n d : ℕ} {B : Set (Fin n → ℝ)} (hB : IsLipschitzParametrizable B d) (e : (Fin n → ℝ) ≃L[ℝ] Fin n → ℝ) : IsLipschitzParametrizable (⇑e '' B) d

theorem Section19.IsLipschitzParametrizable.union {X : Type u_1} [PseudoMetricSpace X] {A B : Set X} {d : ℕ} (hA : IsLipschitzParametrizable A d.succ) (hB : IsLipschitzParametrizable B d.succ) : IsLipschitzParametrizable (A ∪ B) d.succ

theorem Section19.floor_diff_bound' {a b D : ℝ} (hab : |a - b| ≤ D) : |⌊a⌋ - ⌊b⌋| ≤ ⌈D⌉

theorem Section19.scaled_coord_diff_le_K {n d : ℕ} {f : (Fin d → ℝ) → Fin n → ℝ} {K : NNReal} (hf : LipschitzWith K f) {y y' : Fin d → ℝ} {t : ℝ} (ht_pos : 0 < t) {T : ℝ} (hT_pos : 0 < T) (ht_le : t ≤ T) (hdist : dist y y' ≤ 1 / T) (i : Fin n) : |t * f y i - t * f y' i| ≤ ↑K

theorem Section19.lipschitz_floor_image_card_bound {n d : ℕ} (f : (Fin d → ℝ) → Fin n → ℝ) (K : NNReal) (hf : LipschitzWith K f) (t : ℝ) (ht : 1 ≤ t) : Nat.card ↑{v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin d) => Set.Icc 0 1, ∀ (i : Fin n), ↑(v i) ≤ t * f y i ∧ t * f y i < ↑(v i) + 1} ≤ ⌈t⌉₊ ^ d * (2 * ⌈↑K * √↑d⌉₊ + 3) ^ n

theorem Section19.lipschitz_floor_image_finite {n d : ℕ} (f : (Fin d → ℝ) → Fin n → ℝ) (K : NNReal) (hf : LipschitzWith K f) (t : ℝ) (ht : 1 ≤ t) : {v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin d) => Set.Icc 0 1, ∀ (i : Fin n), ↑(v i) ≤ t * f y i ∧ t * f y i < ↑(v i) + 1}.Finite

theorem Section19.single_lipschitz_image_cube_count {n d : ℕ} (f : (Fin d → ℝ) → Fin n → ℝ) (K : NNReal) (hf : LipschitzWith K f) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 1 ≤ t → ↑(Nat.card ↑{v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin d) => Set.Icc 0 1, ∀ (i : Fin n), ↑(v i) ≤ t * f y i ∧ t * f y i < ↑(v i) + 1}) ≤ C * t ^ d

def Section19.outerCubeSet {n : ℕ} (S : Set (Fin n → ℝ)) (t : ℝ) : Set (Fin n → ℤ)

def Section19.innerCubeSet {n : ℕ} (S : Set (Fin n → ℝ)) (t : ℝ) : Set (Fin n → ℤ)

theorem Section19.lattice_count_subset_outerCubeSet {n : ℕ} (S : Set (Fin n → ℝ)) (t : ℝ) : {x : Fin n → ℤ | (fun (i : Fin n) => ↑(x i) / t) ∈ S} ⊆ outerCubeSet S t

theorem Section19.innerCubeSet_subset_lattice_count {n : ℕ} (S : Set (Fin n → ℝ)) (t : ℝ) : innerCubeSet S t ⊆ {x : Fin n → ℤ | (fun (i : Fin n) => ↑(x i) / t) ∈ S}

theorem Section19.outerCubeSet_finite {n : ℕ} (_hn : 0 < n) (S : Set (Fin n → ℝ)) (_hS : MeasurableSet S) (hBdd : Bornology.IsBounded S) (t : ℝ) (ht : 1 ≤ t) : (outerCubeSet S t).Finite

noncomputable def Section19.unitCube {n : ℕ} (v : Fin n → ℤ) : Set (Fin n → ℝ)

theorem Section19.cube_measure_sandwich {n : ℕ} (hn : 0 < n) (S : Set (Fin n → ℝ)) (hS : MeasurableSet S) (hS_vol : MeasureTheory.volume S ≠ ⊤) (t : ℝ) (ht : 1 ≤ t) (hfin_outer : (outerCubeSet S t).Finite) : ↑(Nat.card ↑(innerCubeSet S t)) ≤ (MeasureTheory.volume S).toReal * t ^ n ∧ (MeasureTheory.volume S).toReal * t ^ n ≤ ↑(Nat.card ↑(outerCubeSet S t))

theorem Section19.preconnected_frontier_inter {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsPreconnected s) {A : Set α} (hA : (s ∩ A).Nonempty) (hAc : (s ∩ Aᶜ).Nonempty) : (s ∩ frontier A).Nonempty

theorem Section19.innerCubeSet_subset_outerCubeSet {n : ℕ} (S : Set (Fin n → ℝ)) (t : ℝ) : innerCubeSet S t ⊆ outerCubeSet S t

theorem Section19.boundary_cubes_bound {n : ℕ} (hn : 0 < n) (S : Set (Fin n → ℝ)) (hS : MeasurableSet S) (numMaps : ℕ) (maps : Fin numMaps → (Fin (n - 1) → ℝ) → Fin n → ℝ) (hCover : frontier S ⊆ ⋃ (i : Fin numMaps), maps i '' Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1) (t : ℝ) (ht : 1 ≤ t) (hFinOuter : (outerCubeSet S t).Finite) (hFinBdry : ∀ (i : Fin numMaps), {v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1, ∀ (j : Fin n), ↑(v j) ≤ t * maps i y j ∧ t * maps i y j < ↑(v j) + 1}.Finite) : ↑(Nat.card ↑(outerCubeSet S t)) ≤ ↑(Nat.card ↑(innerCubeSet S t)) + ∑ i : Fin numMaps, ↑(Nat.card ↑{v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1, ∀ (j : Fin n), ↑(v j) ≤ t * maps i y j ∧ t * maps i y j < ↑(v j) + 1})

theorem Section19.lattice_count_upper_sandwich {n : ℕ} (hn : 0 < n) (S : Set (Fin n → ℝ)) (hS_meas : MeasurableSet S) (hS_vol : MeasureTheory.volume S ≠ ⊤) (hBdd : Bornology.IsBounded S) (numMaps : ℕ) (maps : Fin numMaps → (Fin (n - 1) → ℝ) → Fin n → ℝ) (hCover : frontier S ⊆ ⋃ (i : Fin numMaps), maps i '' Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1) (t : ℝ) (ht : 1 ≤ t) (hFinBdry : ∀ (i : Fin numMaps), {v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1, ∀ (j : Fin n), ↑(v j) ≤ t * maps i y j ∧ t * maps i y j < ↑(v j) + 1}.Finite) : ↑(Nat.card ↑{x : Fin n → ℤ | (fun (i : Fin n) => ↑(x i) / t) ∈ S}) ≤ (MeasureTheory.volume S).toReal * t ^ n + ∑ i : Fin numMaps, ↑(Nat.card ↑{v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1, ∀ (j : Fin n), ↑(v j) ≤ t * maps i y j ∧ t * maps i y j < ↑(v j) + 1})

theorem Section19.lattice_count_lower_sandwich {n : ℕ} (hn : 0 < n) (S : Set (Fin n → ℝ)) (hS_meas : MeasurableSet S) (hS_vol : MeasureTheory.volume S ≠ ⊤) (hBdd : Bornology.IsBounded S) (numMaps : ℕ) (maps : Fin numMaps → (Fin (n - 1) → ℝ) → Fin n → ℝ) (hCover : frontier S ⊆ ⋃ (i : Fin numMaps), maps i '' Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1) (t : ℝ) (ht : 1 ≤ t) (hFinBdry : ∀ (i : Fin numMaps), {v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1, ∀ (j : Fin n), ↑(v j) ≤ t * maps i y j ∧ t * maps i y j < ↑(v j) + 1}.Finite) : (MeasureTheory.volume S).toReal * t ^ n ≤ ↑(Nat.card ↑{x : Fin n → ℤ | (fun (i : Fin n) => ↑(x i) / t) ∈ S}) + ∑ i : Fin numMaps, ↑(Nat.card ↑{v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1, ∀ (j : Fin n), ↑(v j) ≤ t * maps i y j ∧ t * maps i y j < ↑(v j) + 1})

theorem Section19.lattice_count_error_bound {n : ℕ} (hn : 0 < n) (S : Set (Fin n → ℝ)) (hS_meas : MeasurableSet S) (hS_vol : MeasureTheory.volume S ≠ ⊤) (hBdd : Bornology.IsBounded S) (numMaps : ℕ) (maps : Fin numMaps → (Fin (n - 1) → ℝ) → Fin n → ℝ) (hCover : frontier S ⊆ ⋃ (i : Fin numMaps), maps i '' Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1) (t : ℝ) (ht : 1 ≤ t) (hFinBdry : ∀ (i : Fin numMaps), {v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1, ∀ (j : Fin n), ↑(v j) ≤ t * maps i y j ∧ t * maps i y j < ↑(v j) + 1}.Finite) : ‖↑(Nat.card ↑{x : Fin n → ℤ | (fun (i : Fin n) => ↑(x i) / t) ∈ S}) - (MeasureTheory.volume S).toReal * t ^ n‖ ≤ ∑ i : Fin numMaps, ↑(Nat.card ↑{v : Fin n → ℤ | ∃ y ∈ Set.univ.pi fun (x : Fin (n - 1)) => Set.Icc 0 1, ∀ (j : Fin n), ↑(v j) ≤ t * maps i y j ∧ t * maps i y j < ↑(v j) + 1})

theorem Section19.lattice_point_count_asymptotics {n : ℕ} (hn : 0 < n) (S : Set (Fin n → ℝ)) (hS_meas : MeasurableSet S) (hS_vol : MeasureTheory.volume S ≠ ⊤) (hBdd : Bornology.IsBounded S) (hS_bdry : IsLipschitzParametrizable (frontier S) (n - 1)) : ∃ (C : ℝ), ∀ᶠ (t : ℝ) in Filter.atTop, ‖↑(Nat.card ↑{x : Fin n → ℤ | (fun (i : Fin n) => ↑(x i) / t) ∈ S}) - (MeasureTheory.volume S).toReal * t ^ n‖ ≤ C * t ^ (n - 1)

theorem Section19.lattice_count_change_of_basis {n : ℕ} (_hn : 0 < n) (S : Set (Fin n → ℝ)) (hS_meas : MeasurableSet S) (hS_bdry : IsLipschitzParametrizable (frontier S) (n - 1)) (Λ : Submodule ℤ (Fin n → ℝ)) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] (hS_vol : MeasureTheory.volume S ≠ ⊤ := by exact ENNReal.ofReal_ne_top) (hBdd : Bornology.IsBounded S := by exact Bornology.IsBounded.empty) : ∃ (S' : Set (Fin n → ℝ)), MeasurableSet S' ∧ IsLipschitzParametrizable (frontier S') (n - 1) ∧ (∀ (t : ℝ), t ≠ 0 → ↑(Nat.card ↑{x : ↥Λ | ↑x ∈ (fun (v : Fin n → ℝ) => t • v) '' S}) = ↑(Nat.card ↑{x : Fin n → ℤ | (fun (i : Fin n) => ↑(x i) / t) ∈ S'})) ∧ ZLattice.covolume Λ MeasureTheory.volume * (MeasureTheory.volume S').toReal = (MeasureTheory.volume S).toReal ∧ MeasureTheory.volume S' ≠ ⊤ ∧ Bornology.IsBounded S'

theorem Section19.lattice_point_count_general {n : ℕ} (hn : 0 < n) (S : Set (Fin n → ℝ)) (hS_meas : MeasurableSet S) (hS_vol : MeasureTheory.volume S ≠ ⊤) (hS_bdry : IsLipschitzParametrizable (frontier S) (n - 1)) (hBdd : Bornology.IsBounded S) (Λ : Submodule ℤ (Fin n → ℝ)) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] : ∃ (C : ℝ), ∀ᶠ (t : ℝ) in Filter.atTop, ‖↑(Nat.card ↑{x : ↥Λ | ↑x ∈ (fun (v : Fin n → ℝ) => t • v) '' S}) - (MeasureTheory.volume S).toReal / ZLattice.covolume Λ MeasureTheory.volume * t ^ n‖ ≤ C * t ^ (n - 1)

theorem Section19.per_class_ideal_count_isBigO (K : Type u_2) [Field K] [NumberField K] (C : ClassGroup (NumberField.RingOfIntegers K)) : (fun (s : ℝ) => ↑(Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C }) - 2 ^ NumberField.InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * NumberField.Units.regulator K / (↑(NumberField.Units.torsionOrder K) * √|↑(NumberField.discr K)|) * s) =O[Filter.atTop] fun (s : ℝ) => s ^ (1 - 1 / ↑(Module.finrank ℚ K))

theorem Section19.ideal_count_error_bound (K : Type u_2) [Field K] [NumberField K] : (fun (t : ℝ) => ↑(Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ t }) - 2 ^ NumberField.InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * NumberField.Units.regulator K * ↑(NumberField.classNumber K) / (↑(NumberField.Units.torsionOrder K) * √|↑(NumberField.discr K)|) * t) =O[Filter.atTop] fun (t : ℝ) => t ^ (1 - 1 / ↑(Module.finrank ℚ K))

noncomputable def Section19.idealToClass (K : Type u_1) [Field K] [NumberField K] (I : Ideal (NumberField.RingOfIntegers K)) (hI : I ≠ ⊥) : ClassGroup (NumberField.RingOfIntegers K)

noncomputable def Section19.toFinME (K : Type u_1) [Field K] [NumberField K] : NumberField.mixedEmbedding.euclidean.mixedSpace K ≃ᵐ (Fin (Module.finrank ℚ K) → ℝ)

theorem Section19.LSeriesSummable_of_partial_sum_bound (a : ℕ → ℂ) (σ : ℝ) (hσ : 0 ≤ σ) (hpartial : ∃ (C : ℝ), ∀ (t : ℕ), ‖∑ i ∈ Finset.range t, a (i + 1)‖ ≤ C * ↑t ^ σ) (s : ℂ) (hs : σ + 1 < s.re) : LSeriesSummable a s

noncomputable def Section19.dirichletSeriesAbel (f : ℕ → ℂ) (s : ℂ) : ℂ

theorem Section19.dirichletSeriesAbel_eq_LSeries (f : ℕ → ℂ) (s : ℂ) (hf : LSeriesSummable f s) {r : ℝ} (hr : 0 ≤ r) (hrs : r < s.re) (hO : (fun (n : ℕ) => ∑ k ∈ Finset.Icc 1 n, f k) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ r) : dirichletSeriesAbel f s = LSeries f s

noncomputable def Section19.dirichletSeriesContinuation (a : ℕ → ℂ) (ρ : ℂ) : ℂ → ℂ

noncomputable def Section19.stepFnAbel (f : ℕ → ℂ) (x : ℝ) : ℂ

theorem Section19.stepFnAbel_eq_zero_of_le_one (f : ℕ → ℂ) {x : ℝ} (hx : x ≤ 1) : stepFnAbel f x = 0

theorem Section19.stepFnAbel_measurable (f : ℕ → ℂ) : Measurable (stepFnAbel f)

theorem Section19.stepFnAbel_locallyIntegrableOn (f : ℕ → ℂ) : MeasureTheory.LocallyIntegrableOn (stepFnAbel f) (Set.Ioi 0) MeasureTheory.volume

theorem Section19.rpow_anti_base {x y σ : ℝ} (hx : 0 < x) (hxy : x ≤ y) (hσ : σ ≤ 0) : y ^ σ ≤ x ^ σ

theorem Section19.floor_rpow_le (x σ : ℝ) (hx : 2 ≤ x) : ↑⌊x⌋₊ ^ σ ≤ 2 ^ |σ| * x ^ σ

theorem Section19.stepFnAbel_isBigO_atTop (f : ℕ → ℂ) (σ : ℝ) (hf : ∃ (C : ℝ), ∀ (t : ℕ), ‖∑ i ∈ Finset.range t, f (i + 1)‖ ≤ C * ↑t ^ σ) : stepFnAbel f =O[Filter.atTop] fun (x : ℝ) => x ^ σ

theorem Section19.stepFnAbel_isBigO_nhds_zero (f : ℕ → ℂ) (b : ℝ) : stepFnAbel f =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => x ^ (-b)

theorem Section19.mellin_integrand_eq_indicator (f : ℕ → ℂ) (s : ℂ) (x : ℝ) : ↑x ^ (-s - 1) • stepFnAbel f x = (Set.Ioi 1).indicator (fun (x : ℝ) => (∑ n ∈ Finset.range ⌊x⌋₊, f (n + 1)) * ↑x ^ (-(s + 1))) x

theorem Section19.mellin_stepFnAbel_eq (f : ℕ → ℂ) (s : ℂ) : mellin (stepFnAbel f) (-s) = ∫ (x : ℝ) in Set.Ioi 1, (∑ n ∈ Finset.range ⌊x⌋₊, f (n + 1)) * ↑x ^ (-(s + 1))

theorem Section19.dirichletSeriesAbel_integral_differentiableOn (f : ℕ → ℂ) (σ : ℝ) (hf : ∃ (C : ℝ), ∀ (t : ℕ), ‖∑ i ∈ Finset.range t, f (i + 1)‖ ≤ C * ↑t ^ σ) : DifferentiableOn ℂ (fun (s : ℂ) => ∫ (x : ℝ) in Set.Ioi 1, (∑ n ∈ Finset.range ⌊x⌋₊, f (n + 1)) * ↑x ^ (-(s + 1))) {s : ℂ | σ < s.re}

theorem Section19.LSeries_analyticOnNhd_of_partialSum_le (f : ℕ → ℂ) (σ : ℝ) (hf : ∃ (C : ℝ), ∀ (t : ℕ), ‖∑ i ∈ Finset.range t, f (i + 1)‖ ≤ C * ↑t ^ σ) : AnalyticOnNhd ℂ (dirichletSeriesAbel f) {s : ℂ | σ < s.re}

theorem Section19.dirichlet_series_remainder_holomorphic (a : ℕ → ℂ) (σ : ℝ) (ρ : ℂ) (hasympt : ∃ (C : ℝ), ∀ (t : ℕ), ‖∑ i ∈ Finset.range t, a (i + 1) - ρ * ↑t‖ ≤ C * ↑t ^ σ) : AnalyticOnNhd ℂ (dirichletSeriesAbel fun (n : ℕ) => a n - ρ) {s : ℂ | σ < s.re}

theorem Section19.dirichlet_series_meromorphic_continuation (a : ℕ → ℂ) (σ : ℝ) (_hσ : 0 ≤ σ) (hσ1 : σ < 1) (ρ : ℂ) (_hρ : ρ ≠ 0) (hasympt : ∃ (C : ℝ), ∀ (t : ℕ), ‖∑ i ∈ Finset.range t, a (i + 1) - ρ * ↑t‖ ≤ C * ↑t ^ σ) : Filter.Tendsto (fun (s : ℝ) => (↑s - 1) * dirichletSeriesContinuation a ρ ↑s) (nhdsWithin 1 (Set.Ioi 1)) (nhds ρ)

theorem Section19.riemannZeta_analyticAt {s : ℂ} (hs : s ≠ 1) : AnalyticAt ℂ riemannZeta s

theorem Section19.riemannZeta_meromorphicAt_one : MeromorphicAt riemannZeta 1

theorem Section19.dirichlet_series_meromorphicOn (a : ℕ → ℂ) (σ : ℝ) (_hσ : 0 ≤ σ) (_hσ1 : σ < 1) (ρ : ℂ) (_hρ : ρ ≠ 0) (hasympt : ∃ (C : ℝ), ∀ (t : ℕ), ‖∑ i ∈ Finset.range t, a (i + 1) - ρ * ↑t‖ ≤ C * ↑t ^ σ) : MeromorphicOn (dirichletSeriesContinuation a ρ) {s : ℂ | σ < s.re}

theorem Section19.dirichlet_series_analyticAt_off_pole (a : ℕ → ℂ) (σ : ℝ) (ρ : ℂ) (hasympt : ∃ (C : ℝ), ∀ (t : ℕ), ‖∑ i ∈ Finset.range t, a (i + 1) - ρ * ↑t‖ ≤ C * ↑t ^ σ) (s : ℂ) : s ∈ {s : ℂ | σ < s.re} → s ≠ 1 → AnalyticAt ℂ (dirichletSeriesContinuation a ρ) s

theorem Section19.riemannZeta_order_witness : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g 1 ∧ g 1 ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhdsWithin 1 {1}ᶜ, riemannZeta z = (z - 1) ^ (-1) • g z

theorem Section19.dirichlet_series_residue_complex (a : ℕ → ℂ) (σ : ℝ) (_hσ : 0 ≤ σ) (hσ1 : σ < 1) (ρ : ℂ) (_hρ : ρ ≠ 0) (hasympt : ∃ (C : ℝ), ∀ (t : ℕ), ‖∑ i ∈ Finset.range t, a (i + 1) - ρ * ↑t‖ ≤ C * ↑t ^ σ) : Filter.Tendsto (fun (s : ℂ) => (s - 1) * dirichletSeriesContinuation a ρ s) (nhdsWithin 1 {1}ᶜ) (nhds ρ)

theorem Section19.dedekindZeta_sub_one_mul_analytic_aux (K : Type u_2) [Field K] [NumberField K] : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g 1 ∧ (fun (s : ℂ) => (s - 1) * NumberField.dedekindZeta K s) =ᶠ[nhds 1] g

theorem Section19.dedekindZeta_sub_one_mul_analyticAt (K : Type u_1) [Field K] [NumberField K] : AnalyticAt ℂ (fun (s : ℂ) => (s - 1) * NumberField.dedekindZeta K s) 1

theorem Section19.analytic_class_number_formula_explicit (K : Type u_1) [Field K] [NumberField K] : Filter.Tendsto (fun (s : ℝ) => (↑s - 1) * NumberField.dedekindZeta K ↑s) (nhdsWithin 1 (Set.Ioi 1)) (nhds ↑(2 ^ NumberField.InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * NumberField.Units.regulator K * ↑(NumberField.classNumber K) / (↑(NumberField.Units.torsionOrder K) * √|↑(NumberField.discr K)|))) ∧ 0 < 2 ^ NumberField.InfinitePlace.nrRealPlaces K * (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * NumberField.Units.regulator K * ↑(NumberField.classNumber K) / (↑(NumberField.Units.torsionOrder K) * √|↑(NumberField.discr K)|) ∧ AnalyticAt ℂ (fun (s : ℂ) => (s - 1) * NumberField.dedekindZeta K s) 1

def Section19.IsUnramifiedAtPrime (K : Type u_1) [Field K] [NumberField K] (p : ℕ) : Prop

def Section19.pFreePart (m p : ℕ) : ℕ

theorem Section19.pFreePart_pos {m : ℕ} (hm : 0 < m) (p : ℕ) : 0 < pFreePart m p

instance Section19.pFreePart_neZero {m : ℕ} [NeZero m] (p : ℕ) : NeZero (pFreePart m p)

theorem Section19.pFreePart_dvd (m p : ℕ) : pFreePart m p ∣ m

theorem Section19.not_dvd_pFreePart {m : ℕ} (hm : 0 < m) (p : ℕ) (hp : Nat.Prime p) : ¬p ∣ pFreePart m p

theorem Section19.isUnramifiedAtPrime_of_le (m : ℕ) [NeZero m] (p : ℕ) (E E' : IntermediateField ℚ (CyclotomicField m ℚ)) (hle : E ≤ E') (hE' : IsUnramifiedAtPrime (↥E') p) : IsUnramifiedAtPrime (↥E) p

theorem Section19.cyclotomic_ppow_unramified_at_other_primes (m : ℕ) [NeZero m] (p : ℕ) (hp : Nat.Prime p) (E₁ : IntermediateField ℚ (CyclotomicField m ℚ)) [IsCyclotomicExtension {p ^ padicValNat p m} ℚ ↥E₁] (q : ℕ) (hq : Nat.Prime q) (hqp : q ≠ p) : IsUnramifiedAtPrime (↥E₁) q

theorem Section19.minkowski_no_unramified_extension (m : ℕ) [NeZero m] (F : IntermediateField ℚ (CyclotomicField m ℚ)) (hF : ∀ (q : ℕ), Nat.Prime q → IsUnramifiedAtPrime (↥F) q) : F = ⊥

theorem Section19.cyclotomic_ppow_unramified_le_bot (m : ℕ) [NeZero m] (p : ℕ) (hp : Nat.Prime p) (E₁ : IntermediateField ℚ (CyclotomicField m ℚ)) [IsCyclotomicExtension {p ^ padicValNat p m} ℚ ↥E₁] (F : IntermediateField ℚ (CyclotomicField m ℚ)) (hFE₁ : F ≤ E₁) (hF : IsUnramifiedAtPrime (↥F) p) : F = ⊥

theorem Section19.cyclotomic_ramIdx_eq_of_unramified (m : ℕ) [NeZero m] (p : ℕ) (E E' : IntermediateField ℚ (CyclotomicField m ℚ)) (hE' : IsUnramifiedAtPrime (↥E') p) [Algebra ↥E ↥(E ⊔ E')] (P : Ideal (NumberField.RingOfIntegers ↥E)) [P.IsPrime] (hP : P.LiesOver (Ideal.span {↑p})) (Q : Ideal (NumberField.RingOfIntegers ↥(E ⊔ E'))) [Q.IsPrime] [Q.LiesOver P] [Q.LiesOver (Ideal.span {↑p})] : (Ideal.span {↑p}).ramificationIdx Q = (Ideal.span {↑p}).ramificationIdx P

theorem Section19.baseChange_ramificationIdx_eq_one (m : ℕ) [NeZero m] (p : ℕ) (E E' : IntermediateField ℚ (CyclotomicField m ℚ)) (hE' : IsUnramifiedAtPrime (↥E') p) [inst_alg : Algebra ↥E ↥(E ⊔ E')] (P : Ideal (NumberField.RingOfIntegers ↥E)) [P.IsPrime] (hP : P.LiesOver (Ideal.span {↑p})) (Q : Ideal (NumberField.RingOfIntegers ↥(E ⊔ E'))) [Q.IsPrime] [Q.LiesOver P] : P.ramificationIdx Q = 1

theorem Section19.isUnramifiedAtPrime_sup (m : ℕ) [NeZero m] (p : ℕ) (E E' : IntermediateField ℚ (CyclotomicField m ℚ)) (hE : IsUnramifiedAtPrime (↥E) p) (hE' : IsUnramifiedAtPrime (↥E') p) : IsUnramifiedAtPrime (↥(E ⊔ E')) p

instance Section19.cyclotomicSubgroupModular (m : ℕ) [NeZero m] : IsModularLattice (Subgroup Gal(CyclotomicField m ℚ/ℚ))

instance Section19.cyclotomicIntermediateFieldModular (m : ℕ) [NeZero m] : IsModularLattice (IntermediateField ℚ (CyclotomicField m ℚ))

theorem Section19.cyclotomic_coprime_sup_eq_top (m : ℕ) [NeZero m] (p : ℕ) (hp : Nat.Prime p) (E₀ : IntermediateField ℚ (CyclotomicField m ℚ)) [IsCyclotomicExtension {pFreePart m p} ℚ ↥E₀] (E₁ : IntermediateField ℚ (CyclotomicField m ℚ)) [IsCyclotomicExtension {p ^ padicValNat p m} ℚ ↥E₁] : E₀ ⊔ E₁ = ⊤

theorem Section19.cyclotomic_coprime_nontrivial_ext (m : ℕ) [NeZero m] (p : ℕ) (hp : Nat.Prime p) (E₀ : IntermediateField ℚ (CyclotomicField m ℚ)) [IsCyclotomicExtension {pFreePart m p} ℚ ↥E₀] (E₁ : IntermediateField ℚ (CyclotomicField m ℚ)) [IsCyclotomicExtension {p ^ padicValNat p m} ℚ ↥E₁] (F : IntermediateField ℚ (CyclotomicField m ℚ)) (hE₀F : E₀ < F) : F ⊓ E₁ ≠ ⊥

theorem Section19.le_of_inf_ppow_cyclotomic_eq_bot (m : ℕ) [NeZero m] (p : ℕ) (hp : Nat.Prime p) (E₀ : IntermediateField ℚ (CyclotomicField m ℚ)) [IsCyclotomicExtension {pFreePart m p} ℚ ↥E₀] (E₁ : IntermediateField ℚ (CyclotomicField m ℚ)) [IsCyclotomicExtension {p ^ padicValNat p m} ℚ ↥E₁] (E : IntermediateField ℚ (CyclotomicField m ℚ)) (hEE₁ : E ⊓ E₁ = ⊥) (hEunram : IsUnramifiedAtPrime (↥E) p) : E ≤ E₀

theorem Section19.cyclotomic_unramified_intermediate_le (m : ℕ) [NeZero m] (p : ℕ) (hp : Nat.Prime p) (E₀ : IntermediateField ℚ (CyclotomicField m ℚ)) [IsCyclotomicExtension {pFreePart m p} ℚ ↥E₀] (E : IntermediateField ℚ (CyclotomicField m ℚ)) (hE : IsUnramifiedAtPrime (↥E) p) : E ≤ E₀

theorem Section19.cyclotomic_maximal_unramified_subextension (m : ℕ) [NeZero m] (p : ℕ) (hp : Nat.Prime p) : ∃ (E₀ : IntermediateField ℚ (CyclotomicField m ℚ)), IsCyclotomicExtension {pFreePart m p} ℚ ↥E₀ ∧ IsUnramifiedAtPrime (↥E₀) p ∧ ∀ (E : IntermediateField ℚ (CyclotomicField m ℚ)), IsUnramifiedAtPrime (↥E) p → E ≤ E₀

theorem Section19.proposition_19_14 (m : ℕ) [NeZero m] (p : ℕ) (hp : Nat.Prime p) : ∃ (E₀ : IntermediateField ℚ (CyclotomicField m ℚ)), IsCyclotomicExtension {pFreePart m p} ℚ ↥E₀ ∧ IsUnramifiedAtPrime (↥E₀) p ∧ ∀ (E : IntermediateField ℚ (CyclotomicField m ℚ)), IsUnramifiedAtPrime (↥E) p → E ≤ E₀

instance Section19.instNeZeroCastRat (m : ℕ) [NeZero m] : NeZero ↑m

instance Section19.instIsCyclotomicExtensionCyclotomicField (m : ℕ) [NeZero m] : IsCyclotomicExtension {m} ℚ (CyclotomicField m ℚ)

noncomputable def Section19.subgroupDualOrderIso (G : Type u_1) [CommGroup G] [Finite G] : Subgroup G ≃o (Subgroup (G →* ℂˣ))ᵒᵈ

@[reducible, inline]

noncomputable abbrev Section19.prop_18_40 (G : Type u_1) [CommGroup G] [Finite G] : Subgroup G ≃o (Subgroup (G →* ℂˣ))ᵒᵈ

theorem Section19.subgroup_dual_annihilator_mem (G : Type u_1) [CommGroup G] [Finite G] (K : Subgroup (G →* ℂˣ)) (g : G) : g ∈ (subgroupDualOrderIso G).symm (OrderDual.toDual K) ↔ ∀ χ ∈ K, χ g = 1

theorem Section19.subgroup_dual_card_annihilator (G : Type u_1) [CommGroup G] [Fintype G] (H : Subgroup G) : Nat.card ↥H * Nat.card ↥(MonoidHom.restrictHom H ℂˣ).ker = Nat.card G

@[reducible, inline]

abbrev Section19.prop_18_40_card (G : Type u_1) [CommGroup G] [Fintype G] (H : Subgroup G) : Nat.card ↥H * Nat.card ↥(MonoidHom.restrictHom H ℂˣ).ker = Nat.card G

theorem Section19.subgroup_dual_card_dual_annihilator (G : Type u_1) [CommGroup G] [Fintype G] (K : Subgroup (G →* ℂˣ)) : Nat.card ↥K * Nat.card ↥((subgroupDualOrderIso G).symm (OrderDual.toDual K)) = Nat.card G

theorem Section19.subgroup_dual_correspondence (G : Type u_1) [CommGroup G] [Fintype G] : Nonempty (Subgroup G ≃o (Subgroup (G →* ℂˣ))ᵒᵈ) ∧ (∀ (K : Subgroup (G →* ℂˣ)) (g : G), g ∈ (subgroupDualOrderIso G).symm (OrderDual.toDual K) ↔ ∀ χ ∈ K, χ g = 1) ∧ (∀ (H : Subgroup G), Nat.card ↥H * Nat.card ↥(MonoidHom.restrictHom H ℂˣ).ker = Nat.card G) ∧ ∀ (K : Subgroup (G →* ℂˣ)), Nat.card ↥K * Nat.card ↥((subgroupDualOrderIso G).symm (OrderDual.toDual K)) = Nat.card G

def Section19.characterAnnihilator (m : ℕ) (H : Subgroup (DirichletCharacter ℂ m)) : Subgroup (ZMod m)ˣ

noncomputable def Section19.galoisAnnihilator (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) : Subgroup Gal(CyclotomicField m ℚ/ℚ)

noncomputable def Section19.fixedFieldOfCharacterSubgroup (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) : IntermediateField ℚ (CyclotomicField m ℚ)

instance Section19.instNumberFieldFixedField (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) : NumberField ↥(fixedFieldOfCharacterSubgroup m H)

noncomputable def Section19.dedekindZetaLocalFactor (K : Type u_1) [Field K] [NumberField K] (p : ℕ) (s : ℂ) : ℂ

noncomputable def Section19.characterLocalFactor (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (s : ℂ) : ℂ

theorem Section19.roots_of_unity_prod_eq (f : ℕ) (hf : 0 < f) (T : ℂ) : ∏ μ ∈ Polynomial.nthRootsFinset f 1, (1 - μ * T) = 1 - T ^ f

noncomputable def Section19.frobenius_f_p (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (_hp : Nat.Prime p) : ℕ

noncomputable def Section19.frobenius_g_p (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) : ℕ

theorem Section19.frobenius_f_p_pos (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) : 0 < frobenius_f_p m H p hp

theorem Section19.prod_fiber_const_card {α : Type u_1} {β : Type u_2} {M : Type u_3} [CommMonoid M] [DecidableEq β] [Fintype α] {f : α → β} {S : Finset β} {k : ℕ} (himg : ∀ (a : α), f a ∈ S) (hfib : ∀ b ∈ S, {a : α | f a = b}.card = k) (h : β → M) : ∏ a : α, h (f a) = (∏ b ∈ S, h b) ^ k

def Section19.evalAtUnit (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (u : (ZMod m)ˣ) : ↥H →* ℂ

theorem Section19.fiber_card_of_surj_onto {G : Type u_1} [Group G] [Fintype G] (f : G →* ℂ) (S : Finset ℂ) (hS : 0 < S.card) (himg : ∀ (g : G), f g ∈ S) (hsurj : ∀ s ∈ S, ∃ (g : G), f g = s) (μ : ℂ) : μ ∈ S → {g : G | f g = μ}.card = Fintype.card G / S.card

theorem Section19.artin_eval_surjective_aux (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) (hcop : p.Coprime m) (μ : ℂ) : μ ∈ Polynomial.nthRootsFinset (frobenius_f_p m H p hp) 1 → ∃ (χ : ↥H), (evalAtUnit m H (ZMod.unitOfCoprime p hcop)) χ = μ

theorem Section19.artin_eval_fiber_uniform_aux (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) (hcop : p.Coprime m) : have f_p := frobenius_f_p m H p hp; have g_p := frobenius_g_p m H p hp; ∀ μ ∈ Polynomial.nthRootsFinset f_p 1, {χ : ↥H | ↑χ ↑p = μ}.card = g_p

theorem Section19.artin_eval_fiber_uniform (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) (hcop : p.Coprime m) : have f_p := frobenius_f_p m H p hp; have g_p := frobenius_g_p m H p hp; (∀ (χ : ↥H), ↑χ ↑p ∈ Polynomial.nthRootsFinset f_p 1) ∧ ∀ μ ∈ Polynomial.nthRootsFinset f_p 1, {χ : ↥H | ↑χ ↑p = μ}.card = g_p

theorem Section19.frobenius_character_distribution_identity (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) (hcop : p.Coprime m) (T : ℂ) : ∏ χ : ↥H, (1 - ↑χ ↑p * T) = (∏ μ ∈ Polynomial.nthRootsFinset (frobenius_f_p m H p hp) 1, (1 - μ * T)) ^ frobenius_g_p m H p hp

@[reducible]

noncomputable def Section19.primes_above_fintype (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (_hp : Nat.Prime p) : Fintype { I : Ideal (NumberField.RingOfIntegers ↥(fixedFieldOfCharacterSubgroup m H)) // I.IsPrime ∧ I ≠ ⊥ ∧ ↑p ∈ I }

theorem Section19.artin_reciprocity_efg_identity (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) : Fintype.card { I : Ideal (NumberField.RingOfIntegers ↥(fixedFieldOfCharacterSubgroup m H)) // I.IsPrime ∧ I ≠ ⊥ ∧ ↑p ∈ I } * frobenius_f_p m H p hp = Fintype.card ↥H

theorem Section19.artin_reciprocity_card_primes_mul_f_eq_card_H (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) : Fintype.card { I : Ideal (NumberField.RingOfIntegers ↥(fixedFieldOfCharacterSubgroup m H)) // I.IsPrime ∧ I ≠ ⊥ ∧ ↑p ∈ I } * frobenius_f_p m H p hp = Fintype.card ↥H

theorem Section19.primes_above_card (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) : Fintype.card { I : Ideal (NumberField.RingOfIntegers ↥(fixedFieldOfCharacterSubgroup m H)) // I.IsPrime ∧ I ≠ ⊥ ∧ ↑p ∈ I } = frobenius_g_p m H p hp

theorem Section19.inertiaDeg_eq_frobenius_f_p (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) (𝔭 : Ideal (NumberField.RingOfIntegers ↥(fixedFieldOfCharacterSubgroup m H))) (h𝔭_prime : 𝔭.IsPrime) (h𝔭_ne_bot : 𝔭 ≠ ⊥) (h𝔭_mem : ↑p ∈ 𝔭) [𝔭.LiesOver (Ideal.span {↑p})] : (Ideal.span {↑p}).inertiaDeg 𝔭 = frobenius_f_p m H p hp

theorem Section19.primes_above_absNorm (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) (𝔭 : { I : Ideal (NumberField.RingOfIntegers ↥(fixedFieldOfCharacterSubgroup m H)) // I.IsPrime ∧ I ≠ ⊥ ∧ ↑p ∈ I }) : ↑(Ideal.absNorm ↑𝔭) = ↑p ^ ↑(frobenius_f_p m H p hp)

theorem Section19.frobenius_local_factor (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) (s : ℂ) : dedekindZetaLocalFactor (↥(fixedFieldOfCharacterSubgroup m H)) p s = (1 - ↑p ^ (-(s * ↑(frobenius_f_p m H p hp))))⁻¹ ^ frobenius_g_p m H p hp

theorem Section19.frobenius_character_distribution (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) (hcop : p.Coprime m) : ∃ (f_p : ℕ) (g_p : ℕ), 0 < f_p ∧ (∀ (T : ℂ), ∏ χ : ↥H, (1 - ↑χ ↑p * T) = (∏ μ ∈ Polynomial.nthRootsFinset f_p 1, (1 - μ * T)) ^ g_p) ∧ ∀ (s : ℂ), dedekindZetaLocalFactor (↥(fixedFieldOfCharacterSubgroup m H)) p s = (1 - ↑p ^ (-(s * ↑f_p)))⁻¹ ^ g_p

theorem Section19.artin_reciprocity_frobenius_distribution (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (p : ℕ) (hp : Nat.Prime p) (hcop : p.Coprime m) (s : ℂ) : dedekindZetaLocalFactor (↥(fixedFieldOfCharacterSubgroup m H)) p s = characterLocalFactor m H p s

noncomputable def Section19.dedekindZetaTerm (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : ℕ → ℂ

theorem Section19.dedekindZetaTerm_zero (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : dedekindZetaTerm K s 0 = 0

theorem Section19.dedekindZetaTerm_one (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : dedekindZetaTerm K s 1 = 1

theorem Section19.idealNormCount_mul_coprime (K : Type u_1) [Field K] [NumberField K] {m n : ℕ} (hmn : m.Coprime n) (hm : m ≠ 0) (hn : n ≠ 0) : Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = m * n } = Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = m } * Nat.card { J : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm J = n }

theorem Section19.dedekindZetaTerm_mul_coprime (K : Type u_1) [Field K] [NumberField K] (s : ℂ) {m n : ℕ} (hmn : m.Coprime n) : dedekindZetaTerm K s (m * n) = dedekindZetaTerm K s m * dedekindZetaTerm K s n

theorem Section19.dedekindZetaTerm_normSummable (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (hs : 1 < s.re) : Summable fun (n : ℕ) => ‖dedekindZetaTerm K s n‖

theorem Section19.absNorm_prime_above_is_prime_pow (K : Type u_1) [Field K] [NumberField K] (p : Nat.Primes) (𝔭 : Ideal (NumberField.RingOfIntegers K)) (h𝔭 : 𝔭.IsPrime ∧ 𝔭 ≠ ⊥ ∧ ↑↑p ∈ 𝔭) : ∃ (f : ℕ), 0 < f ∧ Ideal.absNorm 𝔭 = ↑p ^ f

@[implicit_reducible]

noncomputable instance Section19.primesAbove_fintype (K : Type u_1) [Field K] [NumberField K] (p : Nat.Primes) : Fintype { I : Ideal (NumberField.RingOfIntegers K) // I.IsPrime ∧ I ≠ ⊥ ∧ ↑↑p ∈ I }

theorem Section19.idealCount_localFactor_identity (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (hs : 1 < s.re) (p : Nat.Primes) : ∑' (e : ℕ), ↑(Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = ↑p ^ e }) * ↑(↑p ^ e) ^ (-s) = ∏ᶠ (𝔭 : { I : Ideal (NumberField.RingOfIntegers K) // I.IsPrime ∧ I ≠ ⊥ ∧ ↑↑p ∈ I }), (1 - ↑(Ideal.absNorm ↑𝔭) ^ (-s))⁻¹

theorem Section19.idealCount_localFactor_tsum_eq (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (hs : 1 < s.re) (p : Nat.Primes) : ∑' (e : ℕ), LSeries.term (fun (n : ℕ) => ↑(Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n })) s (↑p ^ e) = ∏ᶠ (𝔭 : { I : Ideal (NumberField.RingOfIntegers K) // I.IsPrime ∧ I ≠ ⊥ ∧ ↑↑p ∈ I }), (1 - ↑(Ideal.absNorm ↑𝔭) ^ (-s))⁻¹

theorem Section19.dedekindZetaTerm_localFactor_eq (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (hs : 1 < s.re) (p : Nat.Primes) : ∑' (e : ℕ), dedekindZetaTerm K s (↑p ^ e) = dedekindZetaLocalFactor K (↑p) s

theorem Section19.dedekindZeta_hasProd_localFactor (K : Type u_1) [Field K] [NumberField K] (s : ℂ) (hs : 1 < s.re) : HasProd (fun (p : Nat.Primes) => dedekindZetaLocalFactor K (↑p) s) (NumberField.dedekindZeta K s)

theorem Section19.LSeries_prod_eq_tprod_localFactor (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (s : ℂ) (hs : 1 < s.re) : ∏ χ : ↥H, LSeries (fun (n : ℕ) => ↑χ ↑n) s = ∏' (p : Nat.Primes), characterLocalFactor m H (↑p) s

theorem Section19.euler_product_determines_equality (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (s : ℂ) (hs : 1 < s.re) (hfactors : ∀ (p : ℕ), Nat.Prime p → dedekindZetaLocalFactor (↥(fixedFieldOfCharacterSubgroup m H)) p s = characterLocalFactor m H p s) : NumberField.dedekindZeta (↥(fixedFieldOfCharacterSubgroup m H)) s = ∏ χ : ↥H, LSeries (fun (n : ℕ) => ↑χ ↑n) s

theorem Section19.conductor_reduction_data (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (s : ℂ) (hs : 1 < s.re) (p : ℕ) (hp : Nat.Prime p) (hram : ¬p.Coprime m) : ∃ (m' : ℕ) (x : NeZero m') (H' : Subgroup (DirichletCharacter ℂ m')), m' < m ∧ NumberField.dedekindZeta (↥(fixedFieldOfCharacterSubgroup m H)) s = NumberField.dedekindZeta (↥(fixedFieldOfCharacterSubgroup m' H')) s ∧ ∏ χ : ↥H, LSeries (fun (n : ℕ) => ↑χ ↑n) s = ∏ χ : ↥H', LSeries (fun (n : ℕ) => ↑χ ↑n) s

theorem Section19.conductor_reduction_at_ramified_prime (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (s : ℂ) (hs : 1 < s.re) (p : ℕ) (hp : Nat.Prime p) (hram : ¬p.Coprime m) (ih : ∀ (m' : ℕ) [inst : NeZero m'] (H' : Subgroup (DirichletCharacter ℂ m')), m' < m → NumberField.dedekindZeta (↥(fixedFieldOfCharacterSubgroup m' H')) s = ∏ χ : ↥H', LSeries (fun (n : ℕ) => ↑χ ↑n) s) : NumberField.dedekindZeta (↥(fixedFieldOfCharacterSubgroup m H)) s = ∏ χ : ↥H, LSeries (fun (n : ℕ) => ↑χ ↑n) s

@[irreducible]

theorem Section19.conductor_reduction_global (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (s : ℂ) (hs : 1 < s.re) : NumberField.dedekindZeta (↥(fixedFieldOfCharacterSubgroup m H)) s = ∏ χ : ↥H, LSeries (fun (n : ℕ) => ↑χ ↑n) s

theorem Section19.subgroup_dedekindZeta_eq_LSeries_prod (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (s : ℂ) (hs : 1 < s.re) : NumberField.dedekindZeta (↥(fixedFieldOfCharacterSubgroup m H)) s = ∏ χ : ↥H, LSeries (fun (n : ℕ) => ↑χ ↑n) s

theorem Section19.subgroup_zeta_eq_prod_L_functions (m : ℕ) [NeZero m] (H : Subgroup (DirichletCharacter ℂ m)) (s : ℂ) (hs : 1 < s.re) : NumberField.dedekindZeta (↥(fixedFieldOfCharacterSubgroup m H)) s = ∏ χ : ↥H, DirichletCharacter.LFunction (↑χ) s

theorem Section19.dirichlet_L_ne_zero_at_one {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ ≠ 1) : DirichletCharacter.LFunction χ 1 ≠ 0