Module

Homomorphisms.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.Homomorphisms

50 declarations indexed from sourceView source ↗

Module documentation

Packages the convergent logarithm and exponential series as additive and multiplicative homomorphisms on their natural nonarchimedean domains.

Imports1

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.PrincipalUnitLog

Imported by4

def

principalUnitLogPartialSumOfWithZeroValuation

L34 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogPartialSumOfWithZeroValuation

Documentation

Finite logarithm polynomials of a first principal unit.

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 principalUnitLogPartialSumOfWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (N : ℕ) : K

theorem

principalUnitLogPartialSum_zero_ofWithZeroValuation

L42 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogPartialSum_zero_ofWithZeroValuation

Documentation

Establishes the identity principalUnitLogPartialSumOfWithZeroValuation v u 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 principalUnitLogPartialSum_zero_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) :
    principalUnitLogPartialSumOfWithZeroValuation v u hnK 0 = 0

theorem

principalUnitLogPartialSum_one_ofWithZeroValuation

L54 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogPartialSum_one_ofWithZeroValuation

Documentation

Establishes the identity principalUnitLogPartialSumOfWithZeroValuation v u hnK 1 = principalUnitSubOneOfWithZeroValuation v u.

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 principalUnitLogPartialSum_one_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) :
    principalUnitLogPartialSumOfWithZeroValuation v u hnK 1 =
      principalUnitSubOneOfWithZeroValuation v u

theorem

principalUnitLogSeries_one_ofWithZeroValuation

L67 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_one_ofWithZeroValuation

Documentation

Establishes the identity principalUnitLogSeriesOfWithZeroValuation v (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) hnK = 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 principalUnitLogSeries_one_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) :
    principalUnitLogSeriesOfWithZeroValuation v
        (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
        hnK = 0

theorem

principalUnitLogSeries_valuation_eq_subOne_of_inv_sub_one_lt

L78 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_valuation_eq_subOne_of_inv_sub_one_lt

Documentation

Above the usual 1/(p-1) threshold, the principal-unit logarithm has the same valuation as the additive parameter 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 principalUnitLogSeries_valuation_eq_subOne_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hne : principalUnitSubOneOfWithZeroValuation v u ≠ 0)
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val
          (Units.mk0 (principalUnitSubOneOfWithZeroValuation v u) hne) :
          ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    v (principalUnitLogSeriesOfWithZeroValuation v u hnK) =
      v (principalUnitSubOneOfWithZeroValuation v u) := by
  have hvx :
      v (principalUnitSubOneOfWithZeroValuation v u) <
        (1 : WithZero (Multiplicative ℤ)) :=
    principalUnitSubOne_val_lt_one_ofWithZeroValuation v u
  simpa [principalUnitLogSeriesOfWithZeroValuation] using
    valuation_logOnePlusSeriesField_eq_self_of_inv_sub_one_lt
      (v := v) (p := p)
      (x := principalUnitSubOneOfWithZeroValuation v u) hne
      hnK hnval hvx hthreshold hcomplete

theorem

principalUnitLogSeries_ne_zero_of_inv_sub_one_lt

L110 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_ne_zero_of_inv_sub_one_lt

Documentation

Above the usual 1/(p-1) threshold, the principal-unit logarithm is nonzero away from the 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 · full declaration

theorem principalUnitLogSeries_ne_zero_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hne : principalUnitSubOneOfWithZeroValuation v u ≠ 0)
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val
          (Units.mk0 (principalUnitSubOneOfWithZeroValuation v u) hne) :
          ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitLogSeriesOfWithZeroValuation v u hnK ≠ 0 := by
  intro hzero
  have hv :
      v (principalUnitLogSeriesOfWithZeroValuation v u hnK) =
        v (principalUnitSubOneOfWithZeroValuation v u) :=
    principalUnitLogSeries_valuation_eq_subOne_of_inv_sub_one_lt
      (v := v) (p := p) u hnK hnval hne hthreshold hcomplete
  rw [hzero, map_zero] at hv
  exact ((_root_.Valuation.ne_zero_iff v).2 hne) hv.symm

theorem

principalUnitLogSeries_eq_zero_iff_subOne_eq_zero_of_inv_sub_one_lt

L140 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_eq_zero_iff_subOne_eq_zero_of_inv_sub_one_lt

Documentation

On a threshold-controlled principal-unit domain, the logarithm has kernel exactly the identity element.

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 principalUnitLogSeries_eq_zero_iff_subOne_eq_zero_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hthreshold : ∀ hne : principalUnitSubOneOfWithZeroValuation v u ≠ 0,
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val
          (Units.mk0 (principalUnitSubOneOfWithZeroValuation v u) hne) :
          ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitLogSeriesOfWithZeroValuation v u hnK = 0 ↔
      principalUnitSubOneOfWithZeroValuation v u = 0 := by
  constructor
  · intro hlog
    by_contra hne
    exact
      (principalUnitLogSeries_ne_zero_of_inv_sub_one_lt
        (v := v) (p := p) u hnK hnval hne (hthreshold hne) hcomplete)
        hlog
  · intro hsub
    simp [principalUnitLogSeriesOfWithZeroValuation, hsub]

theorem

principalUnitLogSeries_eq_zero_iff_eq_one_of_inv_sub_one_lt

L171 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_eq_zero_iff_eq_one_of_inv_sub_one_lt

Documentation

On a threshold-controlled principal-unit domain, the logarithm has kernel exactly the 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 · full declaration

theorem principalUnitLogSeries_eq_zero_iff_eq_one_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hthreshold : ∀ hne : principalUnitSubOneOfWithZeroValuation v u ≠ 0,
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val
          (Units.mk0 (principalUnitSubOneOfWithZeroValuation v u) hne) :
          ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitLogSeriesOfWithZeroValuation v u hnK = 0 ↔
      u = (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) := by
  rw [principalUnitLogSeries_eq_zero_iff_subOne_eq_zero_of_inv_sub_one_lt
    (v := v) (p := p) u hnK hnval hthreshold hcomplete]
  exact principalUnitSubOne_eq_zero_iff_ofWithZeroValuation v u

theorem

principalUnitLogSeries_val_lt_exp_neg_one_of_subOne_val_lt_exp_neg_one

L197 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_val_lt_exp_neg_one_of_subOne_val_lt_exp_neg_one

Documentation

If u - 1 lies in the normalized exponential convergence ball and the logarithm threshold holds, then Log(u) also lies in the exponential convergence ball.

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 principalUnitLogSeries_val_lt_exp_neg_one_of_subOne_val_lt_exp_neg_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hne : principalUnitSubOneOfWithZeroValuation v u ≠ 0)
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val
          (Units.mk0 (principalUnitSubOneOfWithZeroValuation v u) hne) :
          ℚ))
    (hsubExp :
      v (principalUnitSubOneOfWithZeroValuation v u) <
        WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    v (principalUnitLogSeriesOfWithZeroValuation v u hnK) <
      WithZero.exp (-1 : ℤ) := by
  have hv :
      v (principalUnitLogSeriesOfWithZeroValuation v u hnK) =
        v (principalUnitSubOneOfWithZeroValuation v u) :=
    principalUnitLogSeries_valuation_eq_subOne_of_inv_sub_one_lt
      (v := v) (p := p) u hnK hnval hne hthreshold hcomplete
  rw [hv]
  exact hsubExp

theorem

principalUnitExpSeries_logSeries_eq_one_iff_eq_one_ofWithZeroValuation

L230 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitExpSeries_logSeries_eq_one_iff_eq_one_ofWithZeroValuation

Documentation

On a threshold-controlled domain where Log(u) lies in the exponential convergence ball, the composite Exp(Log(u)) has kernel exactly the 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 · full declaration

theorem principalUnitExpSeries_logSeries_eq_one_iff_eq_one_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnKexp : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnvalExp : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hnKlog : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnvalLog : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvlogExp :
      v (principalUnitLogSeriesOfWithZeroValuation v u hnKlog) <
        WithZero.exp (-1 : ℤ))
    (hthreshold : ∀ hne : principalUnitSubOneOfWithZeroValuation v u ≠ 0,
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val
          (Units.mk0 (principalUnitSubOneOfWithZeroValuation v u) hne) :
          ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p)
        (principalUnitLogSeriesOfWithZeroValuation v u hnKlog)
        hnKexp hnvalExp hvlogExp hcomplete =
        (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) ↔
      u = (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) := by
  rw [principalUnitExpSeries_eq_one_iff_ofWithZeroValuation
    (v := v) (p := p)
    (x := principalUnitLogSeriesOfWithZeroValuation v u hnKlog)
    hnKexp hnvalExp hvlogExp hcomplete]
  exact
    principalUnitLogSeries_eq_zero_iff_eq_one_of_inv_sub_one_lt
      (v := v) (p := p) u hnKlog hnvalLog hthreshold hcomplete

theorem

principalUnitLogSeries_expSeries_valuation_eq_self_ofWithZeroValuation

L270 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_expSeries_valuation_eq_self_ofWithZeroValuation

Documentation

On the common convergence and threshold domain, the composite Log(Exp(x)) has the same valuation as 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 principalUnitLogSeries_expSeries_valuation_eq_self_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnKexp : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnvalExp : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hnKlog : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnvalLog : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    v (principalUnitLogSeriesOfWithZeroValuation v
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnKexp hnvalExp hvx hcomplete) hnKlog) =
      v x := by
  let u :=
    principalUnitExpSeriesOfWithZeroValuation
      (v := v) (p := p) x hnKexp hnvalExp hvx hcomplete
  have hne : principalUnitSubOneOfWithZeroValuation v u ≠ 0 := by
    dsimp [u]
    exact
      principalUnitSubOne_expSeries_ne_zero_ofWithZeroValuation
        (v := v) (p := p) (x := x) hx hnKexp hnvalExp hvx hcomplete
  have hthresholdSub :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val
          (Units.mk0 (principalUnitSubOneOfWithZeroValuation v u) hne) :
          ℚ) := by
    dsimp [u]
    exact
      principalUnitSubOne_expSeries_threshold_ofWithZeroValuation
        (v := v) (p := p) (x := x) hx hnKexp hnvalExp hvx hthreshold
        hcomplete hne
  have hvlog :
      v (principalUnitLogSeriesOfWithZeroValuation v u hnKlog) =
        v (principalUnitSubOneOfWithZeroValuation v u) :=
    principalUnitLogSeries_valuation_eq_subOne_of_inv_sub_one_lt
      (v := v) (p := p) u hnKlog hnvalLog hne hthresholdSub hcomplete
  have hvsub :
      v (principalUnitSubOneOfWithZeroValuation v u) = v x := by
    dsimp [u]
    exact
      principalUnitSubOne_expSeries_valuation_eq_self_ofWithZeroValuation
        (v := v) (p := p) (x := x) hx hnKexp hnvalExp hvx hcomplete
  exact hvlog.trans hvsub

theorem

principalUnitLogSeries_expSeries_ne_zero_ofWithZeroValuation

L326 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_expSeries_ne_zero_ofWithZeroValuation

Documentation

On the common convergence and threshold domain, Log(Exp(x)) is nonzero for nonzero 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 principalUnitLogSeries_expSeries_ne_zero_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnKexp : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnvalExp : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hnKlog : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnvalLog : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitLogSeriesOfWithZeroValuation v
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnKexp hnvalExp hvx hcomplete) hnKlog ≠ 0 := by
  intro hzero
  have hv :
      v (principalUnitLogSeriesOfWithZeroValuation v
        (principalUnitExpSeriesOfWithZeroValuation
          (v := v) (p := p) x hnKexp hnvalExp hvx hcomplete) hnKlog) =
        v x :=
    principalUnitLogSeries_expSeries_valuation_eq_self_ofWithZeroValuation
      (v := v) (p := p) (x := x) hx hnKexp hnvalExp hnKlog hnvalLog
      hvx hthreshold hcomplete
  rw [hzero, map_zero] at hv
  exact ((_root_.Valuation.ne_zero_iff v).2 hx) hv.symm

theorem

principalUnitLogSeries_expSeries_eq_zero_iff_ofWithZeroValuation

L362 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_expSeries_eq_zero_iff_ofWithZeroValuation

Documentation

On the common convergence and threshold domain, the composite Log ∘ Exp has trivial kernel.

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 principalUnitLogSeries_expSeries_eq_zero_iff_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] {x : K}
    (hnKexp : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnvalExp : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hnKlog : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnvalLog : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hthreshold : ∀ hx : x ≠ 0,
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitLogSeriesOfWithZeroValuation v
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnKexp hnvalExp hvx hcomplete) hnKlog = 0 ↔
      x = 0 := by
  constructor
  · intro hlog
    by_contra hx
    exact
      (principalUnitLogSeries_expSeries_ne_zero_ofWithZeroValuation
        (v := v) (p := p) (x := x) hx hnKexp hnvalExp hnKlog hnvalLog
        hvx (hthreshold hx) hcomplete) hlog
  · intro hx
    subst x
    have hExp :
        principalUnitExpSeriesOfWithZeroValuation
          (v := v) (p := p) (0 : K) hnKexp hnvalExp hvx hcomplete =
          (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) :=
      (principalUnitExpSeries_eq_one_iff_ofWithZeroValuation
        (v := v) (p := p) (x := (0 : K)) hnKexp hnvalExp hvx hcomplete).2 rfl
    simp [hExp]

theorem

principalUnitLogSeries_mul_argument_ofWithZeroValuation

L404 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_mul_argument_ofWithZeroValuation

Documentation

Product of principal units, rewritten as the log(1 + z) argument for z = (u - 1) + (w - 1) + (u - 1)(w - 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 · statement

theorem principalUnitLogSeries_mul_argument_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) :
    principalUnitLogSeriesOfWithZeroValuation v (u * w) hnK =
      logOnePlusSeriesFieldOfWithZeroValuation v
        (principalUnitSubOneOfWithZeroValuation v u +
          principalUnitSubOneOfWithZeroValuation v w +
            principalUnitSubOneOfWithZeroValuation v u *
              principalUnitSubOneOfWithZeroValuation v w) hnK

theorem

principalUnitLogPartialSum_mul_argument_ofWithZeroValuation

L420 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogPartialSum_mul_argument_ofWithZeroValuation

Documentation

Finite-logarithm-polynomial version of principalUnitLogSeries_mul_argument_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 principalUnitLogPartialSum_mul_argument_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (N : ℕ) :
    principalUnitLogPartialSumOfWithZeroValuation v (u * w) hnK N =
      logOnePlusPartialSumField
        (principalUnitSubOneOfWithZeroValuation v u +
          principalUnitSubOneOfWithZeroValuation v w +
            principalUnitSubOneOfWithZeroValuation v u *
              principalUnitSubOneOfWithZeroValuation v w) hnK N

theorem

hasSum_principalUnitLogSeries_mul_argument_ofWithZeroValuation

L436 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.hasSum_principalUnitLogSeries_mul_argument_ofWithZeroValuation

Documentation

The logarithm series for a product of first principal units, written with the explicit product argument (u - 1) + (w - 1) + (u - 1)(w - 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 hasSum_principalUnitLogSeries_mul_argument_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum
      (fun n : ℕ =>
        signedLogSeriesTermField
          (principalUnitSubOneOfWithZeroValuation v u +
            principalUnitSubOneOfWithZeroValuation v w +
              principalUnitSubOneOfWithZeroValuation v u *
                principalUnitSubOneOfWithZeroValuation v w) hnK n)
      (principalUnitLogSeriesOfWithZeroValuation v (u * w) hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hvu :
      v (principalUnitSubOneOfWithZeroValuation v u) <
        (1 : WithZero (Multiplicative ℤ)) :=
    principalUnitSubOne_val_lt_one_ofWithZeroValuation v u
  have hvw :
      v (principalUnitSubOneOfWithZeroValuation v w) <
        (1 : WithZero (Multiplicative ℤ)) :=
    principalUnitSubOne_val_lt_one_ofWithZeroValuation v w
  have hsum :=
    hasSum_signedLogSeriesTermField_logOnePlusSeriesField_mul_argument
      (v := v) (p := p)
      (principalUnitSubOneOfWithZeroValuation v u)
      (principalUnitSubOneOfWithZeroValuation v w)
      hnK hnval hvu hvw hcomplete
  simpa [principalUnitLogSeries_mul_argument_ofWithZeroValuation] using hsum

theorem

tendsto_principalUnitLogPartialSum_mul_argument_ofWithZeroValuation

L477 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.tendsto_principalUnitLogPartialSum_mul_argument_ofWithZeroValuation

Documentation

Finite logarithm polynomials for a product of first principal units converge to the product logarithm-series value, in the explicit (u - 1) + (w - 1) + (u - 1)(w - 1) argument form.

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_principalUnitLogPartialSum_mul_argument_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto
      (fun N : ℕ =>
        logOnePlusPartialSumField
          (principalUnitSubOneOfWithZeroValuation v u +
            principalUnitSubOneOfWithZeroValuation v w +
              principalUnitSubOneOfWithZeroValuation v u *
                principalUnitSubOneOfWithZeroValuation v w) hnK N)
      atTop (𝓝 (principalUnitLogSeriesOfWithZeroValuation v (u * w) hnK)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hsum :=
    hasSum_principalUnitLogSeries_mul_argument_ofWithZeroValuation
      (v := v) (p := p) u w hnK hnval hcomplete
  simpa [logOnePlusPartialSumField] using hsum.tendsto_sum_nat

theorem

hasSum_principalUnitLogSeries_ofWithZeroValuation

L506 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.hasSum_principalUnitLogSeries_ofWithZeroValuation

Documentation

The principal-unit logarithm series has the value principalUnitLogSeriesOfWithZeroValuation.

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_principalUnitLogSeries_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum
      (fun n : ℕ =>
        signedLogSeriesTermField
          (principalUnitSubOneOfWithZeroValuation v u) hnK n)
      (principalUnitLogSeriesOfWithZeroValuation v u hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hvx :
      v (principalUnitSubOneOfWithZeroValuation v u) <
        (1 : WithZero (Multiplicative ℤ)) :=
    principalUnitSubOne_val_lt_one_ofWithZeroValuation v u
  simpa [principalUnitLogSeriesOfWithZeroValuation] using
    hasSum_signedLogSeriesTermField_logOnePlusSeriesField_ofWithZeroValuation_of_lt_one
      (v := v) (p := p)
      (principalUnitSubOneOfWithZeroValuation v u) hnK hnval hvx hcomplete

theorem

tendsto_principalUnitLogPartialSum_ofWithZeroValuation

L536 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.tendsto_principalUnitLogPartialSum_ofWithZeroValuation

Documentation

The finite logarithm polynomials of a first principal unit converge to the principal-unit logarithm-series 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 · full declaration

theorem tendsto_principalUnitLogPartialSum_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto
      (fun N : ℕ =>
        principalUnitLogPartialSumOfWithZeroValuation v u hnK N)
      atTop (𝓝 (principalUnitLogSeriesOfWithZeroValuation v u hnK)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hvx :
      v (principalUnitSubOneOfWithZeroValuation v u) <
        (1 : WithZero (Multiplicative ℤ)) :=
    principalUnitSubOne_val_lt_one_ofWithZeroValuation v u
  simpa [principalUnitLogPartialSumOfWithZeroValuation,
    principalUnitLogSeriesOfWithZeroValuation] using
    tendsto_logOnePlusPartialSumField_ofWithZeroValuation_of_lt_one
      (v := v) (p := p)
      (principalUnitSubOneOfWithZeroValuation v u) hnK hnval hvx hcomplete

theorem

hasSum_principalUnitLogSeries_add_ofWithZeroValuation

L566 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.hasSum_principalUnitLogSeries_add_ofWithZeroValuation

Documentation

The termwise sum of the two principal-unit logarithm series has value Log(u) + Log(w).

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_principalUnitLogSeries_add_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum
      (fun n : ℕ =>
        signedLogSeriesTermField
            (principalUnitSubOneOfWithZeroValuation v u) hnK n +
          signedLogSeriesTermField
            (principalUnitSubOneOfWithZeroValuation v w) hnK n)
      (principalUnitLogSeriesOfWithZeroValuation v u hnK +
        principalUnitLogSeriesOfWithZeroValuation v w hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  exact
    (hasSum_principalUnitLogSeries_ofWithZeroValuation
      (v := v) (p := p) u hnK hnval hcomplete).add
      (hasSum_principalUnitLogSeries_ofWithZeroValuation
        (v := v) (p := p) w hnK hnval hcomplete)

theorem

principalUnitLogPartialSum_add_eq_sum_add_terms_ofWithZeroValuation

L595 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogPartialSum_add_eq_sum_add_terms_ofWithZeroValuation

Documentation

Finite logarithm polynomials for two principal units add term by term.

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 principalUnitLogPartialSum_add_eq_sum_add_terms_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (N : ℕ) :
    principalUnitLogPartialSumOfWithZeroValuation v u hnK N +
        principalUnitLogPartialSumOfWithZeroValuation v w hnK N =
      ∑ n ∈ Finset.range N,
        (signedLogSeriesTermField
            (principalUnitSubOneOfWithZeroValuation v u) hnK n +
          signedLogSeriesTermField
            (principalUnitSubOneOfWithZeroValuation v w) hnK n)

theorem

tendsto_principalUnitLogPartialSum_add_ofWithZeroValuation

L614 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.tendsto_principalUnitLogPartialSum_add_ofWithZeroValuation

Documentation

The sum of two finite principal-unit logarithm polynomials converges to Log(u) + Log(w).

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_principalUnitLogPartialSum_add_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto
      (fun N : ℕ =>
        principalUnitLogPartialSumOfWithZeroValuation v u hnK N +
          principalUnitLogPartialSumOfWithZeroValuation v w hnK N)
      atTop
      (𝓝 (principalUnitLogSeriesOfWithZeroValuation v u hnK +
        principalUnitLogSeriesOfWithZeroValuation v w hnK)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hu :=
    tendsto_principalUnitLogPartialSum_ofWithZeroValuation
      (v := v) (p := p) u hnK hnval hcomplete
  have hw :=
    tendsto_principalUnitLogPartialSum_ofWithZeroValuation
      (v := v) (p := p) w hnK hnval hcomplete
  exact hu.add hw

theorem

eq_of_tendsto_sub_zero

L647 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.eq_of_tendsto_sub_zero

Documentation

If two convergent field-valued sequences differ by a sequence converging to zero, then their limits agree. This is the topological endpoint used to turn the formal logarithm product defect into actual additivity of the local logarithm.

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 eq_of_tendsto_sub_zero
    [TopologicalSpace K] [T2Space K] [ContinuousAdd K] [ContinuousNeg K]
    {f g : ℕ → K} {a b : K}
    (hf : Tendsto f atTop (𝓝 a))
    (hg : Tendsto g atTop (𝓝 b))
    (hsub : Tendsto (fun n => f n - g n) atTop (𝓝 0)) :
    a = b := by
  have hfg :
      Tendsto (fun n => (f n - g n) + g n) atTop (𝓝 (0 + b)) :=
    hsub.add hg
  have hf' : Tendsto f atTop (𝓝 b) := by
    simpa [sub_eq_add_neg, add_assoc] using hfg
  exact tendsto_nhds_unique hf hf'

theorem

principalUnitLogPartialSum_product_defect_eq_field_defect_ofWithZeroValuation

L663 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogPartialSum_product_defect_eq_field_defect_ofWithZeroValuation

Documentation

The principal-unit logarithm product defect is the same as the field-level defect for the two additive parameters u - 1 and w - 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 · statement

theorem principalUnitLogPartialSum_product_defect_eq_field_defect_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (N : ℕ) :
    principalUnitLogPartialSumOfWithZeroValuation v (u * w) hnK N -
        (principalUnitLogPartialSumOfWithZeroValuation v u hnK N +
          principalUnitLogPartialSumOfWithZeroValuation v w hnK N) =
      logOnePlusPartialSumField
          (principalUnitSubOneOfWithZeroValuation v u +
            principalUnitSubOneOfWithZeroValuation v w +
              principalUnitSubOneOfWithZeroValuation v u *
                principalUnitSubOneOfWithZeroValuation v w) hnK N -
        (logOnePlusPartialSumField
            (principalUnitSubOneOfWithZeroValuation v u) hnK N +
          logOnePlusPartialSumField
            (principalUnitSubOneOfWithZeroValuation v w) hnK N)

theorem

principalUnitLogSeries_mul_eq_add_of_tendsto_defect_ofWithZeroValuation

L688 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_mul_eq_add_of_tendsto_defect_ofWithZeroValuation

Documentation

Principal-unit logarithm additivity reduced to the one remaining analytic bridge: the difference between the product logarithm partial sums and the sum of the two logarithm partial sums tends to zero. The formal identity proved above supplies the coefficient cancellation for this defect; this lemma records the exact topological endpoint needed by the field-unit logarithm theorem.

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 principalUnitLogSeries_mul_eq_add_of_tendsto_defect_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      Tendsto
        (fun N : ℕ =>
          principalUnitLogPartialSumOfWithZeroValuation v (u * w) hnK N -
            (principalUnitLogPartialSumOfWithZeroValuation v u hnK N +
              principalUnitLogPartialSumOfWithZeroValuation v w hnK N))
        atTop (𝓝 (0 : K))) :
    principalUnitLogSeriesOfWithZeroValuation v (u * w) hnK =
      principalUnitLogSeriesOfWithZeroValuation v u hnK +
        principalUnitLogSeriesOfWithZeroValuation v w hnK := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hprod :=
    tendsto_principalUnitLogPartialSum_ofWithZeroValuation
      (v := v) (p := p) (u * w) hnK hnval hcomplete
  have hadd :=
    tendsto_principalUnitLogPartialSum_add_ofWithZeroValuation
      (v := v) (p := p) u w hnK hnval hcomplete
  exact
    eq_of_tendsto_sub_zero
      (K := K) hprod hadd hdefect

theorem

principalUnitLogSeries_mul_eq_add_of_tendsto_field_defect_ofWithZeroValuation

L727 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeries_mul_eq_add_of_tendsto_field_defect_ofWithZeroValuation

Documentation

Field-level version of principalUnitLogSeries_mul_eq_add_of_tendsto_defect_ofWithZeroValuation. After this reduction, the remaining analytic work for the field-unit logarithm theorem is to prove that the displayed field-level defect tends to zero from the formal coefficient 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 · full declaration

theorem principalUnitLogSeries_mul_eq_add_of_tendsto_field_defect_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      Tendsto
        (fun N : ℕ =>
          logOnePlusPartialSumField
              (principalUnitSubOneOfWithZeroValuation v u +
                principalUnitSubOneOfWithZeroValuation v w +
                  principalUnitSubOneOfWithZeroValuation v u *
                    principalUnitSubOneOfWithZeroValuation v w) hnK N -
            (logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u) hnK N +
              logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v w) hnK N))
        atTop (𝓝 (0 : K))) :
    principalUnitLogSeriesOfWithZeroValuation v (u * w) hnK =
      principalUnitLogSeriesOfWithZeroValuation v u hnK +
        principalUnitLogSeriesOfWithZeroValuation v w hnK := by
  apply principalUnitLogSeries_mul_eq_add_of_tendsto_defect_ofWithZeroValuation
    (v := v) (p := p) u w hnK hnval hcomplete
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  simpa [principalUnitLogPartialSum_product_defect_eq_field_defect_ofWithZeroValuation
    (v := v) u w hnK] using hdefect

def

principalUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation

L765 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation

Documentation

Principal-unit logarithm as a multiplicative homomorphism, conditional only on the remaining field-level defect convergence. The codomain is written as Multiplicative K, so multiplication there is addition in the local field.

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

def principalUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      ∀ u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1,
        letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
        Tendsto
          (fun N : ℕ =>
            logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u +
                  principalUnitSubOneOfWithZeroValuation v w +
                    principalUnitSubOneOfWithZeroValuation v u *
                      principalUnitSubOneOfWithZeroValuation v w) hnK N -
              (logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v u) hnK N +
                logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v w) hnK N))
          atTop (𝓝 (0 : K))) :
    (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1 →*
      Multiplicative K where
  toFun u := Multiplicative.ofAdd
    (principalUnitLogSeriesOfWithZeroValuation v u hnK)
  map_one' := by
    simp
  map_mul' u w := by
    change
      Multiplicative.ofAdd
          (principalUnitLogSeriesOfWithZeroValuation v (u * w) hnK) =
        Multiplicative.ofAdd
          (principalUnitLogSeriesOfWithZeroValuation v u hnK +
            principalUnitLogSeriesOfWithZeroValuation v w hnK)
    rw [principalUnitLogSeries_mul_eq_add_of_tendsto_field_defect_ofWithZeroValuation
      (v := v) (p := p) u w hnK hnval hcomplete (hdefect u w)]

theorem

principalUnitLogSeriesHom_apply_toAdd_ofWithZeroValuation

L812 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogSeriesHom_apply_toAdd_ofWithZeroValuation

Documentation

Establishes the identity Multiplicative.toAdd (principalUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation (v := v) (p := p) hnK hnval hcomplete hdefect u) = principalUnitLogSeriesOfWithZeroValuation v u 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 · full declaration

theorem principalUnitLogSeriesHom_apply_toAdd_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      ∀ u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1,
        letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
        Tendsto
          (fun N : ℕ =>
            logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u +
                  principalUnitSubOneOfWithZeroValuation v w +
                    principalUnitSubOneOfWithZeroValuation v u *
                      principalUnitSubOneOfWithZeroValuation v w) hnK N -
              (logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v u) hnK N +
                logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v w) hnK N))
          atTop (𝓝 (0 : K)))
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) :
    Multiplicative.toAdd
        (principalUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation
          (v := v) (p := p) hnK hnval hcomplete hdefect u) =
      principalUnitLogSeriesOfWithZeroValuation v u hnK := by
  rfl

def

fieldUnitDecompositionLogHomOfPrincipalUnitHom

L849 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitDecompositionLogHomOfPrincipalUnitHom

Documentation

A homomorphism on first principal units extends to the three-factor decomposition of Kˣ by killing the Teichmuller root factor and the uniformizer factor. This is the algebraic extension shape used in the field-unit logarithm theorem after the principal-unit logarithm has been proved additive.

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

def fieldUnitDecompositionLogHomOfPrincipalUnitHom
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) :
    CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F →*
      Multiplicative A where
  toFun z := φ z.1.2
  map_one' := by
    simp
  map_mul' z w := by
    simp

theorem

fieldUnitDecompositionLogHomOfPrincipalUnitHom_apply

L865 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitDecompositionLogHomOfPrincipalUnitHom_apply

Documentation

The defining evaluation formula for fieldUnitDecompositionLogHomOfPrincipalUnitHom is fieldUnitDecompositionLogHomOfPrincipalUnitHom (F := F) φ z = φ z.1.2.

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 fieldUnitDecompositionLogHomOfPrincipalUnitHom_apply
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A)
    (z : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F) :
    fieldUnitDecompositionLogHomOfPrincipalUnitHom (F := F) φ z = φ z.1.2

theorem

fieldUnitDecompositionLogHomOfPrincipalUnitHom_root

L877 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitDecompositionLogHomOfPrincipalUnitHom_root

Documentation

Establishes the identity fieldUnitDecompositionLogHomOfPrincipalUnitHom (F := F) φ ((ζ, 1), (1 : Multiplicative ℤ)) = 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 · statement

theorem fieldUnitDecompositionLogHomOfPrincipalUnitHom_root
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A)
    (ζ : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F) :
    fieldUnitDecompositionLogHomOfPrincipalUnitHom (F := F) φ
        ((ζ, 1), (1 : Multiplicative ℤ)) = 1

theorem

fieldUnitDecompositionLogHomOfPrincipalUnitHom_principal

L891 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitDecompositionLogHomOfPrincipalUnitHom_principal

Documentation

Establishes the identity fieldUnitDecompositionLogHomOfPrincipalUnitHom (F := F) φ (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F), u), (1 : Multiplicative ℤ)) = φ u.

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 fieldUnitDecompositionLogHomOfPrincipalUnitHom_principal
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A)
    (u : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1) :
    fieldUnitDecompositionLogHomOfPrincipalUnitHom (F := F) φ
        (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F), u),
          (1 : Multiplicative ℤ)) = φ u

theorem

fieldUnitDecompositionLogHomOfPrincipalUnitHom_uniformizer

L906 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitDecompositionLogHomOfPrincipalUnitHom_uniformizer

Documentation

Establishes the identity fieldUnitDecompositionLogHomOfPrincipalUnitHom (F := F) φ (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F), (1 : (CompleteDVF.higherPrincipalUnitGroup F) 1)), Multiplicative.ofAdd m) = 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 · statement

theorem fieldUnitDecompositionLogHomOfPrincipalUnitHom_uniformizer
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A)
    (m : ℤ) :
    fieldUnitDecompositionLogHomOfPrincipalUnitHom (F := F) φ
        (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F),
            (1 : (CompleteDVF.higherPrincipalUnitGroup F) 1)),
          Multiplicative.ofAdd m) = 1

def

fieldUnitLogHomOfPrincipalUnitHom

L920 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomOfPrincipalUnitHom

Documentation

A field-unit logarithm homomorphism obtained from a chosen the uniformizer–residue–principal-unit decomposition three-factor decomposition and a principal-unit logarithm homomorphism.

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 fieldUnitLogHomOfPrincipalUnitHom
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (e : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) :
    Kˣ →* Multiplicative A

theorem

fieldUnitLogHomOfPrincipalUnitHom_apply

L933 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomOfPrincipalUnitHom_apply

Documentation

The defining evaluation formula for fieldUnitLogHomOfPrincipalUnitHom is fieldUnitLogHomOfPrincipalUnitHom (F := F) e φ x = φ ((e.symm x).1.2).

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 fieldUnitLogHomOfPrincipalUnitHom_apply
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (e : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (x : Kˣ) :
    fieldUnitLogHomOfPrincipalUnitHom (F := F) e φ x =
      φ ((e.symm x).1.2)

theorem

fieldUnitLogHomOfPrincipalUnitHom_apply_of_decomposition_eq

L943 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomOfPrincipalUnitHom_apply_of_decomposition_eq

Documentation

Establishes the identity fieldUnitLogHomOfPrincipalUnitHom (F := F) e φ x = φ z.1.2.

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 fieldUnitLogHomOfPrincipalUnitHom_apply_of_decomposition_eq
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (e : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A)
    (z : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F)
    {x : Kˣ} (hx : e z = x) :
    fieldUnitLogHomOfPrincipalUnitHom (F := F) e φ x = φ z.1.2

theorem

fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_root_decomposition

L955 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_root_decomposition

Documentation

Establishes the identity fieldUnitLogHomOfPrincipalUnitHom (F := F) e φ x = 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 · statement

theorem fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_root_decomposition
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (e : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A)
    (ζ : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)
    {x : Kˣ}
    (hx : e ((ζ, 1), (1 : Multiplicative ℤ)) = x) :
    fieldUnitLogHomOfPrincipalUnitHom (F := F) e φ x = 1

theorem

fieldUnitLogHomOfPrincipalUnitHom_eq_of_principal_decomposition

L969 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomOfPrincipalUnitHom_eq_of_principal_decomposition

Documentation

Establishes the identity fieldUnitLogHomOfPrincipalUnitHom (F := F) e φ x = φ u.

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 fieldUnitLogHomOfPrincipalUnitHom_eq_of_principal_decomposition
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (e : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A)
    (u : (CompleteDVF.higherPrincipalUnitGroup F) 1) {x : Kˣ}
    (hx :
      e (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F),
          u), (1 : Multiplicative ℤ)) = x) :
    fieldUnitLogHomOfPrincipalUnitHom (F := F) e φ x = φ u

theorem

fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_uniformizer_decomposition

L986 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_uniformizer_decomposition

Documentation

Establishes the identity fieldUnitLogHomOfPrincipalUnitHom (F := F) e φ x = 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 · statement

theorem fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_uniformizer_decomposition
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (e : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A)
    (m : ℤ) {x : Kˣ}
    (hx :
      e (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F),
          (1 : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1)),
        Multiplicative.ofAdd m) = x) :
    fieldUnitLogHomOfPrincipalUnitHom (F := F) e φ x = 1

theorem

fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_completeDVF_root

L1009 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_completeDVF_root

Documentation

public root-factor value of the field-unit logarithm constructed from the complete-DVF uniformizer decomposition.

Source context 13 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]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
   fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF_apply) in

Lean source · statement

theorem fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_completeDVF_root
    (F : CompleteDVF K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A)
    (ζ : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F) :
    fieldUnitLogHomOfPrincipalUnitHom
        (F := F)
        (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
          F hπ) φ
        (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (ζ : F.valuationSubringˣ)) = 1

theorem

fieldUnitLogHomOfPrincipalUnitHom_eq_of_completeDVF_principal

L1035 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomOfPrincipalUnitHom_eq_of_completeDVF_principal

Documentation

public principal-unit value of the field-unit logarithm constructed from the complete-DVF uniformizer decomposition.

Source context 13 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]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
   fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF_apply) in

Lean source · statement

theorem fieldUnitLogHomOfPrincipalUnitHom_eq_of_completeDVF_principal
    (F : CompleteDVF K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A)
    (u : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1) :
    fieldUnitLogHomOfPrincipalUnitHom
        (F := F)
        (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
          F hπ) φ
        (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (u : F.valuationSubringˣ)) = φ u

theorem

fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_completeDVF_uniformizer

L1062 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_completeDVF_uniformizer

Documentation

public uniformizer value of the field-unit logarithm constructed from the complete-DVF uniformizer decomposition: the selected uniformizer is sent to zero, written as 1 in Multiplicative A.

Source context 13 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]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
   fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF_apply) in

Lean source · statement

theorem fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_completeDVF_uniformizer
    (F : CompleteDVF K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) :
    fieldUnitLogHomOfPrincipalUnitHom
        (F := F)
        (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
          F hπ) φ
        (Units.mk0 (π : K) hπ.ne_zero) = 1

def

fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation

L1085 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation

Documentation

Conditional field-unit logarithm for the field-unit logarithm theorem: once the remaining field-level defect convergence proves additivity on U¹, the resulting principal-unit logarithm extends over a chosen field-unit decomposition by sending the root and uniformizer factors 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

def fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    [Finite (completeDVFOfWithZeroValuation v).residueField]
    (e :
      CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors
          (completeDVFOfWithZeroValuation v) ≃* Kˣ)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      ∀ u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1,
        letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
        Tendsto
          (fun N : ℕ =>
            logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u +
                  principalUnitSubOneOfWithZeroValuation v w +
                    principalUnitSubOneOfWithZeroValuation v u *
                      principalUnitSubOneOfWithZeroValuation v w) hnK N -
              (logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v u) hnK N +
                logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v w) hnK N))
          atTop (𝓝 (0 : K))) :
    Kˣ →* Multiplicative K :=
  fieldUnitLogHomOfPrincipalUnitHom
    (F := completeDVFOfWithZeroValuation v) e
    (principalUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation
      (v := v) (p := p) hnK hnval hcomplete hdefect)

def

fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer

L1128 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer

Documentation

public conditional logarithm on Kˣ, using the complete-DVF uniformizer decomposition supplied by the uniformizer–residue–principal-unit decomposition. This is the same construction as fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation, with the decomposition chosen canonically from a uniformizer.

Source context 13 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]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF) in

Lean source · full declaration

def fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    [Finite (completeDVFOfWithZeroValuation v).residueField]
    {π : (completeDVFOfWithZeroValuation v).valuationSubring}
    (hπ : v.IsUniformizer (π : K))
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      ∀ u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1,
        letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
        Tendsto
          (fun N : ℕ =>
            logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u +
                  principalUnitSubOneOfWithZeroValuation v w +
                    principalUnitSubOneOfWithZeroValuation v u *
                      principalUnitSubOneOfWithZeroValuation v w) hnK N -
              (logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v u) hnK N +
                logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v w) hnK N))
          atTop (𝓝 (0 : K))) :
    Kˣ →* Multiplicative K :=
  fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation
    (v := v) (p := p)
    (e :=
      fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
        (completeDVFOfWithZeroValuation v) hπ)
    hnK hnval hcomplete hdefect

theorem

fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_principal

L1167 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_principal

Documentation

On first principal units, the public conditional field-unit logarithm agrees with the principal-unit logarithm.

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 fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_principal
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    [Finite (completeDVFOfWithZeroValuation v).residueField]
    {π : (completeDVFOfWithZeroValuation v).valuationSubring}
    (hπ : v.IsUniformizer (π : K))
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      ∀ u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1,
        letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
        Tendsto
          (fun N : ℕ =>
            logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u +
                  principalUnitSubOneOfWithZeroValuation v w +
                    principalUnitSubOneOfWithZeroValuation v u *
                      principalUnitSubOneOfWithZeroValuation v w) hnK N -
              (logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v u) hnK N +
                logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v w) hnK N))
          atTop (𝓝 (0 : K)))
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) :
    fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer
        (v := v) (p := p) hπ hnK hnval hcomplete hdefect
        (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom
          (completeDVFOfWithZeroValuation v) (u : _)) =
      principalUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete hdefect u := by
  simpa [fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer,
    fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation] using
    fieldUnitLogHomOfPrincipalUnitHom_eq_of_completeDVF_principal
      (F := completeDVFOfWithZeroValuation v) hπ
      (principalUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete hdefect) u

theorem

fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_principal_toAdd

L1212 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_principal_toAdd

Documentation

Additive-value form of the preceding principal-unit evaluation: on U¹, the public field-unit logarithm is 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 · full declaration

theorem fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_principal_toAdd
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    [Finite (completeDVFOfWithZeroValuation v).residueField]
    {π : (completeDVFOfWithZeroValuation v).valuationSubring}
    (hπ : v.IsUniformizer (π : K))
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      ∀ u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1,
        letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
        Tendsto
          (fun N : ℕ =>
            logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u +
                  principalUnitSubOneOfWithZeroValuation v w +
                    principalUnitSubOneOfWithZeroValuation v u *
                      principalUnitSubOneOfWithZeroValuation v w) hnK N -
              (logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v u) hnK N +
                logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v w) hnK N))
          atTop (𝓝 (0 : K)))
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) :
    Multiplicative.toAdd
        (fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer
          (v := v) (p := p) hπ hnK hnval hcomplete hdefect
          (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom
            (completeDVFOfWithZeroValuation v) (u : _))) =
      principalUnitLogSeriesOfWithZeroValuation v u hnK := by
  rw [fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_principal
    (v := v) (p := p) hπ hnK hnval hcomplete hdefect u]
  rfl

theorem

fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_root

L1254 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_root

Documentation

Teichmuller root factors have logarithm zero for the public conditional field-unit logarithm.

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 fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_root
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    [Finite (completeDVFOfWithZeroValuation v).residueField]
    {π : (completeDVFOfWithZeroValuation v).valuationSubring}
    (hπ : v.IsUniformizer (π : K))
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      ∀ u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1,
        letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
        Tendsto
          (fun N : ℕ =>
            logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u +
                  principalUnitSubOneOfWithZeroValuation v w +
                    principalUnitSubOneOfWithZeroValuation v u *
                      principalUnitSubOneOfWithZeroValuation v w) hnK N -
              (logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v u) hnK N +
                logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v w) hnK N))
          atTop (𝓝 (0 : K)))
    (ζ :
      CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup
        (completeDVFOfWithZeroValuation v)) :
    fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer
        (v := v) (p := p) hπ hnK hnval hcomplete hdefect
        (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom
          (completeDVFOfWithZeroValuation v) (ζ : _)) = 1 := by
  simpa [fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer,
    fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation] using
    fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_completeDVF_root
      (F := completeDVFOfWithZeroValuation v) hπ
      (principalUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete hdefect) ζ

theorem

fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_root_toAdd

L1299 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_root_toAdd

Documentation

Additive-value form of the Teichmuller-root evaluation: root factors have field-unit logarithm 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 · full declaration

theorem fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_root_toAdd
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    [Finite (completeDVFOfWithZeroValuation v).residueField]
    {π : (completeDVFOfWithZeroValuation v).valuationSubring}
    (hπ : v.IsUniformizer (π : K))
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      ∀ u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1,
        letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
        Tendsto
          (fun N : ℕ =>
            logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u +
                  principalUnitSubOneOfWithZeroValuation v w +
                    principalUnitSubOneOfWithZeroValuation v u *
                      principalUnitSubOneOfWithZeroValuation v w) hnK N -
              (logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v u) hnK N +
                logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v w) hnK N))
          atTop (𝓝 (0 : K)))
    (ζ :
      CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup
        (completeDVFOfWithZeroValuation v)) :
    Multiplicative.toAdd
        (fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer
          (v := v) (p := p) hπ hnK hnval hcomplete hdefect
          (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom
            (completeDVFOfWithZeroValuation v) (ζ : _))) = 0 := by
  rw [fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_root
    (v := v) (p := p) hπ hnK hnval hcomplete hdefect ζ]
  rfl

theorem

fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_uniformizer

L1342 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_uniformizer

Documentation

The selected uniformizer has logarithm zero for the public conditional field-unit logarithm.

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 fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_uniformizer
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    [Finite (completeDVFOfWithZeroValuation v).residueField]
    {π : (completeDVFOfWithZeroValuation v).valuationSubring}
    (hπ : v.IsUniformizer (π : K))
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      ∀ u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1,
        letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
        Tendsto
          (fun N : ℕ =>
            logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u +
                  principalUnitSubOneOfWithZeroValuation v w +
                    principalUnitSubOneOfWithZeroValuation v u *
                      principalUnitSubOneOfWithZeroValuation v w) hnK N -
              (logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v u) hnK N +
                logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v w) hnK N))
          atTop (𝓝 (0 : K))) :
    fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer
        (v := v) (p := p) hπ hnK hnval hcomplete hdefect
        (Units.mk0 (π : K) hπ.ne_zero) = 1 := by
  simpa [fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer,
    fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation] using
    fieldUnitLogHomOfPrincipalUnitHom_eq_one_of_completeDVF_uniformizer
      (F := completeDVFOfWithZeroValuation v) hπ
      (principalUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete hdefect)

theorem

fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_uniformizer_toAdd

L1383 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_uniformizer_toAdd

Documentation

Additive-value form of the uniformizer evaluation: the selected uniformizer has field-unit logarithm 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 · full declaration

theorem fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_uniformizer_toAdd
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    [Finite (completeDVFOfWithZeroValuation v).residueField]
    {π : (completeDVFOfWithZeroValuation v).valuationSubring}
    (hπ : v.IsUniformizer (π : K))
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hdefect :
      ∀ u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1,
        letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
        Tendsto
          (fun N : ℕ =>
            logOnePlusPartialSumField
                (principalUnitSubOneOfWithZeroValuation v u +
                  principalUnitSubOneOfWithZeroValuation v w +
                    principalUnitSubOneOfWithZeroValuation v u *
                      principalUnitSubOneOfWithZeroValuation v w) hnK N -
              (logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v u) hnK N +
                logOnePlusPartialSumField
                  (principalUnitSubOneOfWithZeroValuation v w) hnK N))
          atTop (𝓝 (0 : K))) :
    Multiplicative.toAdd
        (fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer
          (v := v) (p := p) hπ hnK hnval hcomplete hdefect
          (Units.mk0 (π : K) hπ.ne_zero)) = 0 := by
  rw [fieldUnitLogSeriesHomOfTendstoFieldDefect_ofWithZeroValuationUniformizer_uniformizer
    (v := v) (p := p) hπ hnK hnval hcomplete hdefect]
  rfl

Module documentation

Declarations