OrderDiscriminant.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The multiplier-order index

The conductor inclusion bounds the index of the multiplier order by q^n. This is the integer-index part of the discriminant-scale bound in Section 2 of paper 031-01. The discriminant is expressed by the usual index formula |disc K| [O_K : O(M)]².

def OAI.DukePrimeDegree.integralMultiplierLattice line 25
Source documentation
The multiplier order as a submodule of the maximal order.
```
def integralMultiplierLattice (M : Submodule ℤ K) : Submodule ℤ (𝓞 K) :=
…
```
def OAI.DukePrimeDegree.multiplierIndex line 30
Source documentation
Index of the multiplier order inside the maximal order.
```
noncomputable def multiplierIndex (M : Submodule ℤ K) : ℕ :=
…
```
lemma OAI.DukePrimeDegree.range_nsmul_le_integralMultiplierLattice line 34
lemma OAI.DukePrimeDegree.FullLattice.multiplierIndex_le line 44
Source documentation
The index bound does not require an invertible module over the multiplier order. It uses only the full-lattice property.
```
lemma FullLattice.multiplierIndex_le (M : FullLattice K) :
    multiplierIndex M.toSubmodule ≤
      saturationIndex M.toSubmodule ^ Module.finrank ℚ K := by
…
```
Mentions: OAI.DukePrimeDegree.FullLattice, OAI.DukePrimeDegree.multiplierIndex, OAI.DukePrimeDegree.saturationIndex
lemma OAI.DukePrimeDegree.FullLattice.multiplierIndex_pos line 53
def OAI.DukePrimeDegree.multiplierDiscriminant line 62
Source documentation
The absolute order discriminant in the index convention.
```
noncomputable def multiplierDiscriminant (M : Submodule ℤ K) : ℕ :=
…
```
lemma OAI.DukePrimeDegree.FullLattice.multiplierDiscriminant_le line 65
def OAI.DukePrimeDegree.arithmeticScale line 79
Source documentation
The unfolding scale Q = [O_K M : M] √|disc K|.
```
noncomputable def arithmeticScale (M : Submodule ℤ K) : ℝ :=
…
```
lemma OAI.DukePrimeDegree.FullLattice.arithmeticScale_pos line 82
lemma OAI.DukePrimeDegree.FullLattice.multiplierDiscriminant_le_scale line 90
Source documentation
The discriminant grows no faster than the 2nth power of the unfolding scale. No discriminant lower bound beyond nonvanishing is used.
```
lemma FullLattice.multiplierDiscriminant_le_scale (M : FullLattice K) :
    (multiplierDiscriminant M.toSubmodule : ℝ) ≤
      arithmeticScale M.toSubmodule ^ (2 * Module.finrank ℚ K) := by
…
```
Mentions: OAI.DukePrimeDegree.FullLattice, OAI.DukePrimeDegree.multiplierDiscriminant, OAI.DukePrimeDegree.arithmeticScale

theorem OAI.DukePrimeDegree.arithmeticScale_tendsto_atTop line 118

Source documentation

For a fixed degree, divergence of order discriminants forces the unfolding scale to diverge, including sequences in a fixed number field.

theorem arithmeticScale_tendsto_atTop
    (K : ℕ → Type*) [∀ i, Field (K i)] [∀ i, NumberField (K i)]
    (M : ∀ i, FullLattice (K i)) (n : ℕ)
    (hn : ∀ i, Module.finrank ℚ (K i) = n)
    (hD : Tendsto (fun i => (multiplierDiscriminant (M i).toSubmodule : ℝ)) atTop atTop) :
    Tendsto (fun i => arithmeticScale (M i).toSubmodule) atTop atTop := by
…

Mentions: OAI.DukePrimeDegree.FullLattice, OAI.DukePrimeDegree.multiplierDiscriminant, OAI.DukePrimeDegree.arithmeticScale