RadialFutureLifts.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exponentially shrinking radial cells give triangular future lifts

lemma OAI.DukePrimeDegree.LocalInjectivityAt.injOn line 14

theorem OAI.DukePrimeDegree.exists_radial_radius_small_conjugate_lifts line 22

Source documentation

The chosen lift remains in the height-dependent small matrix ball at every future time; the same radius is an injectivity radius at each point.

theorem exists_radial_radius_small_conjugate_lifts {n : ℕ} (hn : 0 < n)
    (ell : Fin n → ℝ) (hell : ∑ i, ell i=0)
    (B : ℝ) (hB : 0 < B) (H : X n → ℕ)
    (hheight : ∀ x, quotientLogDistance (Quotient.mk _ (1 : G n)) x ≤
      2*B*(H x:ℝ)+B) (R : ℝ) (hR : 0 < R) :
    ∃ r₀ : ℝ, 0 < r₀ ∧ r₀ ≤ 1 ∧ r₀ ≤ R ∧
      (∀ x, Set.InjOn (fun g => rightAction x g)
        (matrixBall n (r₀*Real.exp (-(4*B)*(H x:ℝ))))) ∧
      ∀ (Q : X n → ℕ),
      (∀ x y, Q y=Q x →
        ∃ g ∈ matrixBall n (r₀*Real.exp (-(4*B)*(H x:ℝ))), rightAction x g=y) →
      ∀ x y, (∀ k : ℕ,
…

Mentions: OAI.DukePrimeDegree.quotientLogDistance

theorem OAI.DukePrimeDegree.exists_radial_radius_small_triangular_lifts line 138

Source documentation

Future fibers admit small triangular lifts.

theorem exists_radial_radius_small_triangular_lifts {n : ℕ} (hn : 0 < n)
    (ell : Fin n → ℝ) (hell : ∑ i, ell i=0)
    (B : ℝ) (hB : 0 < B) (H : X n → ℕ)
    (hheight : ∀ x, quotientLogDistance (Quotient.mk _ (1 : G n)) x ≤
      2*B*(H x:ℝ)+B) (R : ℝ) (hR : 0 < R) :
    ∃ r₀ : ℝ, 0 < r₀ ∧ r₀ ≤ 1 ∧ r₀ ≤ R ∧
      ∀ (Q : X n → ℕ),
      (∀ x y, Q y=Q x →
        ∃ g ∈ matrixBall n (r₀*Real.exp (-(4*B)*(H x:ℝ))), rightAction x g=y) →
      ∀ x y, (∀ k : ℕ,
        Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k] y) =
        Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k] x)) →
…

Mentions: OAI.DukePrimeDegree.quotientLogDistance

theorem OAI.DukePrimeDegree.exists_radial_radius_triangular_lifts line 161

Source documentation

Future fibers admit triangular lifts.

theorem exists_radial_radius_triangular_lifts {n : ℕ} (hn : 0 < n)
    (ell : Fin n → ℝ) (hell : ∑ i, ell i=0)
    (B : ℝ) (hB : 0 < B) (H : X n → ℕ)
    (hheight : ∀ x, quotientLogDistance (Quotient.mk _ (1 : G n)) x ≤
      2*B*(H x:ℝ)+B) :
    ∃ r₀ : ℝ, 0 < r₀ ∧ r₀ ≤ 1 ∧
      ∀ (Q : X n → ℕ),
      (∀ x y, Q y=Q x →
        ∃ g ∈ matrixBall n (r₀*Real.exp (-(4*B)*(H x:ℝ))), rightAction x g=y) →
      ∀ x y, (∀ k : ℕ,
        Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k] y) =
        Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k] x)) →
…

Mentions: OAI.DukePrimeDegree.quotientLogDistance