NYLL
Module

Function.lean

Nyll.ValuedFieldTheory.Ramification.Herbrand.Function
41 declarations indexed from sourceView source ↗

Module documentation

The Herbrand function

This file supplies the group-theoretic content of the Herbrand-function sum formula. The old AntitoneNormalSubgroupFiltration.herbrandStep starts with |G₀| / |G₀|; the normalized Herbrand function has, on (m,m+1), slope |Gₘ₊₁| / |G₀|. We therefore deliberately use a new, shifted definition here.

The definition is made on all of ℝ. Below zero it is the identity, so its restriction to [-1,∞) is exactly the normalized function on this range.

Imports6
Imported by5

Declarations

instance

subgroupFintype

L39 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subgroupFintype
Source context 6 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
Lean source · statement
instance subgroupFintype (H : Subgroup G) : Fintype H
instance

subgroupMembershipDecidable

L42 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subgroupMembershipDecidable
Source context 7 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
Lean source · statement
instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H)
def

herbrandSlope

L48 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandSlope
Documentation

The slope of the Herbrand function on (i,i+1). This is the shifted quantity |G_(i+1)| / |G_0|, not the pre-existing herbrandStep i.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
def herbrandSlope (i : ℕ) : ℝ
def

herbrandValueNat

L52 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandValueNat
Documentation

The value of the normalized Herbrand function at a natural number.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
def herbrandValueNat (n : ℕ) : ℝ
theorem

herbrandValueNat_zero

L57 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandValueNat_zero
Documentation

States the theorem herbrandValueNat_zero.

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
omit [Finite G] in
Lean source · statement
theorem herbrandValueNat_zero : (herbrandValueNat F) 0 = 0
theorem

herbrandValueNat_succ

L62 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandValueNat_succ
Documentation

States the theorem herbrandValueNat_succ.

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
omit [Finite G] in
Lean source · statement
theorem herbrandValueNat_succ (n : ℕ) :
    (herbrandValueNat F) (n + 1) =
      (herbrandValueNat F) n + (herbrandSlope F) n
theorem

herbrandSlope_pos

L68 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandSlope_pos
Documentation

States the theorem herbrandSlope_pos.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandSlope_pos (i : ℕ) :
    0 < (herbrandSlope F) i
theorem

herbrandSlope_nonneg

L75 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandSlope_nonneg
Documentation

States the theorem herbrandSlope_nonneg.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandSlope_nonneg (i : ℕ) :
    0 ≤ (herbrandSlope F) i
theorem

one_div_card_le_herbrandSlope

L80 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.one_div_card_le_herbrandSlope
Documentation

States the theorem one_div_card_le_herbrandSlope.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem one_div_card_le_herbrandSlope (i : ℕ) :
    (1 : ℝ) / Nat.card (F.lower 0) ≤ (herbrandSlope F) i
theorem

herbrandValueNat_nonneg

L89 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandValueNat_nonneg
Documentation

States the theorem herbrandValueNat_nonneg.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandValueNat_nonneg (n : ℕ) :
    0 ≤ (herbrandValueNat F) n
theorem

nat_div_card_le_herbrandValueNat

L94 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.nat_div_card_le_herbrandValueNat
Documentation

States the theorem nat_div_card_le_herbrandValueNat.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem nat_div_card_le_herbrandValueNat (n : ℕ) :
    (n : ℝ) / Nat.card (F.lower 0) ≤ (herbrandValueNat F) n
theorem

herbrandValueNat_strictMono

L105 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandValueNat_strictMono
Documentation

States the theorem herbrandValueNat_strictMono.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandValueNat_strictMono : StrictMono (herbrandValueNat F)
def

herbrandFunction

L112 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction
Documentation

The Herbrand-function sum formula, in its explicit piecewise-linear form.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
def herbrandFunction (s : ℝ) : ℝ
theorem

herbrandFunction_eq_of_card_lower_eq

L124 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_eq_of_card_lower_eq
Documentation

The Herbrand function depends only on the cardinalities of the lower groups. This comparison lemma is useful when a Galois group is replaced by an isomorphic subgroup or quotient model.

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
omit [Finite G] in
Lean source · statement
theorem herbrandFunction_eq_of_card_lower_eq
    {G' : Type*} [Group G']
    (F' : AntitoneNormalSubgroupFiltration G')
    (hcard : ∀ n : ℕ, Nat.card (F.lower n) = Nat.card (F'.lower n))
    (s : ℝ) :
    (herbrandFunction F) s = (herbrandFunction F') s
theorem

herbrandFunction_of_nonpos

L144 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_of_nonpos
Documentation

States the theorem herbrandFunction_of_nonpos.

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
omit [Finite G] in
Lean source · statement
theorem herbrandFunction_of_nonpos {s : ℝ} (hs : s ≤ 0) :
    (herbrandFunction F) s = s
theorem

herbrandFunction_zero

L153 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_zero
Documentation

States the theorem herbrandFunction_zero.

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
omit [Finite G] in
Lean source · statement
theorem herbrandFunction_zero : (herbrandFunction F) 0 = 0
theorem

herbrandFunction_neg_one

L158 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_neg_one
Documentation

States the theorem herbrandFunction_neg_one.

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
omit [Finite G] in
Lean source · statement
theorem herbrandFunction_neg_one : (herbrandFunction F) (-1) = -1
theorem

herbrandFunction_of_floor

L163 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_of_floor
Documentation

States the theorem herbrandFunction_of_floor.

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
omit [Finite G] in
Lean source · statement
theorem herbrandFunction_of_floor {s : ℝ} (hs : 0 ≤ s) (m : ℕ)
    (hm : ⌊s⌋₊ = m) :
    (herbrandFunction F) s = (herbrandValueNat F) m +
      (s - (m : ℝ)) * (herbrandSlope F) m
theorem

herbrandFunction_nat

L171 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_nat
Documentation

States the theorem herbrandFunction_nat.

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
omit [Finite G] in
Lean source · statement
theorem herbrandFunction_nat (n : ℕ) :
    (herbrandFunction F) (n : ℝ) = (herbrandValueNat F) n
theorem

herbrandFunction_one_eq

L176 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_one_eq
Documentation

The first Herbrand value is the ratio of the first two lower-group orders.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandFunction_one_eq :
    (herbrandFunction F) 1 =
      (Nat.card (F.lower 1) : ℝ) / Nat.card (F.lower 0)
theorem

herbrandFunction_one_pos_le_one

L185 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_one_pos_le_one
Documentation

The first Herbrand value lies strictly above zero and at most one.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandFunction_one_pos_le_one :
    0 < (herbrandFunction F) 1 ∧ (herbrandFunction F) 1 ≤ 1
theorem

herbrandFunction_eq_on_Ico

L209 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_eq_on_Ico
Documentation

The defining affine formula on a half-open unit interval.

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
omit [Finite G] in
Lean source · statement
theorem herbrandFunction_eq_on_Ico (m : ℕ) {s : ℝ}
    (hms : (m : ℝ) ≤ s) (hsm : s < m + 1) :
    (herbrandFunction F) s = (herbrandValueNat F) m +
      (s - (m : ℝ)) * (herbrandSlope F) m
theorem

herbrandFunction_eq_on_Icc

L219 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_eq_on_Icc
Documentation

The closed-interval form. At the right endpoint the two adjacent affine expressions agree.

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
omit [Finite G] in
Lean source · statement
theorem herbrandFunction_eq_on_Icc (m : ℕ) {s : ℝ}
    (hms : (m : ℝ) ≤ s) (hsm : s ≤ m + 1) :
    (herbrandFunction F) s = (herbrandValueNat F) m +
      (s - (m : ℝ)) * (herbrandSlope F) m
theorem

herbrandFunction_eq_card_sum_of_mem_Icc

L231 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_eq_card_sum_of_mem_Icc
Documentation

The displayed formula immediately preceding the Herbrand-function sum formula.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandFunction_eq_card_sum_of_mem_Icc (m : ℕ) {s : ℝ}
    (hms : (m : ℝ) ≤ s) (hsm : s ≤ m + 1) :
    (herbrandFunction F) s =
      ((∑ i ∈ Finset.range m, (Nat.card (F.lower (i + 1)) : ℝ)) +
          (s - m) * Nat.card (F.lower (m + 1))) /
        Nat.card (F.lower 0)
theorem

herbrandFunction_nonneg

L246 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_nonneg
Documentation

States the theorem herbrandFunction_nonneg.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandFunction_nonneg {s : ℝ} (hs : 0 ≤ s) :
    0 ≤ (herbrandFunction F) s
theorem

herbrandFunction_strictMono

L255 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_strictMono
Documentation

The Herbrand function is strictly increasing, as asserted after the Herbrand quotient theorem.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandFunction_strictMono : StrictMono (herbrandFunction F)
theorem

herbrandFunction_surjective

L295 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_surjective
Documentation

States the theorem herbrandFunction_surjective.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandFunction_surjective : Function.Surjective (herbrandFunction F)
theorem

continuous_herbrandFunction

L347 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.continuous_herbrandFunction
Documentation

Continuity of the piecewise-linear Herbrand function.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem continuous_herbrandFunction : Continuous (herbrandFunction F)
def

inverseHerbrandFunction

L352 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.inverseHerbrandFunction
Documentation

The inverse Herbrand function ψ.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
def inverseHerbrandFunction (t : ℝ) : ℝ
theorem

herbrandFunction_inverseHerbrandFunction

L356 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_inverseHerbrandFunction
Documentation

States the theorem herbrandFunction_inverseHerbrandFunction.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandFunction_inverseHerbrandFunction (t : ℝ) :
    (herbrandFunction F) ((inverseHerbrandFunction F) t) = t
theorem

inverseHerbrandFunction_herbrandFunction

L361 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.inverseHerbrandFunction_herbrandFunction
Documentation

States the theorem inverseHerbrandFunction_herbrandFunction.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem inverseHerbrandFunction_herbrandFunction (s : ℝ) :
    (inverseHerbrandFunction F) ((herbrandFunction F) s) = s
theorem

inverseHerbrandFunction_strictMono

L366 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.inverseHerbrandFunction_strictMono
Documentation

States the theorem inverseHerbrandFunction_strictMono.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem inverseHerbrandFunction_strictMono : StrictMono (inverseHerbrandFunction F)
theorem

inverseHerbrandFunction_surjective

L372 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.inverseHerbrandFunction_surjective
Documentation

States the theorem inverseHerbrandFunction_surjective.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem inverseHerbrandFunction_surjective : Function.Surjective (inverseHerbrandFunction F)
theorem

continuous_inverseHerbrandFunction

L377 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.continuous_inverseHerbrandFunction
Documentation

States the theorem continuous_inverseHerbrandFunction.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem continuous_inverseHerbrandFunction : Continuous (inverseHerbrandFunction F)
def

herbrandOrderIso

L383 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandOrderIso
Documentation

The mutually inverse Herbrand functions as an order isomorphism of the real line. Its canonical form uses the restriction to [-1,∞).

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · full declaration
def herbrandOrderIso : ℝ ≃o ℝ where
  toFun := (herbrandFunction F)
  invFun := (inverseHerbrandFunction F)
  left_inv := (inverseHerbrandFunction_herbrandFunction F)
  right_inv := (herbrandFunction_inverseHerbrandFunction F)
  map_rel_iff' := (herbrandFunction_strictMono F).le_iff_le
theorem

herbrandFunction_mem_Ici_neg_one_iff

L391 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_mem_Ici_neg_one_iff
Documentation

States the theorem herbrandFunction_mem_Ici_neg_one_iff.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandFunction_mem_Ici_neg_one_iff {s : ℝ} :
    (herbrandFunction F) s ∈ Set.Ici (-1) ↔ s ∈ Set.Ici (-1)
theorem

inverseHerbrandFunction_mem_Ici_neg_one_iff

L399 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.inverseHerbrandFunction_mem_Ici_neg_one_iff
Documentation

States the theorem inverseHerbrandFunction_mem_Ici_neg_one_iff.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem inverseHerbrandFunction_mem_Ici_neg_one_iff {t : ℝ} :
    (inverseHerbrandFunction F) t ∈ Set.Ici (-1) ↔ t ∈ Set.Ici (-1)
def

truncatedLowerDepth

L412 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.truncatedLowerDepth
Documentation

The number of positive lower-numbered levels, truncated at n, through which an inertia element survives. For a classical depth i(σ), this is min (i(σ) - 1) n.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
def truncatedLowerDepth (n : ℕ) (σ : F.lower 0) : ℕ
theorem

card_lower_succ_eq_sum_indicator

L417 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.card_lower_succ_eq_sum_indicator
Documentation

States the theorem card_lower_succ_eq_sum_indicator.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · full declaration
theorem card_lower_succ_eq_sum_indicator (i : ℕ) :
    Nat.card (F.lower (i + 1)) =
      ∑ σ : F.lower 0, if (σ : G) ∈ F.lower (i + 1) then 1 else 0 := by
  classical
  let ι : F.lower (i + 1) → F.lower 0 := fun σ =>
    ⟨(σ : G), F.antitone (Nat.zero_le (i + 1)) σ.property⟩
  have hι : Function.Injective ι := by
    intro σ τ h
    exact Subtype.ext (congrArg (fun x : F.lower 0 => (x : G)) h)
  rw [Nat.card_eq_fintype_card]
  change Finset.univ.card =
    ∑ σ : F.lower 0, if (σ : G) ∈ F.lower (i + 1) then 1 else 0
  rw [← Finset.card_image_of_injective Finset.univ hι]
  rw [show (∑ σ : F.lower 0,
      if (σ : G) ∈ F.lower (i + 1) then 1 else 0) =
      (Finset.univ.filter fun σ : F.lower 0 =>
        (σ : G) ∈ F.lower (i + 1)).card by simp]
  congr 1
  ext σ
  simp only [Finset.mem_image, Finset.mem_univ, true_and, Finset.mem_filter]
  constructor
  · rintro ⟨τ, hτ⟩
    have hcoe : (τ : G) = (σ : G) :=
      congrArg (fun z : F.lower 0 => (z : G)) hτ
    rw [← hcoe]
    exact τ.property
  · intro hσ
    refine ⟨⟨(σ : G), hσ⟩, ?_⟩
    exact Subtype.ext rfl
theorem

herbrandValueNat_eq_depth_sum

L451 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandValueNat_eq_depth_sum
Documentation

The Herbrand-function sum formula at an integral argument, in the intrinsic depth form. It is the defining identity g₀⁻¹ ∑σ (min {i(σ), n+1} - 1) with the truncated depth expressed directly by membership in the lower groups.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandValueNat_eq_depth_sum (n : ℕ) :
    (herbrandValueNat F) n =
      (∑ σ : F.lower 0, ((truncatedLowerDepth F) n σ : ℝ)) /
        Nat.card (F.lower 0)
theorem

herbrandFunction_eq_depth_sum_of_mem_Icc

L474 ↗
RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunction_eq_depth_sum_of_mem_Icc
Documentation

The Herbrand-function sum formula for a general real argument in [m,m+1]. The first sum is the intrinsic version of ∑σ (min {i(σ),m+1}-1); the last term records the elements surviving in G_(m+1) for the fractional part.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] [Finite G]
variable (F : AntitoneNormalSubgroupFiltration G)
local instance subgroupFintype (H : Subgroup G) : Fintype H :=
  Fintype.ofFinite H
local instance subgroupMembershipDecidable (H : Subgroup G) (x : G) :
    Decidable (x ∈ H) :=
  Classical.propDecidable _
Lean source · statement
theorem herbrandFunction_eq_depth_sum_of_mem_Icc (m : ℕ) {s : ℝ}
    (hms : (m : ℝ) ≤ s) (hsm : s ≤ m + 1) :
    (herbrandFunction F) s =
      ((∑ σ : F.lower 0, ((truncatedLowerDepth F) m σ : ℝ)) +
          (s - m) * Nat.card (F.lower (m + 1))) /
        Nat.card (F.lower 0)

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