NYLL
Module

LogDenominatorLowerBound.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.LogDenominatorLowerBound
2 declarations indexed from sourceView source ↗

Module documentation

Lower bounds and a minimum for logarithm denominators

Linear growth dominates the logarithmic denominator contribution, so a single integer lies strictly below every term of the resulting real sequence. The corresponding integer sequence using padicValNat therefore attains a minimum.

Imports5
Imported by2

Declarations

theorem

exists_int_lt_log_denominator_bound

L25 ↗
LocalFieldTheory.DiscreteValuationField.exists_int_lt_log_denominator_bound
Documentation

The logarithmic denominator estimate has an integer lower bound uniform in the series index. This arithmetic statement does not require p to be prime.

Source context 1 command

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

namespace LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem exists_int_lt_log_denominator_bound (p e : ℕ) :
    ∃ b : ℤ, ∀ n : ℕ,
      (b : ℝ) < ((n + 1 : ℕ) : ℝ) -
        (e : ℝ) * Real.logb (p : ℝ) ((n + 1 : ℕ) : ℝ)
theorem

exists_log_denominator_min

L42 ↗
LocalFieldTheory.DiscreteValuationField.exists_log_denominator_min
Documentation

The exact integer denominator estimate attains a minimum at some series index, with the lower bound constructed from logarithmic domination.

Source context 1 command

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

namespace LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem exists_log_denominator_min (p e : ℕ) [Fact p.Prime] :
    ∃ m : ℕ, ∀ n : ℕ,
      ((m + 1 : ℕ) : ℤ) - (e : ℤ) * (padicValNat p (m + 1) : ℤ) ≤
        ((n + 1 : ℕ) : ℤ) - (e : ℤ) * (padicValNat p (n + 1) : ℤ)

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