OAI/NumberTheory/DukePrimeDegree/Dynamics/SingleBlockOrbitExistence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A positive-mass block orbit from actual root ergodicity

Local block preservation of the measure stabilizer supplies the fixed transverse shell. Haar patches supply the common corrections, and root ergodicity supplies a common generic set. If every block orbit were null, the resulting normalized transverse pairs would contradict the fixed-window shearing estimate.

  1. lemma OAI.DukePrimeDegree.exists_positive_real_fiber_budget line 27
  2. theorem OAI.DukePrimeDegree.exists_positive_singleBlock_orbit_of_patch line 44
  3. theorem OAI.DukePrimeDegree.exists_positive_singleBlock_orbit line 94

    Source documentation

    The correction patches are constructed from Haar measure on the closed root group; no patch or homogeneous-orbit assumption remains.

    theorem exists_positive_singleBlock_orbit {n : ℕ}
    (S : Finset (Fin n)) (k l : Fin n) (hkl : k ≠ l) (hk : k ∈ S) (hl : l ∈ S)
    (μ : Measure (X n)) [IsProbabilityMeasure μ]
    [ErgodicSMul (singleBlockRootGroup (S : Set (Fin n))) (X n) μ]
    (hlocal : {g : invariantRightSubgroup μ |
      g.val ∈ blockMatrixGroup (blockComplementSetoid (S : Set (Fin n)))} ∈
        𝓝 (1 : invariantRightSubgroup μ)) :
    ∃ g : G n,
      μ (range (latticeOrbitPoint g (blockMatrixGroup (blockComplementSetoid (S : Set (Fin n)))))) ≠ 0 := by
…

    Mentions: OAI.DukePrimeDegree.singleBlockRootGroup, OAI.DukePrimeDegree.blockMatrixGroup, OAI.DukePrimeDegree.blockComplementSetoid, OAI.DukePrimeDegree.latticeOrbitPoint