OAI/NumberTheory/DukePrimeDegree/Dynamics/SingleBlockNormalization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Transverse representatives using only a single root block

On an ergodic component for a single root block, an arbitrary ambient diagonal correction need not preserve the component measure. Here the correction is a product of roots in that block. It clears the entries inside the block and equalizes its diagonal, leaving the complementary coordinates unrestricted.

  1. def OAI.DukePrimeDegree.singleBlockSetoid line 25
  2. lemma OAI.DukePrimeDegree.singleBlockSetoid_off_diagonal line 29
  3. lemma OAI.DukePrimeDegree.blockRootGroup_singleBlockSetoid line 35
  4. theorem OAI.DukePrimeDegree.supported_diagonal_mem_singleBlockRootGroup line 48

    Source documentation

    A diagonal supported on one coordinate block belongs to its actual root-generated group, provided its determinant is one.

    theorem supported_diagonal_mem_singleBlockRootGroup {n : ℕ}
    (S : Set (Fin n)) (i₀ : Fin n) (hi₀ : i₀ ∈ S)
    (D : Fin n → ℝ) (hdet : Matrix.det (Matrix.diagonal D) = 1)
    (hsupport : ∀ i, i ∉ S → D i = 1) :
    (⟨Matrix.diagonal D, hdet⟩ : G n) ∈ singleBlockRootGroup S := by
…

    Mentions: OAI.DukePrimeDegree.singleBlockRootGroup

  5. theorem OAI.DukePrimeDegree.supported_diagonalOneParameter_mem_singleBlockRootGroup line 71
  6. def OAI.DukePrimeDegree.singleBlockDiagonalMean line 80
  7. def OAI.DukePrimeDegree.singleBlockDiagonalWeights line 83
  8. lemma OAI.DukePrimeDegree.singleBlockDiagonalWeights_sum line 87
  9. def OAI.DukePrimeDegree.singleBlockDiagonalCorrection line 100
  10. lemma OAI.DukePrimeDegree.singleBlockDiagonalCorrection_mem line 105
  11. lemma OAI.DukePrimeDegree.mul_singleBlockDiagonalCorrection_mem line 114
  12. lemma OAI.DukePrimeDegree.singleBlockDiagonalCorrection_entry line 125
  13. lemma OAI.DukePrimeDegree.singleBlockDiagonalCorrection_diagonal line 134
  14. lemma OAI.DukePrimeDegree.singleBlockDiagonalCorrection_tendsto line 143
  15. theorem OAI.DukePrimeDegree.exists_singleBlock_transverse_sequence line 184

    Source documentation

    Both corrections remain in the single-block group. This is the normalization available on its actual ergodic components.

    theorem exists_singleBlock_transverse_sequence {n : ℕ}
    (S : Finset (Fin n)) (hS : S.Nonempty)
    (g : ℕ → G n) (hg : Tendsto g atTop (𝓝 1)) :
    ∃ s b : ℕ → G n, ∃ c : ℕ → ℝ,
      Tendsto s atTop (𝓝 1) ∧ Tendsto b atTop (𝓝 1) ∧
      (∀ k, s k = g k * b k) ∧ (∀ k, b k ∈ singleBlockRootGroup (↑S)) ∧
      (∀ k, 0 < c k) ∧
      ∀ᶠ k in atTop, (∀ i ∈ S, (s k).val i i = c k) ∧
        ∀ i ∈ S, ∀ j ∈ S, i ≠ j → (s k).val i j = 0 := by
…

    Mentions: OAI.DukePrimeDegree.singleBlockRootGroup