OAI/NumberTheory/DukePrimeDegree/Dynamics/CentralizerWeights.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An explicit neutral direction excluding centralizer orbits

The two root coordinates receive the same negative weight. The remaining coordinates receive distinct positive weights. Their sum is balanced by the repeated negative weight. This discharges the elementary weight conditions in the centralizer-orbit exclusion.

  1. def OAI.DukePrimeDegree.centralizerWitnessWeights line 21
  2. lemma OAI.DukePrimeDegree.centralizerWitnessWeights_sum line 25
  3. lemma OAI.DukePrimeDegree.centralizerWitnessWeights_neutral line 33
  4. lemma OAI.DukePrimeDegree.centralizerWitnessWeights_negative line 38
  5. lemma OAI.DukePrimeDegree.centralizerWitnessWeights_injective line 48
  6. theorem OAI.DukePrimeDegree.no_invariant_rootPair_orbit line 58

    Source documentation

    No nonzero finite measure invariant under the neutral diagonal group can be supported on a single root-pair centralizer orbit.

    theorem no_invariant_rootPair_orbit {n m : ℕ}
    (e : Fin n ≃ Fin 2 ⊕ Fin m) (hm : 0 < m)
    (hij : e.symm (Sum.inl 0) ≠ e.symm (Sum.inl 1))
    (μ : Measure (X n)) [IsFiniteMeasure μ] [NeZero μ]
    (x : X n)
    (hfull : ∀ᵐ y ∂μ, ∃ h : rootPairCentralizer hij, rightAction x (h : G n) = y)
    (hinv : ∀ (ell : Fin n → ℝ) (hell : ∑ r, ell r = 0),
      ell (e.symm (Sum.inl 0)) = ell (e.symm (Sum.inl 1)) →
      μ.map (fun y => rightAction y (diagonalOneParameter ell hell 1)) = μ) : False := by
…

    Mentions: OAI.DukePrimeDegree.rootPairCentralizer