MainConditional.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Conditional prime-degree packet equidistribution

Complete volume-weighted local-homothety packets converge to Haar probability and form a tight family under a residue-relative uniform zeta scale bound and prime-degree positive-entropy rigidity. The arithmetic and dynamical hypotheses concern the actual homogeneous lattice space and its diagonal action. A subsequential packet limit supplies Haar probability.

def OAI.DukePrimeDegree.EKLPrimeInput line 28
Source documentation
The published rigidity input, on the actual lattice space and with actual diagonal ergodicity and measure-theoretic entropy.
```
def EKLPrimeInput (d : ℕ) : Prop :=
…
```

theorem OAI.DukePrimeDegree.packet_limit_isHaar_of_scale_and_EKL line 38

Source documentation

Every weak packet limit is Haar under the analytic scale bound and published prime-degree rigidity.

theorem packet_limit_isHaar_of_scale_and_EKL
    (d : ℕ) (hprime : Nat.Prime (d + 1)) (hthree : 3 ≤ d + 1) (hodd : Odd (d + 1))
    (Hscale : UniformZetaScaleBound.{u} (d + 1)) (ekl : EKLPrimeInput d)
    (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)))
    (hlim : Tendsto (fun i => packetProbability (M i) (σ i) (hn i) hodd)
      atTop (𝓝 ν)) : IsHaarProbability (ν : Measure (X (d + 1))) := by
…

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

theorem OAI.DukePrimeDegree.prime_degree_packet_equidistribution_of_scale_and_EKL line 73

Source documentation

The full volume-weighted packet conclusion, including no escape of mass, conditional on the explicitly separated analytic and published rigidity inputs. The family may vary through arbitrary full lattices and arbitrary local homothety types.

theorem prime_degree_packet_equidistribution_of_scale_and_EKL
    (d : ℕ) (hprime : Nat.Prime (d + 1)) (hfive : 5 ≤ d + 1)
    (Hscale : UniformZetaScaleBound.{u} (d + 1)) (ekl : EKLPrimeInput d)
    (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)
…

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