MainUnconditional.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Prime-degree torus-packet equidistribution

The manuscript's full packet theorem, after discharging both the Stark zero-exclusion input and the prime-degree positive-entropy rigidity input. The lattice and field may vary, so nonmaximal multiplier orders and arbitrary prescribed local homothety types are included. Tightness gives no escape of mass for the complete volume-weighted packets.

theorem OAI.DukePrimeDegree.prime_degree_packet_equidistribution_unconditional line 24

Source documentation

Theorem 1.1: complete volume-weighted packets converge to Haar probability as their multiplier-order discriminants tend to infinity.

theorem prime_degree_packet_equidistribution_unconditional
    (d : ℕ) (hprime : Nat.Prime (d+1)) (hfive : 5 ≤ d+1)
    (K : ℕ → Type u) [∀ i, Field (K i)] [∀ i, NumberField (K i)]
    [∀ i, NumberField.IsTotallyReal (K i)]
    (M : ∀ i, PrimeDegreePackets.FullLattice (d+1) (K i))
    (σ : ∀ i, OrderedEmbeddings (d+1) (K i))
    (hn : ∀ i, Module.finrank ℚ (K i)=d+1)
    (hD : Tendsto (fun i => PrimeDegreePackets.multiplierDiscriminant (M i)) atTop atTop) :
    ∃ ν : ProbabilityMeasure (X (d+1)),
      IsHaarProbability (ν : Measure (X (d+1))) ∧
      Tendsto (fun i => packetProbability (M i) (σ i) (hn i)
        (hprime.odd_of_ne_two (by omega))) atTop (𝓝 ν) ∧
…

Mentions: OAI.PrimeDegreePackets.FullLattice, OAI.PrimeDegreePackets.multiplierDiscriminant

theorem OAI.DukePrimeDegree.prime_degree_packets_tendsto_haar_unconditional line 41

Source documentation

The same packets converge to any specified Haar probability.

theorem prime_degree_packets_tendsto_haar_unconditional
    (d : ℕ) (hprime : Nat.Prime (d+1)) (hfive : 5 ≤ d+1)
    (K : ℕ → Type u) [∀ i, Field (K i)] [∀ i, NumberField (K i)]
    [∀ i, NumberField.IsTotallyReal (K i)]
    (M : ∀ i, PrimeDegreePackets.FullLattice (d+1) (K i))
    (σ : ∀ i, OrderedEmbeddings (d+1) (K i))
    (hn : ∀ i, Module.finrank ℚ (K i)=d+1)
    (hD : Tendsto (fun i => PrimeDegreePackets.multiplierDiscriminant (M i)) atTop atTop)
    (m : ProbabilityMeasure (X (d+1)))
    (hm : IsHaarProbability (m : Measure (X (d+1)))) :
    Tendsto (fun i => packetProbability (M i) (σ i) (hn i)
      (hprime.odd_of_ne_two (by omega))) atTop (𝓝 m) := by
…

Mentions: OAI.PrimeDegreePackets.FullLattice, OAI.PrimeDegreePackets.multiplierDiscriminant

theorem OAI.DukePrimeDegree.prime_degree_packet_measure_equidistribution_unconditional line 60

Source documentation

Theorem 1.1 as weak convergence of the actual complete packet measures, including tightness of the entire family.

Distinct definitions of this name: ComparatorChallenges/DukePrimeDegree.lean:200 (same statement text; different proof or body). Qualify references as OAI.DukePrimeDegree.prime_degree_packet_measure_equidistribution_unconditional@path.

theorem prime_degree_packet_measure_equidistribution_unconditional
    (d : ℕ) (hprime : Nat.Prime (d+1)) (hfive : 5 ≤ d+1)
    (K : ℕ → Type u) [∀ i, Field (K i)] [∀ i, NumberField (K i)]
    [∀ i, NumberField.IsTotallyReal (K i)]
    (M : ∀ i, PrimeDegreePackets.FullLattice (d+1) (K i))
    (σ : ∀ i, OrderedEmbeddings (d+1) (K i))
    (hn : ∀ i, Module.finrank ℚ (K i)=d+1)
    (hD : Tendsto (fun i => PrimeDegreePackets.multiplierDiscriminant (M i)) atTop atTop) :
    ∃ ν : Measure (X (d+1)), IsHaarProbability ν ∧
      WeakProbabilityConvergence (fun i => packetMeasure (M i) (σ i)) ν ∧
      IsTightMeasureSet (Set.range (fun i => packetMeasure (M i) (σ i))) := by
…

Mentions: OAI.PrimeDegreePackets.FullLattice, OAI.PrimeDegreePackets.multiplierDiscriminant

theorem OAI.DukePrimeDegree.prime_degree_packet_measures_tendsto_haar_unconditional line 80

Source documentation

The complete packet measures converge weakly to any specified Haar probability, in the formulation by bounded continuous test functions.

Distinct definitions of this name: ComparatorChallenges/DukePrimeDegree.lean:215 (same statement text; different proof or body). Qualify references as OAI.DukePrimeDegree.prime_degree_packet_measures_tendsto_haar_unconditional@path.

theorem prime_degree_packet_measures_tendsto_haar_unconditional
    (d : ℕ) (hprime : Nat.Prime (d+1)) (hfive : 5 ≤ d+1)
    (K : ℕ → Type u) [∀ i, Field (K i)] [∀ i, NumberField (K i)]
    [∀ i, NumberField.IsTotallyReal (K i)]
    (M : ∀ i, PrimeDegreePackets.FullLattice (d+1) (K i))
    (σ : ∀ i, OrderedEmbeddings (d+1) (K i))
    (hn : ∀ i, Module.finrank ℚ (K i)=d+1)
    (hD : Tendsto (fun i => PrimeDegreePackets.multiplierDiscriminant (M i)) atTop atTop)
    (m : ProbabilityMeasure (X (d+1)))
    (hm : IsHaarProbability (m : Measure (X (d+1)))) :
    WeakProbabilityConvergence (fun i => packetMeasure (M i) (σ i))
      (m : Measure (X (d+1))) := by
…

Mentions: OAI.PrimeDegreePackets.FullLattice, OAI.PrimeDegreePackets.multiplierDiscriminant