Module

HerbrandFunction.lean

Nyll.ClassFieldTheory.Definitions.HasseArf.HerbrandFunction

1 declaration indexed from sourceView source ↗

Module documentation

The real Herbrand function from integral lower groups

Between consecutive nonnegative integers, the function interpolates linearly between the rational Herbrand values. On the negative half-line it is the identity. Its slope on (m, m + 1) is |G_(m+1)| / |G_0|.

Imports4

Nyll.ClassFieldTheory.Definitions.HasseArf.HerbrandFunctionAtLowerIndex
Mathlib.Algebra.Order.Floor.Ring
Mathlib.Algebra.Order.Archimedean.Real.Basic
Mathlib.Basic.Real.Basic

Imported by7

def

herbrandFunction

L29 ↗

ClassFieldTheory.herbrandFunction

Documentation

The piecewise-linear Herbrand function attached to the lower ramification groups of a valuation subring. This definition itself does not require the extension to be finite.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

def herbrandFunction
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (A : ValuationSubring L) (s : ℝ) : ℝ

Module documentation

The real Herbrand function from integral lower groups

Declarations

herbrandFunction