OAI/Dynamics/SmoothObstruction/ShearGauge.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothObstruction.FiniteShears.forward line 16

   Source documentation

   The finite forward Green solution; no division by a spectral gap.

   noncomputable def forward (q : ℝ) (f : ℕ → ℝ) (t : ℕ) : ℝ :=
   …

2. lemma OAI.SmoothObstruction.FiniteShears.forward_zero line 19
3. lemma OAI.SmoothObstruction.FiniteShears.forward_succ line 22
4. lemma OAI.SmoothObstruction.FiniteShears.forward_bound line 33
5. def OAI.SmoothObstruction.FiniteShears.backward line 47

   Source documentation

   A terminal-value Green solution with coefficients at most one when q≥1.

   noncomputable def backward (N : ℕ) (q : ℝ) (f : ℕ → ℝ) (t : ℕ) : ℝ :=
   …

6. lemma OAI.SmoothObstruction.FiniteShears.backward_terminal line 50
7. lemma OAI.SmoothObstruction.FiniteShears.backward_succ line 53
8. lemma OAI.SmoothObstruction.FiniteShears.backward_bound line 63
9. theorem OAI.SmoothObstruction.FiniteShears.exists_bounded_recurrence line 85

   Source documentation

   The scalar input needed by every elementary shear in the finite triangular cocycle reduction. This includes q=1; it never divides by q−1.

   theorem exists_bounded_recurrence (N : ℕ) {q M : ℝ} (hq : 0 < q) (hM : 0 ≤ M)
       (f : ℕ → ℝ) (hf : ∀ t < N, |f t| ≤ M) :
       ∃ u : ℕ → ℝ, (∀ t < N, u (t + 1) = q * u t + f t) ∧
         (∀ t ≤ N, |u t| ≤ N * M) := by
   …

10. def OAI.SmoothObstruction.TriangularGauge.rowReplace line 105

    Source documentation

    Replace one row, retaining the other rows.

    def rowReplace (U : Matrix (Fin d) (Fin d) ℝ) (i : Fin d) (v : Fin d → ℝ) :
        Matrix (Fin d) (Fin d) ℝ := fun k j => if k = i then v j else U k j

11. lemma OAI.SmoothObstruction.TriangularGauge.mul_rowReplace_same line 108
12. lemma OAI.SmoothObstruction.TriangularGauge.mul_rowReplace_later line 123
13. lemma OAI.SmoothObstruction.TriangularGauge.forcing_zero line 134
14. lemma OAI.SmoothObstruction.TriangularGauge.forcing_bound line 143
15. theorem OAI.SmoothObstruction.TriangularGauge.exists_diagonal_gauge line 163

    Source documentation

    A full finite-time unitriangular diagonalizing gauge. In contrast to infinite-time reducibility, this assertion needs no separation of rates. All losses are fixed-degree polynomials in the length and entry bound.

    theorem exists_diagonal_gauge (N : ℕ) (A : ℕ → Matrix (Fin d) (Fin d) ℝ)
        (a : Fin d → ℝ) {H : ℝ} (hH : 1 ≤ H)
        (ha : ∀ j, 0 < a j) (hai : ∀ j, |(a j)⁻¹| ≤ H)
        (htri : ∀ t < N, (A t).IsUpperTriangular)
        (hdiag : ∀ t < N, ∀ j, A t j j = a j)
        (hbound : ∀ t < N, ∀ i j, |A t i j| ≤ H) :
        ∃ U : ℕ → Matrix (Fin d) (Fin d) ℝ,
          (∀ t, (U t).IsUpperTriangular ∧ ∀ j, U t j j = 1) ∧
          (∀ t ≤ N, ∀ i j, |U t i j| ≤ (1 + N * d * H ^ 2) ^ d) ∧
          (∀ t < N, A t * U t = U (t + 1) * Matrix.diagonal a) := by
    …

16. lemma OAI.SmoothObstruction.TriangularGauge.abs_det_le_entry_bound line 292

    Source documentation

    A deliberately coarse finite-dimensional determinant estimate.

    lemma abs_det_le_entry_bound (A : Matrix (Fin d) (Fin d) ℝ) {B : ℝ}
        (hA : ∀ i j, |A i j| ≤ B) :
        |A.det| ≤ (Nat.factorial d : ℝ) * B ^ d := by
    …

17. lemma OAI.SmoothObstruction.TriangularGauge.unitriangular_det line 313
18. lemma OAI.SmoothObstruction.TriangularGauge.unitriangular_inverse_bound line 318
19. theorem OAI.SmoothObstruction.TriangularGauge.exists_diagonal_gauge_invertible line 336

    Source documentation

    The gauge can be chosen with a polynomially bounded genuine inverse.

    theorem exists_diagonal_gauge_invertible (N : ℕ)
        (A : ℕ → Matrix (Fin d) (Fin d) ℝ) (a : Fin d → ℝ)
        {H : ℝ} (hH : 1 ≤ H) (ha : ∀ j, 0 < a j)
        (hai : ∀ j, |(a j)⁻¹| ≤ H)
        (htri : ∀ t < N, (A t).IsUpperTriangular)
        (hdiag : ∀ t < N, ∀ j, A t j j = a j)
        (hbound : ∀ t < N, ∀ i j, |A t i j| ≤ H) :
        ∃ U : ℕ → Matrix (Fin d) (Fin d) ℝ,
          (∀ t, U t * (U t)⁻¹ = 1 ∧ (U t)⁻¹ * U t = 1) ∧
          (∀ t ≤ N, ∀ i j, |U t i j| ≤ (1 + N * d * H ^ 2) ^ d) ∧
          (∀ t ≤ N, ∀ i j, |(U t)⁻¹ i j| ≤
            (Nat.factorial d : ℝ) * ((1 + N * d * H ^ 2) ^ d) ^ d) ∧
    …

20. def OAI.SmoothObstruction.NormalizedGauge.error line 368
21. lemma OAI.SmoothObstruction.NormalizedGauge.error_succ line 372
22. def OAI.SmoothObstruction.NormalizedGauge.normalized line 378
23. lemma OAI.SmoothObstruction.NormalizedGauge.normalized_tri line 382
24. lemma OAI.SmoothObstruction.NormalizedGauge.normalized_diag line 388
25. lemma OAI.SmoothObstruction.NormalizedGauge.normalized_bound line 397
26. theorem OAI.SmoothObstruction.NormalizedGauge.exists_normalized_gauge line 416

    Source documentation

    Diagonal chord normalization followed by a finite bounded shear gauge.

    theorem exists_normalized_gauge (N : ℕ) (A : ℕ → Matrix (Fin d) (Fin d) ℝ)
        (lam : Fin d → ℝ) {R E : ℝ} (hR : 0 ≤ R) (hE : 0 ≤ E)
        (htri : ∀ t < N, (A t).IsUpperTriangular)
        (hpos : ∀ t < N, ∀ j, 0 < A t j j)
        (hA : ∀ t < N, ∀ i j, |A t i j| ≤ Real.exp R)
        (hlam : ∀ j, |lam j| ≤ R)
        (he : ∀ t ≤ N, ∀ j, |error A lam t j| ≤ E) :
        ∃ C V : ℕ → Matrix (Fin d) (Fin d) ℝ,
          (∀ t, C t * V t = 1 ∧ V t * C t = 1) ∧
          (∀ t ≤ N, ∀ i j, |C t i j| ≤ Real.exp E *
            (1 + N * d * (Real.exp (R + 2 * E)) ^ 2) ^ d) ∧
          (∀ t ≤ N, ∀ i j, |V t i j| ≤ (Nat.factorial d : ℝ) *
    …

    Mentions: OAI.SmoothObstruction.NormalizedGauge.error

27. lemma OAI.SmoothObstruction.NormalizedGauge.gauge_polynomial_le_exp line 489
28. theorem OAI.SmoothObstruction.NormalizedGauge.exists_exponential_gauge line 523

    Source documentation

    Uniform exponential estimates with a constant depending only on d and R. This is the finite gauge estimate eq:finite-gauge before conversion of the entry norm to the Euclidean operator norm.

    theorem exists_exponential_gauge (d : ℕ) (R : ℝ) (hR : 0 ≤ R) :
        ∃ C : ℝ, 0 ≤ C ∧ ∀ (N : ℕ) (E : ℝ) (A : ℕ → Matrix (Fin d) (Fin d) ℝ)
          (lam : Fin d → ℝ), 1 ≤ E → Real.log (N + 1) ≤ E →
          (∀ t < N, (A t).IsUpperTriangular) →
          (∀ t < N, ∀ j, 0 < A t j j) →
          (∀ t < N, ∀ i j, |A t i j| ≤ Real.exp R) →
          (∀ j, |lam j| ≤ R) →
          (∀ t ≤ N, ∀ j, |error A lam t j| ≤ E) →
          ∃ U V : ℕ → Matrix (Fin d) (Fin d) ℝ,
            (∀ t, U t * V t = 1 ∧ V t * U t = 1) ∧
            (∀ t ≤ N, ∀ i j, |U t i j| ≤ Real.exp (C * E)) ∧
            (∀ t ≤ N, ∀ i j, |V t i j| ≤ Real.exp (C * E)) ∧
    …

    Mentions: OAI.SmoothObstruction.NormalizedGauge.error