NYLL
Module

Average.lean

Nyll.ValuedFieldTheory.Ramification.Herbrand.Average
17 declarations indexed from sourceView source ↗

Module documentation

The fibre average in Herbrand's theorem

This file formalizes the remaining finite-group calculation in the Herbrand quotient theorem. For a normal subgroup H, the depth on G defines the lower filtration

H_s = {τ : H | s + 1 ≤ depth τ}.

For a nonidentity class in G ⧸ H, all depths in its fibre are finite, so their normalized average is a definition rather than an assumed quotient depth. The main theorem identifies this average, at a representative of maximal depth, with the Herbrand function of the above filtration. The valued-field equality between this average and the actual quotient depth is the separate input of the quotient-depth identity.

Imports3
Imported by2

Declarations

theorem

depth_inv

L43 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.depth_inv
Documentation

States the theorem depth_inv.

Source context 7 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
Lean source · statement
theorem depth_inv (σ : G) : D.depth σ⁻¹ = D.depth σ
instance

averageSubgroupFintype

L55 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.averageSubgroupFintype
Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
Lean source · statement
instance averageSubgroupFintype [Finite G] : Fintype H
instance

averageQuotientFiberFintype

L58 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.averageQuotientFiberFintype
Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
Lean source · statement
instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q)
def

depthLowerSubgroup

L64 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.depthLowerSubgroup
Documentation

The nth lower group of H cut out by the ambient depth: H_n = {τ | n + 1 ≤ depth τ}.

Source context 10 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
Lean source · full declaration
def depthLowerSubgroup (n : ℕ) : Subgroup H where
  carrier := {τ | WithTop.some (n + 1) ≤ D.depth (τ : G)}
  one_mem' := by simp [D.depth_one]
  mul_mem' := by
    intro σ τ hσ hτ
    exact le_trans (le_min hσ hτ) (D.depth_mul_ge_min (σ : G) (τ : G))
  inv_mem' := by
    intro σ hσ
    simpa [D.depth_inv] using hσ
theorem

mem_depthLowerSubgroup_iff

L76 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.mem_depthLowerSubgroup_iff
Documentation

States the theorem mem_depthLowerSubgroup_iff.

Source context 11 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
omit [H.Normal] in
Lean source · statement
theorem mem_depthLowerSubgroup_iff (n : ℕ) (τ : H) :
    τ ∈ D.depthLowerSubgroup H n ↔
      WithTop.some (n + 1) ≤ D.depth (τ : G)
def

depthLowerFiltration

L83 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.depthLowerFiltration
Documentation

The exact lower filtration on H induced by D. Conjugation invariance of the depth supplies normality of every level.

Source context 10 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
Lean source · full declaration
def depthLowerFiltration : AntitoneNormalSubgroupFiltration H where
  lower := D.depthLowerSubgroup H
  lower_normal := by
    intro n
    constructor
    intro τ hτ σ
    change WithTop.some (n + 1) ≤ D.depth (((σ * τ * σ⁻¹ : H) : G))
    rw [show (((σ * τ * σ⁻¹ : H) : G)) =
        (σ : G) * (τ : G) * (σ : G)⁻¹ by rfl, D.depth_conj]
    exact hτ
  antitone := fun {m n} hmn τ hτ => by
    change WithTop.some (m + 1) ≤ D.depth (τ : G)
    have hmn' : m + 1 ≤ n + 1 := Nat.add_le_add_right hmn 1
    exact le_trans (WithTop.coe_le_coe.2 hmn') hτ
theorem

depthLowerFiltration_lower

L100 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.depthLowerFiltration_lower
Documentation

States the theorem depthLowerFiltration_lower.

Source context 11 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
omit [H.Normal] in
Lean source · statement
theorem depthLowerFiltration_lower (n : ℕ) :
    (D.depthLowerFiltration H).lower n = D.depthLowerSubgroup H n
def

depthRamificationIndex

L106 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.depthRamificationIndex
Documentation

The ramification index in the purely group-theoretic calculation, namely |H_0|.

Source context 10 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
Lean source · statement
def depthRamificationIndex [Finite G] : ℕ
def

quotientFiberAverage

L111 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.quotientFiberAverage
Documentation

The actual normalized average of the finite depths in a nontrivial quotient fibre. No quotient-depth datum is included in this definition.

Source context 10 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
Lean source · statement
def quotientFiberAverage [Fintype G] {q : G ⧸ H} (hq : q ≠ 1) : ℝ
theorem

truncatedLowerDepth_add_one

L120 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.truncatedLowerDepth_add_one
Documentation

States the theorem truncatedLowerDepth_add_one.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
omit [H.Normal] in
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  truncatedLowerDepth
) in
Lean source · statement
theorem truncatedLowerDepth_add_one (n : ℕ)
    (τ : (D.depthLowerFiltration H).lower 0) :
    (truncatedLowerDepth (D.depthLowerFiltration H)) n τ + 1 =
      WithTop.untopD (α := ℕ) 0
        (min (D.depth ((τ : H) : G)) (WithTop.some (n + 1)))
theorem

depth_eq_zero_of_not_mem_lower_zero

L168 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.depth_eq_zero_of_not_mem_lower_zero
Documentation

States the theorem depth_eq_zero_of_not_mem_lower_zero.

Source context 11 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
omit [H.Normal] in
Lean source · statement
theorem depth_eq_zero_of_not_mem_lower_zero (τ : H)
    (hτ : τ ∉ (D.depthLowerFiltration H).lower 0) :
    D.depth (τ : G) = (0 : ℕ)
theorem

sum_min_depth_eq_card_add_truncated

L191 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.sum_min_depth_eq_card_add_truncated
Documentation

The truncation sum over all of H is the inertia-cardinality constant plus the Herbrand depth sum over H_0.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
omit [H.Normal] in
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  truncatedLowerDepth
) in
Lean source · statement
theorem sum_min_depth_eq_card_add_truncated (n : ℕ) [Finite G] :
    (∑ τ : H,
        (WithTop.untopD (α := ℕ) 0
          (min (D.depth (τ : G)) (WithTop.some (n + 1))) : ℝ)) =
      D.depthRamificationIndex H +
        ∑ τ : (D.depthLowerFiltration H).lower 0,
          ((truncatedLowerDepth (D.depthLowerFiltration H)) n τ : ℝ)
theorem

quotientFiberAverage_sub_one_eq_herbrandValueNat_of_depth_eq_succ

L251 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.quotientFiberAverage_sub_one_eq_herbrandValueNat_of_depth_eq_succ
Documentation

The natural-argument calculation at the heart of Herbrand's theorem. For a maximal representative of depth n + 1, the normalized fibre average minus one is the Herbrand function of H at n.

The proof uses the maximal-representative fibre-sum identity and exactly the integral Herbrand sum formula.

Source context 11 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandValueNat
  herbrandValueNat_eq_depth_sum
  truncatedLowerDepth
) in
Lean source · statement
theorem quotientFiberAverage_sub_one_eq_herbrandValueNat_of_depth_eq_succ
    [Fintype G] {q : G ⧸ H} (hq : q ≠ 1) {σ : G}
    (hσq : QuotientGroup.mk' H σ = q)
    (hmax : ∀ γ : G, QuotientGroup.mk' H γ = q →
      D.depth γ ≤ D.depth σ)
    (n : ℕ) (hdepth : D.depth σ = WithTop.some (n + 1)) :
    D.quotientFiberAverage H hq - 1 =
      (herbrandValueNat (D.depthLowerFiltration H)) n
theorem

quotientFiberAverage_eq_zero_of_maximal_depth_zero

L306 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.quotientFiberAverage_eq_zero_of_maximal_depth_zero
Documentation

The missing m = 0 endpoint of the fibre calculation. If a maximal representative has depth zero, every element of its fibre has depth zero, so the actual normalized average is zero.

Source context 10 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
Lean source · statement
theorem quotientFiberAverage_eq_zero_of_maximal_depth_zero
    [Fintype G] {q : G ⧸ H} (hq : q ≠ 1) {σ : G}
    (hmax : ∀ γ : G, QuotientGroup.mk' H γ = q →
      D.depth γ ≤ D.depth σ)
    (hdepth : D.depth σ = WithTop.some 0) :
    D.quotientFiberAverage H hq = 0
theorem

quotientFiberAverage_sub_one_eq_herbrandFunction_of_maximal

L334 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.quotientFiberAverage_sub_one_eq_herbrandFunction_of_maximal
Documentation

The fibre-average identity in the exact form used in the Herbrand quotient theorem. The finite natural depth of the chosen maximal representative is used in the real argument m - 1, including the endpoint m = 0.

Source context 11 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandFunction
) in
Lean source · statement
theorem quotientFiberAverage_sub_one_eq_herbrandFunction_of_maximal
    [Fintype G] {q : G ⧸ H} (hq : q ≠ 1) {σ : G}
    (hσq : QuotientGroup.mk' H σ = q)
    (hmax : ∀ γ : G, QuotientGroup.mk' H γ = q →
      D.depth γ ≤ D.depth σ) :
    D.quotientFiberAverage H hq - 1 =
      (herbrandFunction (D.depthLowerFiltration H))
        ((D.quotientFiberDepth H hq ⟨σ, hσq⟩ : ℝ) - 1)
theorem

quotientFiberAverage_ge_herbrandFunction_add_one_iff_exists

L374 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.quotientFiberAverage_ge_herbrandFunction_add_one_iff_exists
Documentation

Natural-threshold form of the last equivalence in the proof of Herbrand's theorem. The normalized average is at least η_H(s) + 1 exactly when its quotient fibre contains an element of depth at least s + 1.

Source context 11 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandFunction
  herbrandFunction_strictMono
) in
Lean source · statement
theorem quotientFiberAverage_ge_herbrandFunction_add_one_iff_exists
    [Fintype G] {q : G ⧸ H} (hq : q ≠ 1) {σ : G}
    (hσq : QuotientGroup.mk' H σ = q)
    (hmax : ∀ γ : G, QuotientGroup.mk' H γ = q →
      D.depth γ ≤ D.depth σ)
    (s : ℕ) :
    D.quotientFiberAverage H hq ≥
        (herbrandFunction (D.depthLowerFiltration H)) s + 1 ↔
      ∃ γ : QuotientFiber H q,
        WithTop.some (s + 1) ≤ D.depth (γ : G)
theorem

exists_maximal_representative_quotientFiberAverage

L427 ↗
RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.exists_maximal_representative_quotientFiberAverage
Documentation

Every nontrivial quotient fibre admits a maximal representative for which the Herbrand fibre-average identity holds.

Source context 11 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
namespace NonarchimedeanDepth
variable {G : Type u} [Group G]
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance averageSubgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance averageQuotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration (
  herbrandFunction
) in
Lean source · statement
theorem exists_maximal_representative_quotientFiberAverage [Fintype G]
    {q : G ⧸ H} (hq : q ≠ 1) :
    ∃ σ : G, ∃ hσq : QuotientGroup.mk' H σ = q,
      (∀ γ : G, QuotientGroup.mk' H γ = q →
        D.depth γ ≤ D.depth σ) ∧
      D.quotientFiberAverage H hq - 1 =
        (herbrandFunction (D.depthLowerFiltration H))
          ((D.quotientFiberDepth H hq ⟨σ, hσq⟩ : ℝ) - 1)

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