OAI/Dynamics/SmoothObstruction/Splitting.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SmoothObstruction.EuclideanSplitting.norm_le_sum_coordinates line 19
2. lemma OAI.SmoothObstruction.EuclideanSplitting.opNorm_le_entry line 27

   Source documentation

   Entry bounds produce Euclidean operator bounds. The dimension factor is paid only at endpoints, never once per step.

   lemma opNorm_le_entry (A : Matrix (Fin d) (Fin d) ℝ) {B : ℝ} (hB : 0 ≤ B)
       (hA : ∀ i j, |A i j| ≤ B) : ‖A‖ ≤ (d : ℝ)^2 * B := by
   …

3. lemma OAI.SmoothObstruction.EuclideanSplitting.opNorm_le_exp line 46
4. def OAI.SmoothObstruction.EuclideanSplitting.rate line 59
5. def OAI.SmoothObstruction.EuclideanSplitting.mask line 62
6. lemma OAI.SmoothObstruction.EuclideanSplitting.rate_zero line 65
7. lemma OAI.SmoothObstruction.EuclideanSplitting.rate_add line 67
8. lemma OAI.SmoothObstruction.EuclideanSplitting.rate_mask_comm line 73
9. lemma OAI.SmoothObstruction.EuclideanSplitting.mask_sq line 76
10. lemma OAI.SmoothObstruction.EuclideanSplitting.mask_compl_add line 79
11. lemma OAI.SmoothObstruction.EuclideanSplitting.mask_compl_mul line 83
12. lemma OAI.SmoothObstruction.EuclideanSplitting.norm_mask line 87
13. def OAI.SmoothObstruction.EuclideanSplitting.transition line 93

    Source documentation

    Gauge-coordinate fundamental matrix; both time directions are encoded.

    noncomputable def transition (U V : ℕ → Matrix (Fin d) (Fin d) ℝ)
        (lam : Fin d → ℝ) (s t : ℕ) : Matrix (Fin d) (Fin d) ℝ :=
    …

14. def OAI.SmoothObstruction.EuclideanSplitting.projection line 96
15. lemma OAI.SmoothObstruction.EuclideanSplitting.transition_self line 100
16. lemma OAI.SmoothObstruction.EuclideanSplitting.transition_comp line 103
17. lemma OAI.SmoothObstruction.EuclideanSplitting.transition_projection line 110
18. lemma OAI.SmoothObstruction.EuclideanSplitting.projection_idem line 122
19. lemma OAI.SmoothObstruction.EuclideanSplitting.projection_compl line 129
20. lemma OAI.SmoothObstruction.EuclideanSplitting.norm_projection line 134
21. lemma OAI.SmoothObstruction.EuclideanSplitting.norm_rate_mask line 144
22. lemma OAI.SmoothObstruction.EuclideanSplitting.norm_transition_projection line 158

    Source documentation

    Subinterval propagation on a selected group. The only conditioning loss is at the two endpoints.

    lemma norm_transition_projection (U V : ℕ → Matrix (Fin d) (Fin d) ℝ)
        (hVU : ∀ t, V t*U t=1) (lam : Fin d → ℝ) {K c : ℝ}
        (S : Finset (Fin d)) (s t : ℕ) (hst : s ≤ t)
        (hU : ‖U t‖ ≤ Real.exp K) (hV : ‖V s‖ ≤ Real.exp K)
        (hc : ∀ j ∈ S, lam j ≤ c) :
        ‖transition U V lam s t*projection U V S s‖ ≤
          Real.exp (c*((t:ℝ)-s)+2*K) := by
    …

    Mentions: OAI.SmoothObstruction.EuclideanSplitting.transition, OAI.SmoothObstruction.EuclideanSplitting.projection

23. theorem OAI.SmoothObstruction.EuclideanSplitting.exists_operator_gauge line 182

    Source documentation

    Conversion of the constructed finite triangular gauge to genuine Euclidean operator bounds. The constant is independent of the interval.

    theorem exists_operator_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, |NormalizedGauge.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, ‖U t‖ ≤ Real.exp (C*E)) ∧
            (∀ t ≤ N, ‖V t‖ ≤ Real.exp (C*E)) ∧
    …

    Mentions: OAI.SmoothObstruction.NormalizedGauge.error

24. def OAI.SmoothObstruction.EuclideanSplitting.propagator line 205

    Source documentation

    Actual later-on-the-left product used in the manuscript.

    def propagator (A : ℕ → Matrix (Fin d) (Fin d) ℝ) (s : ℕ) : ℕ → Matrix (Fin d) (Fin d) ℝ
      | 0 => 1
      | n+1 => A (s+n)*propagator A s n

25. lemma OAI.SmoothObstruction.EuclideanSplitting.transition_one_step line 209
26. lemma OAI.SmoothObstruction.EuclideanSplitting.propagator_eq_transition line 220
27. lemma OAI.SmoothObstruction.EuclideanSplitting.norm_rate_mask_lower line 232
28. lemma OAI.SmoothObstruction.EuclideanSplitting.norm_backward_projection line 244
29. def OAI.SmoothObstruction.QR.frameMatrix line 272
30. def OAI.SmoothObstruction.QR.frameInverse line 275
31. lemma OAI.SmoothObstruction.QR.frameMatrix_inverse line 278
32. lemma OAI.SmoothObstruction.QR.norm_frameMatrix line 288
33. lemma OAI.SmoothObstruction.QR.norm_frameInverse line 295
34. lemma OAI.SmoothObstruction.QR.triangular_bound line 302
35. lemma OAI.SmoothObstruction.QR.matrix_qr line 310
36. theorem OAI.SmoothObstruction.QR.transfer_gauge line 335

    Source documentation

    The actual QR frame change transfers a triangular finite gauge to the original derivative matrices, at no loss in operator norm.

    theorem transfer_gauge
        (A : ℕ → EuclideanSpace ℝ (Fin d) ≃L[ℝ] EuclideanSpace ℝ (Fin d))
        (e : ℕ → Frame d) (he : ∀ t,e (t+1)=step (A t) (e t))
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ) (N : ℕ) (K : ℝ)
        (hUV : ∀ t,U t*V t=1 ∧ V t*U t=1)
        (hU : ∀ t≤N,‖U t‖≤Real.exp K) (hV : ∀ t≤N,‖V t‖≤Real.exp K)
        (hEq : ∀ t<N,triangular (A t) (e t)*U t=U (t+1)*EuclideanSplitting.rate lam 1) :
        ∃ P Q : ℕ → Matrix (Fin d) (Fin d) ℝ,
          (∀ t,P t*Q t=1 ∧ Q t*P t=1) ∧
          (∀ t≤N,‖P t‖≤Real.exp K) ∧ (∀ t≤N,‖Q t‖≤Real.exp K) ∧
          (∀ t<N,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm (A t).toContinuousLinearMap*P t=
    …

    Mentions: OAI.SmoothObstruction.QR.Frame, OAI.SmoothObstruction.QR.step, OAI.SmoothObstruction.QR.triangular, OAI.SmoothObstruction.EuclideanSplitting.rate

37. lemma OAI.SmoothObstruction.QR.exists_uniform_qr_bound line 374

    Source documentation

    Compactness bounds both the actual derivative and every positive QR log-diagonal. The frame is arbitrary, so no measurable choice is hidden.

    lemma exists_uniform_qr_bound
        (A : X → EuclideanSpace ℝ (Fin d) ≃L[ℝ] EuclideanSpace ℝ (Fin d))
        (hA : Continuous (fun x => (A x).toContinuousLinearMap)) :
        ∃ R : ℝ, 0≤R ∧ (∀ x,‖(A x).toContinuousLinearMap‖≤Real.exp R) ∧
          ∀ (x : X) (e : Frame d) j, |Real.log (triangular (A x) e j j)|≤R := by
    …

    Mentions: OAI.SmoothObstruction.QR.Frame, OAI.SmoothObstruction.QR.triangular

38. lemma OAI.SmoothObstruction.QR.skew_iterate_fst line 401
39. lemma OAI.SmoothObstruction.QR.log_error_is_chord line 409
40. lemma OAI.SmoothObstruction.QR.average_abs_le line 421
41. theorem OAI.SmoothObstruction.QR.compact_good_gauge line 434

    Source documentation

    Finite gauges for genuine good QR orbit segments. Positivity and triangularity come from the actual Gram--Schmidt process, and the chord errors are identified with the stationary quantities, not assumed anew.

    theorem compact_good_gauge (T : X → X)
        (A : X → EuclideanSpace ℝ (Fin d) ≃L[ℝ] EuclideanSpace ℝ (Fin d))
        (hA : Continuous (fun x => (A x).toContinuousLinearMap)) :
        ∃ R C : ℝ,0≤R ∧ 0≤C ∧ ∀ k b (z : X × Frame d),
          z∈GoodStationary.Good (skew T A)
            (fun j w => Real.log (triangular (A w.1) w.2 j j)) k b →
          1≤b*(2:ℝ)^k → Real.log ((2^(k+1):ℕ)+1)≤b*(2:ℝ)^k →
          ∃ (lam : Fin d → ℝ) (P Q : ℕ → Matrix (Fin d) (Fin d) ℝ),
            (∀ j,|lam j|≤R) ∧ (∀ t,P t*Q t=1 ∧ Q t*P t=1) ∧
            (∀ t≤2^(k+1),‖P t‖≤Real.exp (C*(b*2^k))) ∧
            (∀ t≤2^(k+1),‖Q t‖≤Real.exp (C*(b*2^k))) ∧
            (∀ t<2^(k+1),
    …

    Mentions: OAI.SmoothObstruction.QR.Frame, OAI.SmoothObstruction.GoodStationary.Good, OAI.SmoothObstruction.QR.skew, OAI.SmoothObstruction.QR.triangular