NYLL
Module

RamificationNumberFormula.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RamificationNumberFormula
12 declarations indexed from sourceView source ↗

Module documentation

Herbrand-function sum formula for a general discretely valued field

This is the field-facing, noncomplete form of the Herbrand-function sum formula. The monogenic integral-generator theorem supplies the generator hidden inside intrinsicRamificationNumberOfUniqueExtension; the public endpoint therefore uses exactly the canonical standing hypotheses and has no generator parameter.

Imports3
Imported by2

Declarations

instance

galoisFintype

L38 ↗
RamificationTheory.HilbertRamification.Higher.galoisFintype
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · statement
instance galoisFintype : Fintype Gal(L/K)
instance

subgroupFintype

L41 ↗
RamificationTheory.HilbertRamification.Higher.subgroupFintype
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
Lean source · statement
instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H
instance

subgroupMembershipDecidable

L44 ↗
RamificationTheory.HilbertRamification.Higher.subgroupMembershipDecidable
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
local instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H :=
  Fintype.ofFinite H
Lean source · statement
instance subgroupMembershipDecidable
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : Decidable (sigma ∈ H)
def

truncateENatAtDVF

L49 ↗
RamificationTheory.HilbertRamification.Higher.truncateENatAtDVF
Documentation

min {i,r}, with the extended value infinity truncated to r.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
local instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : Decidable (sigma ∈ H) :=
  Classical.propDecidable _
Lean source · statement
def truncateENatAtDVF (i : ℕ∞) (r : ℝ) : ℝ
theorem

truncateENatAtDVF_top

L53 ↗
RamificationTheory.HilbertRamification.Higher.truncateENatAtDVF_top
Documentation

States the theorem truncateENatAtDVF_top.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
local instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : Decidable (sigma ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem truncateENatAtDVF_top (r : ℝ) :
    truncateENatAtDVF ⊤ r = r
theorem

truncateENatAtDVF_coe

L58 ↗
RamificationTheory.HilbertRamification.Higher.truncateENatAtDVF_coe
Documentation

States the theorem truncateENatAtDVF_coe.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
local instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : Decidable (sigma ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem truncateENatAtDVF_coe (n : ℕ) (r : ℝ) :
    truncateENatAtDVF (n : ℕ∞) r = min (n : ℝ) r
theorem

truncateENatAtDVF_eq_right_of_natCast_le

L63 ↗
RamificationTheory.HilbertRamification.Higher.truncateENatAtDVF_eq_right_of_natCast_le
Documentation

States the theorem truncateENatAtDVF_eq_right_of_natCast_le.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
local instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : Decidable (sigma ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem truncateENatAtDVF_eq_right_of_natCast_le
    {i : ℕ∞} {m : ℕ} {r : ℝ} (hr : r ≤ m) (hi : (m : ℕ∞) ≤ i) :
    truncateENatAtDVF i r = r
theorem

truncate_intrinsicRamificationNumberOfUniqueExtension_eq_intrinsic_summand

L78 ↗
RamificationTheory.HilbertRamification.Higher.truncate_intrinsicRamificationNumberOfUniqueExtension_eq_intrinsic_summand
Documentation

Pointwise ramification-number contribution for an element of inertia.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
local instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : Decidable (sigma ∈ H) :=
  Classical.propDecidable _
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  truncatedLowerDepth
) in
Lean source · full declaration
theorem truncate_intrinsicRamificationNumberOfUniqueExtension_eq_intrinsic_summand
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (m : ℕ) {s : ℝ} (hms : (m : ℝ) ≤ s) (hsm : s ≤ m + 1)
    (sigma : (lowerRamificationFiltrationOfUniqueExtension
      (base := base) (target := target) huniq).lower 0) :
    truncateENatAtDVF
        (intrinsicRamificationNumberOfUniqueExtension
          (base := base) (target := target) huniq (sigma : Gal(L/K)))
        (s + 1) =
      1 + ((truncatedLowerDepth (lowerRamificationFiltrationOfUniqueExtension (base := base)
        (target := target) huniq)) m sigma : ℝ) +
      (s - m) *
        (if (sigma : Gal(L/K)) ∈ (lowerRamificationFiltrationOfUniqueExtension
          (base := base) (target := target) huniq).lower (m + 1)
        then 1 else 0) := by
  classical
  let F := lowerRamificationFiltrationOfUniqueExtension
    (base := base) (target := target) huniq
  let i := intrinsicRamificationNumberOfUniqueExtension
    (base := base) (target := target) huniq (sigma : Gal(L/K))
  change truncateENatAtDVF i (s + 1) =
    1 + ((truncatedLowerDepth F) m sigma : ℝ) +
      (s - m) * (if (sigma : Gal(L/K)) ∈ F.lower (m + 1) then 1 else 0)
  have hi_one : (1 : ℕ∞) ≤ i := by
    exact (mem_lowerRamificationGroup_nat_iff_intrinsicRamificationNumberOfUniqueExtension_ge
      (base := base) (target := target) huniq 0 (sigma : Gal(L/K))).1 sigma.property
  by_cases hhigh : ((m + 2 : ℕ) : ℕ∞) ≤ i
  · have hmem : (sigma : Gal(L/K)) ∈ F.lower (m + 1) := by
      exact (mem_lowerRamificationGroup_nat_iff_intrinsicRamificationNumberOfUniqueExtension_ge
        (base := base) (target := target) huniq (m + 1)
          (sigma : Gal(L/K))).2 (by simpa [i, Nat.add_assoc] using hhigh)
    have hdepth : (truncatedLowerDepth F) m sigma = m := by
      rw [truncatedLowerDepth]
      rw [Finset.filter_eq_self.2]
      · simp
      · intro j hj
        exact (mem_lowerRamificationGroup_nat_iff_intrinsicRamificationNumberOfUniqueExtension_ge
          (base := base) (target := target) huniq (j + 1)
            (sigma : Gal(L/K))).2 (by
              have hjm : j < m := Finset.mem_range.1 hj
              have : ((j + 2 : ℕ) : ℕ∞) ≤ (m + 2 : ℕ) := by
                exact_mod_cast (by omega : j + 2 ≤ m + 2)
              exact (by simpa [i, Nat.add_assoc] using this.trans hhigh))
    have htrunc : truncateENatAtDVF i (s + 1) = s + 1 := by
      exact truncateENatAtDVF_eq_right_of_natCast_le
        (m := m + 2) (by
          norm_num [Nat.cast_add, Nat.cast_ofNat] at hsm ⊢
          linarith) hhigh
    rw [htrunc, hdepth]
    simp [hmem]
    ring
  · have hlt : i < ((m + 2 : ℕ) : ℕ∞) := lt_of_not_ge hhigh
    have hine : i ≠ ⊤ := ne_top_of_lt hlt
    obtain ⟨k, hk⟩ := ENat.ne_top_iff_exists.1 hine
    have hk_one : 1 ≤ k := by
      exact_mod_cast (hi_one.trans_eq hk.symm)
    have hk_upper : k ≤ m + 1 := by
      have : k < m + 2 := by exact_mod_cast (hk.symm ▸ hlt)
      omega
    have hmem : (sigma : Gal(L/K)) ∉ F.lower (m + 1) := by
      intro hmem
      have hge :=
        (mem_lowerRamificationGroup_nat_iff_intrinsicRamificationNumberOfUniqueExtension_ge
          (base := base) (target := target) huniq (m + 1)
            (sigma : Gal(L/K))).1 hmem
      exact hhigh (by simpa [i, Nat.add_assoc] using hge)
    have hdepth : (truncatedLowerDepth F) m sigma = k - 1 := by
      rw [truncatedLowerDepth]
      have hfilter :
          (Finset.range m).filter
              (fun j => (sigma : Gal(L/K)) ∈ F.lower (j + 1)) =
            Finset.range (k - 1) := by
        ext j
        simp only [Finset.mem_filter, Finset.mem_range]
        have hthreshold :
            ((sigma : Gal(L/K)) ∈ F.lower (j + 1)) ↔ j + 2 ≤ k := by
          change
            ((sigma : Gal(L/K)) ∈ lowerRamificationGroup
              (base := base) (target := target) huniq ((j + 1 : ℕ) : ℝ)) ↔
                j + 2 ≤ k
          rw [mem_lowerRamificationGroup_nat_iff_intrinsicRamificationNumberOfUniqueExtension_ge
            (base := base) (target := target) huniq]
          change (((j + 1 + 1 : ℕ) : ℕ∞) ≤ i) ↔ j + 2 ≤ k
          rw [← hk]
          norm_cast
        rw [hthreshold]
        omega
      rw [hfilter, Finset.card_range]
    have htrunc : truncateENatAtDVF i (s + 1) = k := by
      rw [← hk, truncateENatAtDVF_coe, min_eq_left]
      have : (k : ℝ) ≤ m + 1 := by exact_mod_cast hk_upper
      linarith
    rw [htrunc, hdepth]
    rw [ite_eq_right hmem, mul_zero, add_zero]
    exact_mod_cast (by omega : k = 1 + (k - 1))
theorem

truncate_intrinsicRamificationNumberOfUniqueExtension_eq_zero_of_not_mem_inertia

L178 ↗
RamificationTheory.HilbertRamification.Higher.truncate_intrinsicRamificationNumberOfUniqueExtension_eq_zero_of_not_mem_inertia
Documentation

States the theorem truncate_intrinsicRamificationNumberOfUniqueExtension_eq_zero_of_not_mem_inertia.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
local instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : Decidable (sigma ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem truncate_intrinsicRamificationNumberOfUniqueExtension_eq_zero_of_not_mem_inertia
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {s : ℝ} (hs : -1 ≤ s) {sigma : Gal(L/K)}
    (hsigma : sigma ∉ (lowerRamificationFiltrationOfUniqueExtension
      (base := base) (target := target) huniq).lower 0) :
    truncateENatAtDVF
        (intrinsicRamificationNumberOfUniqueExtension
          (base := base) (target := target) huniq sigma) (s + 1) = 0
theorem

sum_truncate_intrinsicRamificationNumberOfUniqueExtension_eq_sum_inertia

L204 ↗
RamificationTheory.HilbertRamification.Higher.sum_truncate_intrinsicRamificationNumberOfUniqueExtension_eq_sum_inertia
Documentation

States the theorem sum_truncate_intrinsicRamificationNumberOfUniqueExtension_eq_sum_inertia.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
local instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : Decidable (sigma ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem sum_truncate_intrinsicRamificationNumberOfUniqueExtension_eq_sum_inertia
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {s : ℝ} (hs : -1 ≤ s) :
    (∑ sigma : Gal(L/K), truncateENatAtDVF
      (intrinsicRamificationNumberOfUniqueExtension
        (base := base) (target := target) huniq sigma) (s + 1)) =
    ∑ sigma : (lowerRamificationFiltrationOfUniqueExtension
        (base := base) (target := target) huniq).lower 0,
      truncateENatAtDVF
        (intrinsicRamificationNumberOfUniqueExtension
          (base := base) (target := target) huniq (sigma : Gal(L/K))) (s + 1)
theorem

sum_inertia_truncate_intrinsicRamificationNumberOfUniqueExtension_eq_intrinsic

L246 ↗
RamificationTheory.HilbertRamification.Higher.sum_inertia_truncate_intrinsicRamificationNumberOfUniqueExtension_eq_intrinsic
Documentation

States the theorem sum_inertia_truncate_intrinsicRamificationNumberOfUniqueExtension_eq_intrinsic.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
local instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : Decidable (sigma ∈ H) :=
  Classical.propDecidable _
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  card_lower_succ_eq_sum_indicator
  truncatedLowerDepth
) in
Lean source · statement
theorem sum_inertia_truncate_intrinsicRamificationNumberOfUniqueExtension_eq_intrinsic
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (m : ℕ) {s : ℝ} (hms : (m : ℝ) ≤ s) (hsm : s ≤ m + 1) :
    (∑ sigma : (lowerRamificationFiltrationOfUniqueExtension
        (base := base) (target := target) huniq).lower 0,
      truncateENatAtDVF
        (intrinsicRamificationNumberOfUniqueExtension
          (base := base) (target := target) huniq (sigma : Gal(L/K))) (s + 1)) =
      Nat.card ((lowerRamificationFiltrationOfUniqueExtension
        (base := base) (target := target) huniq).lower 0) +
      (∑ sigma : (lowerRamificationFiltrationOfUniqueExtension
          (base := base) (target := target) huniq).lower 0,
        ((truncatedLowerDepth (lowerRamificationFiltrationOfUniqueExtension (base := base)
          (target := target) huniq)) m sigma : ℝ)) +
      (s - m) * Nat.card ((lowerRamificationFiltrationOfUniqueExtension
        (base := base) (target := target) huniq).lower (m + 1))
theorem

herbrandFunctionOfUniqueExtension_eq_intrinsicRamificationNumber_sum

L298 ↗
RamificationTheory.HilbertRamification.Higher.herbrandFunctionOfUniqueExtension_eq_intrinsicRamificationNumber_sum
Documentation

The Herbrand-function sum formula under the stated discretely valued field assumptions. The generator from the monogenic integral-generator theorem is internal to the canonical ramification number, so this endpoint has no generator hypothesis.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
local instance galoisFintype : Fintype Gal(L/K) :=
  Fintype.ofFinite Gal(L/K)
local instance subgroupFintype (H : Subgroup Gal(L/K)) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K)) : Decidable (sigma ∈ H) :=
  Classical.propDecidable _
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandFunction
  herbrandFunction_eq_depth_sum_of_mem_Icc
  herbrandFunction_of_nonpos
) in
Lean source · statement
theorem herbrandFunctionOfUniqueExtension_eq_intrinsicRamificationNumber_sum
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {s : ℝ} (hs : -1 ≤ s) :
    herbrandFunctionOfUniqueExtension
        (base := base) (target := target) huniq s =
      (1 / Nat.card ((lowerRamificationFiltrationOfUniqueExtension
        (base := base) (target := target) huniq).lower 0) : ℝ) *
        (∑ sigma : Gal(L/K), truncateENatAtDVF
          (intrinsicRamificationNumberOfUniqueExtension
            (base := base) (target := target) huniq sigma) (s + 1)) - 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.