Module

SeriesTerms.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.SeriesTerms

71 declarations indexed from sourceView source ↗

Module documentation

Defines the logarithm and exponential series terms and proves the valuation estimates used in their convergence arguments.

Exponential-series terms

Imports4

Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Mathlib.Topology.Algebra.Valued.WithZeroMulInt
Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.FormalProduct
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.FieldUnitDecomposition

Imported by5

def

logOnePlusSeriesOfWithZeroValuation

L79 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.logOnePlusSeriesOfWithZeroValuation

Documentation

The value of the principal-unit logarithm series, formed as a topological sum in the topology attached to v.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

def logOnePlusSeriesOfWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (x : Kˣ) (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) : K

def

powerSeries_log_coeff_mul_pow_eq_signedLogSeriesTermField

L111 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.powerSeries_log_coeff_mul_pow_eq_signedLogSeriesTermField

Documentation

The n-th field logarithm-series term is the evaluation of the (n+1)-st coefficient of the formal series log(1+X) at x.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem powerSeries_log_coeff_mul_pow_eq_signedLogSeriesTermField
    [Algebra ℚ K] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (n : ℕ) :
    PowerSeries.coeff (n + 1) (PowerSeries.log K) *
        x ^ (n + 1) =
      signedLogSeriesTermField x hnK n

def

logOnePlusPartialSumField_zero

L137 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.logOnePlusPartialSumField_zero

Documentation

Establishes the identity logOnePlusPartialSumField x hnK 0 = 0.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem logOnePlusPartialSumField_zero
    (x : K) (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) :
    logOnePlusPartialSumField x hnK 0 = 0

theorem

powerSeries_log_partial_eval_eq_logOnePlusPartialSumField

L150 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.powerSeries_log_partial_eval_eq_logOnePlusPartialSumField

Documentation

Finite logarithm polynomials are exactly the finite evaluations of the formal power series log(1+X) with the constant term omitted.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem powerSeries_log_partial_eval_eq_logOnePlusPartialSumField
    [Algebra ℚ K] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (N : ℕ) :
    (∑ n ∈ Finset.range N,
        PowerSeries.coeff (n + 1) (PowerSeries.log K) *
          x ^ (n + 1)) =
      logOnePlusPartialSumField x hnK N

def

logOnePlusSeriesFieldOfWithZeroValuation

L163 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.logOnePlusSeriesFieldOfWithZeroValuation

Documentation

Field-element value of the principal-unit logarithm series.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

def logOnePlusSeriesFieldOfWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (x : K) (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) : K

def

formalExpPowerSeries_coeff_mul_pow_eq_expSeriesTermField

L225 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalExpPowerSeries_coeff_mul_pow_eq_expSeriesTermField

Documentation

The n-th field exponential-series term is the evaluation of the n-th coefficient of mathlib's formal exponential series at x.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem formalExpPowerSeries_coeff_mul_pow_eq_expSeriesTermField
    [Algebra ℚ K] (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0)) (n : ℕ) :
    PowerSeries.coeff n (PowerSeries.exp K) * x ^ n =
      expSeriesTermField x hnK n

def

formalExpPowerSeries_partial_eval_eq_expSeriesPartialSumField

L253 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.formalExpPowerSeries_partial_eval_eq_expSeriesPartialSumField

Documentation

Finite exponential polynomials are exactly the finite evaluations of mathlib's formal exponential series.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem formalExpPowerSeries_partial_eval_eq_expSeriesPartialSumField
    [Algebra ℚ K] (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0)) (N : ℕ) :
    (∑ n ∈ Finset.range N,
        PowerSeries.coeff n (PowerSeries.exp K) * x ^ n) =
      expSeriesPartialSumField x hnK N

theorem

expSeriesTermField_add_eq_sum_antidiagonal

L266 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesTermField_add_eq_sum_antidiagonal

Documentation

Coefficientwise Cauchy product for the local exponential terms, inherited from mathlib's formal identity exp(xX) * exp(yX) = exp((x+y)X).

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem expSeriesTermField_add_eq_sum_antidiagonal
    [Algebra ℚ K] (x y : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0)) (n : ℕ) :
    expSeriesTermField (x + y) hnK n =
      ∑ ij ∈ Finset.antidiagonal n,
        expSeriesTermField x hnK ij.1 *
          expSeriesTermField y hnK ij.2

theorem

expSeriesTermField_add_eq_sum_range_succ

L308 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesTermField_add_eq_sum_range_succ

Documentation

Range-indexed form of the finite Cauchy-product formula for each coefficient of the local exponential series.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem expSeriesTermField_add_eq_sum_range_succ
    [Algebra ℚ K] (x y : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0)) (n : ℕ) :
    expSeriesTermField (x + y) hnK n =
      ∑ i ∈ Finset.range n.succ,
        expSeriesTermField x hnK i *
          expSeriesTermField y hnK (n - i)

theorem

expSeriesPartialSumField_add_eq_sum_range_antidiagonal

L321 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesPartialSumField_add_eq_sum_range_antidiagonal

Documentation

Finite partial sums of exp(x+y) expanded by the Cauchy-product coefficients coming from the formal exponential identity.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem expSeriesPartialSumField_add_eq_sum_range_antidiagonal
    [Algebra ℚ K] (x y : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0)) (N : ℕ) :
    expSeriesPartialSumField (x + y) hnK N =
      ∑ n ∈ Finset.range N,
        ∑ ij ∈ Finset.antidiagonal n,
          expSeriesTermField x hnK ij.1 *
            expSeriesTermField y hnK ij.2

theorem

expSeriesPartialSumField_add_eq_sum_range_range_succ

L336 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesPartialSumField_add_eq_sum_range_range_succ

Documentation

Range-indexed form of finite partial sums of exp(x+y), obtained by opening each Cauchy-product antidiagonal.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem expSeriesPartialSumField_add_eq_sum_range_range_succ
    [Algebra ℚ K] (x y : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0)) (N : ℕ) :
    expSeriesPartialSumField (x + y) hnK N =
      ∑ n ∈ Finset.range N,
        ∑ i ∈ Finset.range n.succ,
          expSeriesTermField x hnK i *
            expSeriesTermField y hnK (n - i)

theorem

expSeriesPartialSumField_mul_eq_sum_range_range

L352 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesPartialSumField_mul_eq_sum_range_range

Documentation

Product of finite exponential partial sums, written as a rectangular double sum. This is the finite algebraic side of the Cauchy-product argument for Exp(x+y) = Exp(x) * Exp(y).

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem expSeriesPartialSumField_mul_eq_sum_range_range
    (x y : K) (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (M N : ℕ) :
    expSeriesPartialSumField x hnK M *
        expSeriesPartialSumField y hnK N =
      ∑ i ∈ Finset.range M,
        ∑ j ∈ Finset.range N,
          expSeriesTermField x hnK i * expSeriesTermField y hnK j

def

expSeriesFieldOfWithZeroValuation

L364 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesFieldOfWithZeroValuation

Documentation

Field-element value of the exponential series.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

def expSeriesFieldOfWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (x : K) (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0)) : K

theorem

logSeriesTermField_eq_logSeriesTerm_mk0

L371 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.logSeriesTermField_eq_logSeriesTerm_mk0

Documentation

Establishes the identity logSeriesTermField x hnK n = logSeriesTerm (Units.mk0 x hx) hnK n.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem logSeriesTermField_eq_logSeriesTerm_mk0
    {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (n : ℕ) :
    logSeriesTermField x hnK n =
      logSeriesTerm (Units.mk0 x hx) hnK n

theorem

signedLogSeriesTermField_eq_signedLogSeriesTerm_mk0

L382 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.signedLogSeriesTermField_eq_signedLogSeriesTerm_mk0

Documentation

Establishes the identity signedLogSeriesTermField x hnK n = signedLogSeriesTerm (Units.mk0 x hx) hnK n.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem signedLogSeriesTermField_eq_signedLogSeriesTerm_mk0
    {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (n : ℕ) :
    signedLogSeriesTermField x hnK n =
      signedLogSeriesTerm (Units.mk0 x hx) hnK n

theorem

logOnePlusSeriesField_eq_logOnePlusSeries_mk0

L394 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.logOnePlusSeriesField_eq_logOnePlusSeries_mk0

Documentation

Establishes the identity logOnePlusSeriesFieldOfWithZeroValuation v x hnK = logOnePlusSeriesOfWithZeroValuation v (Units.mk0 x hx) hnK.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem logOnePlusSeriesField_eq_logOnePlusSeries_mk0
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) :
    logOnePlusSeriesFieldOfWithZeroValuation v x hnK =
      logOnePlusSeriesOfWithZeroValuation v (Units.mk0 x hx) hnK

theorem

expSeriesTermField_eq_expSeriesTerm_mk0

L408 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesTermField_eq_expSeriesTerm_mk0

Documentation

Establishes the identity expSeriesTermField x hnK n = expSeriesTerm (Units.mk0 x hx) hnK n.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem expSeriesTermField_eq_expSeriesTerm_mk0
    {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0)) (n : ℕ) :
    expSeriesTermField x hnK n =
      expSeriesTerm (Units.mk0 x hx) hnK n

theorem

expSeriesField_eq_expSeries_mk0

L419 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesField_eq_expSeries_mk0

Documentation

Establishes the identity expSeriesFieldOfWithZeroValuation v x hnK = expSeriesOfWithZeroValuation v (Units.mk0 x hx) hnK.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem expSeriesField_eq_expSeries_mk0
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0)) :
    expSeriesFieldOfWithZeroValuation v x hnK =
      expSeriesOfWithZeroValuation v (Units.mk0 x hx) hnK

theorem

nonarchimedeanRing_ofWithZeroValuation

L434 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.nonarchimedeanRing_ofWithZeroValuation

Documentation

The topology attached to a valued field is nonarchimedean. This is the topological input needed before applying mathlib's nonarchimedean infinite-sum criterion.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem nonarchimedeanRing_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ))) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    NonarchimedeanRing K := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  simpa [Valued.mk'] using v.subgroups_basis.nonarchimedean

theorem

isTopologicallyNilpotent_ofWithZeroValuation_lt_one

L443 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.isTopologicallyNilpotent_ofWithZeroValuation_lt_one

Documentation

In the topology attached to a ℤᵐ⁰-valued valuation, every element of valuation strictly below one is topologically nilpotent.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem isTopologicallyNilpotent_ofWithZeroValuation_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {x : K} (hx : v x < (1 : WithZero (Multiplicative ℤ))) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    IsTopologicallyNilpotent x := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  exact Valued.tendsto_zero_pow_of_v_lt_one hx

theorem

ofWithZeroValuation_val_mk0_pos_of_lt_one

L453 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_val_mk0_pos_of_lt_one

Documentation

If a nonzero field element has valuation strictly below one, then its attached integer valuation as a field unit is positive.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem ofWithZeroValuation_val_mk0_pos_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {x : K} (hx : x ≠ 0)
    (hvx : v x < (1 : WithZero (Multiplicative ℤ))) :
    0 < (ofWithZeroValuation v).val (Units.mk0 x hx)

theorem

ofWithZeroValuation_val_mk0_one_lt_of_lt_exp_neg_one

L472 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_val_mk0_one_lt_of_lt_exp_neg_one

Documentation

If a nonzero element lies below exp (-1) in the normalized ℤᵐ⁰-valuation, then its attached integer valuation is strictly bigger than one. This is the field-element radius used for the exponential series.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem ofWithZeroValuation_val_mk0_one_lt_of_lt_exp_neg_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {x : K} (hx : x ≠ 0)
    (hvx : v x < WithZero.exp (-1 : ℤ)) :
    1 < ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℝ)

theorem

valuation_lt_one_of_ofWithZeroValuation_val_pos

L490 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_lt_one_of_ofWithZeroValuation_val_pos

Documentation

Positive attached integer valuation is the same direction as lying in the open unit ball for the original ℤᵐ⁰-valued valuation.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem valuation_lt_one_of_ofWithZeroValuation_val_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ))) (x : Kˣ)
    (hpos : 0 < (ofWithZeroValuation v).val x) :
    v (x : K) < (1 : WithZero (Multiplicative ℤ))

theorem

valuation_lt_of_ofWithZeroValuation_val_lt

L504 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_lt_of_ofWithZeroValuation_val_lt

Documentation

Integer-valued valuation comparison, translated back to the original ℤᵐ⁰-valued valuation. Larger integer value means smaller WithZero value.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem valuation_lt_of_ofWithZeroValuation_val_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ))) {x y : Kˣ}
    (hxy : (ofWithZeroValuation v).val x <
      (ofWithZeroValuation v).val y) :
    v (y : K) < v (x : K)

theorem

ofWithZeroValuation_val_lt_of_valuation_lt

L522 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_val_lt_of_valuation_lt

Documentation

Original valuation comparison, translated to the attached integer-valued valuation. This is the converse direction of valuation_lt_of_ofWithZeroValuation_val_lt.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem ofWithZeroValuation_val_lt_of_valuation_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ))) {x y : Kˣ}
    (hyx : v (y : K) < v (x : K)) :
    (ofWithZeroValuation v).val x <
      (ofWithZeroValuation v).val y

theorem

ofWithZeroValuation_val_eq_of_valuation_eq

L538 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_val_eq_of_valuation_eq

Documentation

Equal ℤᵐ⁰-valued valuations give equal integer valuations after passing to ofWithZeroValuation.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem ofWithZeroValuation_val_eq_of_valuation_eq
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ))) {x y : Kˣ}
    (hxy : v (x : K) = v (y : K)) :
    (ofWithZeroValuation v).val x = (ofWithZeroValuation v).val y

theorem

ofWithZeroValuation_val_add_ge_min

L546 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_val_add_ge_min

Documentation

The integer valuation attached to a nonarchimedean ℤᵐ⁰-valuation is bounded below by the minimum under addition.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem ofWithZeroValuation_val_add_ge_min
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {x y : K} (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x + y ≠ 0) :
    min ((ofWithZeroValuation v).val (Units.mk0 x hx))
        ((ofWithZeroValuation v).val (Units.mk0 y hy)) ≤
      (ofWithZeroValuation v).val (Units.mk0 (x + y) hxy)

theorem

valuation_limit_lt_of_tendsto_of_eventually_lt

L590 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_limit_lt_of_tendsto_of_eventually_lt

Documentation

In the topology attached to a discrete ℤᵐ⁰-valued valuation, every open valuation ball of nonzero radius is sequentially closed for convergent sequences.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem valuation_limit_lt_of_tendsto_of_eventually_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {γ : WithZero (Multiplicative ℤ)} (hγ : γ ≠ 0)
    {u : ℕ → K} {z : K}
    (hu :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      Tendsto u atTop (𝓝 z))
    (hsmall : ∀ᶠ n : ℕ in atTop, v (u n) < γ) :
    v z < γ := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  by_contra hznot
  have hzle : γ ≤ v z := le_of_not_gt hznot
  have hvz0 : v z ≠ 0 := by
    intro hvz
    apply hγ
    apply le_antisymm
    · simpa [hvz] using hzle
    · exact zero_le
  have hdiff :
      Tendsto (fun n : ℕ => z - u n) atTop (𝓝 (0 : K)) := by
    have hz : Tendsto (fun _ : ℕ => z) atTop (𝓝 z) := tendsto_const_nhds
    simpa using hz.sub hu
  have hball : {w : K | v w < v z} ∈ 𝓝 (0 : K) := by
    rw [Valued.mem_nhds_zero]
    refine ⟨Units.mk0 (v.restrict z) (by simpa using hvz0), ?_⟩
    intro w hw
    change v.restrict w < v.restrict z at hw
    exact v.restrict_lt_iff.mp hw
  have hdiff_small : ∀ᶠ n : ℕ in atTop, v (z - u n) < v z :=
    hdiff.eventually hball
  have hcontra : ∀ᶠ n : ℕ in atTop, False := by
    filter_upwards [hsmall, hdiff_small] with n hun hdiffn
    have hun_lt_z : v (u n) < v z := lt_of_lt_of_le hun hzle
    have hsub : v (z - u n) = v z :=
      v.map_sub_eq_of_lt_left hun_lt_z
    rw [hsub] at hdiffn
    exact (lt_irrefl _ hdiffn)
  rcases hcontra.exists with ⟨_, hfalse⟩
  exact hfalse

theorem

valuation_limit_lt_one_of_tendsto_of_eventually_lt_one

L632 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_limit_lt_one_of_tendsto_of_eventually_lt_one

Documentation

In the topology attached to a discrete ℤᵐ⁰-valued valuation, the open unit ball is sequentially closed for convergent sequences.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem valuation_limit_lt_one_of_tendsto_of_eventually_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {u : ℕ → K} {z : K}
    (hu :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      Tendsto u atTop (𝓝 z))
    (hsmall :
      ∀ᶠ n : ℕ in atTop,
        v (u n) < (1 : WithZero (Multiplicative ℤ))) :
    v z < (1 : WithZero (Multiplicative ℤ)) := by
  exact
    valuation_limit_lt_of_tendsto_of_eventually_lt
      (v := v) (γ := (1 : WithZero (Multiplicative ℤ))) one_ne_zero
      hu hsmall

theorem

valuation_mul_lt_one_of_lt_one

L649 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_mul_lt_one_of_lt_one

Documentation

The product of two elements of valuation strictly below one again has valuation strictly below one.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem valuation_mul_lt_one_of_lt_one
    {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
    (v : _root_.Valuation K Γ₀) {x y : K}
    (hx : v x < 1) (hy : v y < 1) :
    v (x * y) < 1

theorem

valuation_add_lt_of_lt

L658 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_add_lt_of_lt

Documentation

The open valuation ball of any radius is closed under addition.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem valuation_add_lt_of_lt
    {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
    (v : _root_.Valuation K Γ₀) {γ : Γ₀} {x y : K}
    (hx : v x < γ) (hy : v y < γ) :
    v (x + y) < γ

theorem

valuation_add_lt_exp_neg_one_of_lt_exp_neg_one

L666 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_add_lt_exp_neg_one_of_lt_exp_neg_one

Documentation

The normalized exponential convergence radius is stable under addition.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem valuation_add_lt_exp_neg_one_of_lt_exp_neg_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ))) {x y : K}
    (hx : v x < WithZero.exp (-1 : ℤ))
    (hy : v y < WithZero.exp (-1 : ℤ)) :
    v (x + y) < WithZero.exp (-1 : ℤ)

theorem

valuation_log_mul_argument_lt_one_of_lt_one

L675 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_log_mul_argument_lt_one_of_lt_one

Documentation

The logarithm product argument (1+x)(1+y)-1 = x+y+xy stays in the open unit ball of a valuation.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem valuation_log_mul_argument_lt_one_of_lt_one
    {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
    (v : _root_.Valuation K Γ₀) {x y : K}
    (hx : v x < 1) (hy : v y < 1) :
    v (x + y + x * y) < 1

theorem

ofWithZeroValuation_val_log_term_tendsto_atTop_of_pos

L693 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_val_log_term_tendsto_atTop_of_pos

Documentation

The field-unit logarithm theorem, logarithm-series valuation estimate: if x has positive integer valuation, then the valuations of x^(n+1)/(n+1) tend to +∞.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem ofWithZeroValuation_val_log_term_tendsto_atTop_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hxpos : 0 < (ofWithZeroValuation v).val x) :
    Tendsto
      (fun n : ℕ =>
        ((ofWithZeroValuation v).val
          (x ^ (n + 1) /
            Units.mk0 (((n + 1 : ℕ) : K)) (hnK n)) : ℝ))
      atTop atTop := by
  have hxone : (1 : ℤ) ≤ (ofWithZeroValuation v).val x := by
    omega
  have hxoneReal : (1 : ℝ) ≤ ((ofWithZeroValuation v).val x : ℝ) := by
    exact_mod_cast hxone
  exact
    ofWithZeroValuation_val_pow_succ_div_natCast_tendsto_atTop
      (v := v) (p := p) x hnK hnval
      (hcpos := by norm_num)
      (hc := hxoneReal)

theorem

eventually_le_ofWithZeroValuation_val_log_term_of_pos

L719 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.eventually_le_ofWithZeroValuation_val_log_term_of_pos

Documentation

Eventually the logarithm-series terms have valuation at least any prescribed integer bound.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem eventually_le_ofWithZeroValuation_val_log_term_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hxpos : 0 < (ofWithZeroValuation v).val x)
    (N : ℤ) :
    ∀ᶠ n : ℕ in atTop,
      N ≤
        (ofWithZeroValuation v).val
          (x ^ (n + 1) /
            Units.mk0 (((n + 1 : ℕ) : K)) (hnK n))

theorem

tendsto_zero_log_term_ofWithZeroValuation_of_pos

L748 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.tendsto_zero_log_term_ofWithZeroValuation_of_pos

Documentation

The logarithm-series terms themselves tend to zero for the topology defined by the given ℤᵐ⁰-valued valuation.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem tendsto_zero_log_term_ofWithZeroValuation_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hxpos : 0 < (ofWithZeroValuation v).val x) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto
      (fun n : ℕ =>
        ((x ^ (n + 1) /
          Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K))
      atTop (𝓝 (0 : K)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  rw [tendsto_iff_forall_eventually_mem]
  intro s hs
  rw [Valued.mem_nhds_zero] at hs
  rcases hs with ⟨γ, hγs⟩
  let γ' : (WithZero (Multiplicative ℤ))ˣ :=
    Units.map (MonoidWithZeroHom.ValueGroup₀.embedding
      (f := (v : K →*₀ WithZero (Multiplicative ℤ)))) γ
  rcases WithZero.exists_exp_neg_natCast_lt γ'.ne_zero with ⟨N, hNγ⟩
  have hterm :=
    eventually_le_ofWithZeroValuation_val_log_term_of_pos
      (v := v) (p := p) x hnK hnval hxpos (N : ℤ)
  filter_upwards [hterm] with n hn
  apply hγs
  let y : Kˣ :=
    x ^ (n + 1) /
      Units.mk0 (((n + 1 : ℕ) : K)) (hnK n)
  have hlog :
      WithZero.log (v (y : K)) ≤ -(N : ℤ) := by
    have hNlog : (N : ℤ) ≤ -WithZero.log (v (y : K)) := by
      simpa [y, ofWithZeroValuation_val] using hn
    linarith
  have hvle : v (y : K) ≤ WithZero.exp (-(N : ℤ)) :=
    WithZero.le_exp_of_log_le hlog
  change v.restrict (y : K) < γ.1
  rw [Valuation.restrict_lt_iff_lt_embedding]
  exact lt_of_le_of_lt hvle (by simpa [γ'] using hNγ)

theorem

tendsto_zero_signed_log_term_ofWithZeroValuation_of_pos

L792 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.tendsto_zero_signed_log_term_ofWithZeroValuation_of_pos

Documentation

The signed logarithm-series terms also tend to zero. This is the form matching the usual series for log (1 + x).

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem tendsto_zero_signed_log_term_ofWithZeroValuation_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hxpos : 0 < (ofWithZeroValuation v).val x) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto
      (fun n : ℕ =>
        (-1 : K) ^ n *
          ((x ^ (n + 1) /
            Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K))
      atTop (𝓝 (0 : K)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  rw [tendsto_iff_forall_eventually_mem]
  intro s hs
  rw [Valued.mem_nhds_zero] at hs
  rcases hs with ⟨γ, hγs⟩
  let γ' : (WithZero (Multiplicative ℤ))ˣ :=
    Units.map (MonoidWithZeroHom.ValueGroup₀.embedding
      (f := (v : K →*₀ WithZero (Multiplicative ℤ)))) γ
  rcases WithZero.exists_exp_neg_natCast_lt γ'.ne_zero with ⟨N, hNγ⟩
  have hterm :=
    eventually_le_ofWithZeroValuation_val_log_term_of_pos
      (v := v) (p := p) x hnK hnval hxpos (N : ℤ)
  filter_upwards [hterm] with n hn
  apply hγs
  let y : Kˣ :=
    x ^ (n + 1) /
      Units.mk0 (((n + 1 : ℕ) : K)) (hnK n)
  have hlog :
      WithZero.log (v (y : K)) ≤ -(N : ℤ) := by
    have hNlog : (N : ℤ) ≤ -WithZero.log (v (y : K)) := by
      simpa [y, ofWithZeroValuation_val] using hn
    linarith
  have hvle : v (y : K) ≤ WithZero.exp (-(N : ℤ)) :=
    WithZero.le_exp_of_log_le hlog
  have hsign : v ((-1 : K) ^ n) = 1 := by
    rw [v.map_pow]
    simp
  have hvsigned :
      v ((-1 : K) ^ n * (y : K)) ≤ WithZero.exp (-(N : ℤ)) := by
    rw [v.map_mul, hsign, one_mul]
    exact hvle
  change v.restrict ((-1 : K) ^ n * (y : K)) < γ.1
  rw [Valuation.restrict_lt_iff_lt_embedding]
  exact lt_of_le_of_lt hvsigned (by simpa [γ'] using hNγ)

theorem

summable_log_term_ofWithZeroValuation_of_pos

L845 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.summable_log_term_ofWithZeroValuation_of_pos

Documentation

In a complete nonarchimedean valuation topology, the logarithm-series terms are summable. This is the convergence step of the field-unit logarithm theorem after the valuation estimate has been proved.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem summable_log_term_ofWithZeroValuation_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hxpos : 0 < (ofWithZeroValuation v).val x)
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Summable
      (fun n : ℕ =>
        ((x ^ (n + 1) /
          Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : CompleteSpace K := hcomplete
  have : NonarchimedeanRing K := nonarchimedeanRing_ofWithZeroValuation v
  have hzero :
      Tendsto
        (fun n : ℕ =>
          ((x ^ (n + 1) /
            Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K))
        atTop (𝓝 (0 : K)) :=
    tendsto_zero_log_term_ofWithZeroValuation_of_pos
      (v := v) (p := p) x hnK hnval hxpos
  have hcofinite :
      Tendsto
        (fun n : ℕ =>
          ((x ^ (n + 1) /
            Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K))
        cofinite (𝓝 (0 : K)) := by
    simpa [Nat.cofinite_eq_atTop] using hzero
  rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero]
  exact hcofinite

theorem

summable_signed_log_term_ofWithZeroValuation_of_pos

L883 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.summable_signed_log_term_ofWithZeroValuation_of_pos

Documentation

Summability of the signed logarithm series in the valuation topology.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem summable_signed_log_term_ofWithZeroValuation_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hxpos : 0 < (ofWithZeroValuation v).val x)
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Summable
      (fun n : ℕ =>
        (-1 : K) ^ n *
          ((x ^ (n + 1) /
            Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : CompleteSpace K := hcomplete
  have : NonarchimedeanRing K := nonarchimedeanRing_ofWithZeroValuation v
  have hzero :
      Tendsto
        (fun n : ℕ =>
          (-1 : K) ^ n *
            ((x ^ (n + 1) /
              Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K))
        atTop (𝓝 (0 : K)) :=
    tendsto_zero_signed_log_term_ofWithZeroValuation_of_pos
      (v := v) (p := p) x hnK hnval hxpos
  have hcofinite :
      Tendsto
        (fun n : ℕ =>
          (-1 : K) ^ n *
            ((x ^ (n + 1) /
              Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K))
        cofinite (𝓝 (0 : K)) := by
    simpa [Nat.cofinite_eq_atTop] using hzero
  rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero]
  exact hcofinite

theorem

hasSum_signedLogSeriesTerm_logOnePlusSeries_ofWithZeroValuation_of_pos

L926 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.hasSum_signedLogSeriesTerm_logOnePlusSeries_ofWithZeroValuation_of_pos

Documentation

The field-unit logarithm theorem, principal-unit logarithm series: the signed series for log (1 + x) has the value supplied by logOnePlusSeriesOfWithZeroValuation.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem hasSum_signedLogSeriesTerm_logOnePlusSeries_ofWithZeroValuation_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hxpos : 0 < (ofWithZeroValuation v).val x)
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum (fun n : ℕ => signedLogSeriesTerm x hnK n)
      (logOnePlusSeriesOfWithZeroValuation v x hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hs :
      Summable
        (fun n : ℕ =>
          (-1 : K) ^ n *
            ((x ^ (n + 1) /
              Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K)) :=
    summable_signed_log_term_ofWithZeroValuation_of_pos
      (v := v) (p := p) x hnK hnval hxpos hcomplete
  simpa [logOnePlusSeriesOfWithZeroValuation, signedLogSeriesTerm,
    logSeriesTerm] using hs.hasSum

theorem

tendsto_logOnePlusPartialSum_ofWithZeroValuation_of_pos

L955 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.tendsto_logOnePlusPartialSum_ofWithZeroValuation_of_pos

Documentation

The finite principal-unit logarithm polynomials converge to the logarithm series value. This is the convergence form used before proving additivity of the logarithm on U^(1).

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem tendsto_logOnePlusPartialSum_ofWithZeroValuation_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hxpos : 0 < (ofWithZeroValuation v).val x)
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto (fun N : ℕ => logOnePlusPartialSum x hnK N) atTop
      (𝓝 (logOnePlusSeriesOfWithZeroValuation v x hnK)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hsum :=
    hasSum_signedLogSeriesTerm_logOnePlusSeries_ofWithZeroValuation_of_pos
      (v := v) (p := p) x hnK hnval hxpos hcomplete
  simpa [logOnePlusPartialSum] using hsum.tendsto_sum_nat

theorem

ofWithZeroValuation_val_log_term_scaled_tendsto_atTop_of_pos

L978 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_val_log_term_scaled_tendsto_atTop_of_pos

Documentation

Ramified-denominator version of the logarithm-series valuation estimate: if integer denominators have value e * v_p(n), positive valuation of x still forces x^(n+1)/(n+1) to tend to zero.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem ofWithZeroValuation_val_log_term_scaled_tendsto_atTop_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hxpos : 0 < (ofWithZeroValuation v).val x) :
    Tendsto
      (fun n : ℕ =>
        ((ofWithZeroValuation v).val
          (x ^ (n + 1) /
            Units.mk0 (((n + 1 : ℕ) : K)) (hnK n)) : ℝ))
      atTop atTop := by
  have hxone : (1 : ℤ) ≤ (ofWithZeroValuation v).val x := by
    omega
  have hxoneReal : (1 : ℝ) ≤ ((ofWithZeroValuation v).val x : ℝ) := by
    exact_mod_cast hxone
  exact
    ofWithZeroValuation_val_pow_succ_div_natCast_scaled_tendsto_atTop
      (v := v) (p := p) e x hnK hnval
      (hcpos := by norm_num)
      (hc := hxoneReal)

theorem

eventually_le_ofWithZeroValuation_val_log_term_scaled_of_pos

L1004 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.eventually_le_ofWithZeroValuation_val_log_term_scaled_of_pos

Documentation

Eventually the ramified-denominator logarithm-series terms have valuation at least any prescribed integer bound.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem eventually_le_ofWithZeroValuation_val_log_term_scaled_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hxpos : 0 < (ofWithZeroValuation v).val x)
    (N : ℤ) :
    ∀ᶠ n : ℕ in atTop,
      N ≤
        (ofWithZeroValuation v).val
          (x ^ (n + 1) /
            Units.mk0 (((n + 1 : ℕ) : K)) (hnK n))

theorem

tendsto_zero_signed_log_term_ofWithZeroValuation_scaled_of_pos

L1033 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.tendsto_zero_signed_log_term_ofWithZeroValuation_scaled_of_pos

Documentation

The signed logarithm-series terms tend to zero under the ramified denominator valuation hypothesis.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem tendsto_zero_signed_log_term_ofWithZeroValuation_scaled_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hxpos : 0 < (ofWithZeroValuation v).val x) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto
      (fun n : ℕ =>
        (-1 : K) ^ n *
          ((x ^ (n + 1) /
            Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K))
      atTop (𝓝 (0 : K)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  rw [tendsto_iff_forall_eventually_mem]
  intro s hs
  rw [Valued.mem_nhds_zero] at hs
  rcases hs with ⟨γ, hγs⟩
  let γ' : (WithZero (Multiplicative ℤ))ˣ :=
    Units.map (MonoidWithZeroHom.ValueGroup₀.embedding
      (f := (v : K →*₀ WithZero (Multiplicative ℤ)))) γ
  rcases WithZero.exists_exp_neg_natCast_lt γ'.ne_zero with ⟨N, hNγ⟩
  have hterm :=
    eventually_le_ofWithZeroValuation_val_log_term_scaled_of_pos
      (v := v) (p := p) e x hnK hnval hxpos (N : ℤ)
  filter_upwards [hterm] with n hn
  apply hγs
  let y : Kˣ :=
    x ^ (n + 1) /
      Units.mk0 (((n + 1 : ℕ) : K)) (hnK n)
  have hlog :
      WithZero.log (v (y : K)) ≤ -(N : ℤ) := by
    have hNlog : (N : ℤ) ≤ -WithZero.log (v (y : K)) := by
      simpa [y, ofWithZeroValuation_val] using hn
    linarith
  have hvle : v (y : K) ≤ WithZero.exp (-(N : ℤ)) :=
    WithZero.le_exp_of_log_le hlog
  have hsign : v ((-1 : K) ^ n) = 1 := by
    rw [v.map_pow]
    simp
  have hvsigned :
      v ((-1 : K) ^ n * (y : K)) ≤ WithZero.exp (-(N : ℤ)) := by
    rw [v.map_mul, hsign, one_mul]
    exact hvle
  change v.restrict ((-1 : K) ^ n * (y : K)) < γ.1
  rw [Valuation.restrict_lt_iff_lt_embedding]
  exact lt_of_le_of_lt hvsigned (by simpa [γ'] using hNγ)

theorem

summable_signed_log_term_ofWithZeroValuation_scaled_of_pos

L1085 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.summable_signed_log_term_ofWithZeroValuation_scaled_of_pos

Documentation

Summability of the signed logarithm series under a ramified denominator valuation hypothesis.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem summable_signed_log_term_ofWithZeroValuation_scaled_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hxpos : 0 < (ofWithZeroValuation v).val x)
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Summable
      (fun n : ℕ =>
        (-1 : K) ^ n *
          ((x ^ (n + 1) /
            Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : CompleteSpace K := hcomplete
  have : NonarchimedeanRing K := nonarchimedeanRing_ofWithZeroValuation v
  have hzero :
      Tendsto
        (fun n : ℕ =>
          (-1 : K) ^ n *
            ((x ^ (n + 1) /
              Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K))
        atTop (𝓝 (0 : K)) :=
    tendsto_zero_signed_log_term_ofWithZeroValuation_scaled_of_pos
      (v := v) (p := p) e x hnK hnval hxpos
  have hcofinite :
      Tendsto
        (fun n : ℕ =>
          (-1 : K) ^ n *
            ((x ^ (n + 1) /
              Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K))
        cofinite (𝓝 (0 : K)) := by
    simpa [Nat.cofinite_eq_atTop] using hzero
  rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero]
  exact hcofinite

theorem

hasSum_signedLogSeriesTerm_logOnePlusSeries_ofWithZeroValuation_scaled_of_pos

L1127 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.hasSum_signedLogSeriesTerm_logOnePlusSeries_ofWithZeroValuation_scaled_of_pos

Documentation

The logarithm series has the same tsum value under a ramified denominator valuation hypothesis.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem hasSum_signedLogSeriesTerm_logOnePlusSeries_ofWithZeroValuation_scaled_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hxpos : 0 < (ofWithZeroValuation v).val x)
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum (fun n : ℕ => signedLogSeriesTerm x hnK n)
      (logOnePlusSeriesOfWithZeroValuation v x hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hs :
      Summable
        (fun n : ℕ =>
          (-1 : K) ^ n *
            ((x ^ (n + 1) /
              Units.mk0 (((n + 1 : ℕ) : K)) (hnK n) : Kˣ) : K)) :=
    summable_signed_log_term_ofWithZeroValuation_scaled_of_pos
      (v := v) (p := p) e x hnK hnval hxpos hcomplete
  simpa [logOnePlusSeriesOfWithZeroValuation, signedLogSeriesTerm,
    logSeriesTerm] using hs.hasSum

theorem

tendsto_logOnePlusPartialSum_ofWithZeroValuation_scaled_of_pos

L1155 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.tendsto_logOnePlusPartialSum_ofWithZeroValuation_scaled_of_pos

Documentation

Finite logarithm polynomials converge to the logarithm-series value under the ramified denominator valuation hypothesis.

Source context 12 commands

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

open Filter
open Polynomial
open scoped Topology
open scoped PowerSeries.WithPiTopology
noncomputable section
attribute [local instance] Classical.propDecidable
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · full declaration

theorem tendsto_logOnePlusPartialSum_ofWithZeroValuation_scaled_of_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hxpos : 0 < (ofWithZeroValuation v).val x)
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto (fun N : ℕ => logOnePlusPartialSum x hnK N) atTop
      (𝓝 (logOnePlusSeriesOfWithZeroValuation v x hnK)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hsum :=
    hasSum_signedLogSeriesTerm_logOnePlusSeries_ofWithZeroValuation_scaled_of_pos
      (v := v) (p := p) e x hnK hnval hxpos hcomplete
  simpa [logOnePlusPartialSum] using hsum.tendsto_sum_nat

Module documentation

Exponential-series terms

Declarations