OAI/Geometry/HarmonicGrowth/Flow.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.LinearODE.term line 17

   Source documentation

   The exact Peano--Baker iterates, with oriented integrals on the entire real line.

   def term (A : ℝ → E →L[ℝ] E) (x : E) : ℕ → ℝ → E
     | 0, _ => x
     | n+1, t => ∫ s in (0:ℝ)..t, A s (term A x n s)

2. lemma OAI.HarmonicCounterexample.LinearODE.term_continuous line 21
3. lemma OAI.HarmonicCounterexample.LinearODE.term_succ_hasDerivAt line 32
4. lemma OAI.HarmonicCounterexample.LinearODE.term_bound line 39
5. def OAI.HarmonicCounterexample.LinearODE.flow line 71
6. lemma OAI.HarmonicCounterexample.LinearODE.term_summable line 75
7. lemma OAI.HarmonicCounterexample.LinearODE.flow_eq line 83
8. lemma OAI.HarmonicCounterexample.LinearODE.term_zero line 89
9. lemma OAI.HarmonicCounterexample.LinearODE.flow_initial line 93
10. theorem OAI.HarmonicCounterexample.LinearODE.flow_hasDerivAt line 103

    Source documentation

    A global actual solution, before any positivity, transmission or growth estimates.

    theorem flow_hasDerivAt {A : ℝ → E →L[ℝ] E} (hA : Continuous A) {M : ℝ}
        (hM : 0 ≤ M) (hb : ∀ s, ‖A s‖ ≤ M) (x : E) (t : ℝ) :
        HasDerivAt (flow A x) (A t (flow A x t)) t := by
    …

    Mentions: OAI.HarmonicCounterexample.LinearODE.flow

11. lemma OAI.HarmonicCounterexample.LinearODE.flow_smooth line 137
12. lemma OAI.HarmonicCounterexample.LinearODE.solution_unique line 153
13. lemma OAI.HarmonicCounterexample.LinearODE.flow_injective line 161
14. lemma OAI.HarmonicCounterexample.LinearODE.flow_add line 170
15. lemma OAI.HarmonicCounterexample.LinearODE.flow_smul line 181
16. def OAI.HarmonicCounterexample.LinearODE.flowLinear line 192

    Source documentation

    Actual initial-data linearity, later used for independence of harmonic columns.

    def flowLinear (A : ℝ → E →L[ℝ] E) (hA : Continuous A) (M : ℝ)
        (hM : 0 ≤ M) (hb : ∀ s, ‖A s‖ ≤ M) (t : ℝ) : E →ₗ[ℝ] E where
    …

17. def OAI.HarmonicCounterexample.LinearODE.block line 213
18. lemma OAI.HarmonicCounterexample.LinearODE.block_apply line 217
19. lemma OAI.HarmonicCounterexample.LinearODE.block_eq line 220
20. lemma OAI.HarmonicCounterexample.LinearODE.block_continuous line 226
21. lemma OAI.HarmonicCounterexample.LinearODE.block_smooth line 232
22. lemma OAI.HarmonicCounterexample.LinearODE.block_bound line 238
23. def OAI.HarmonicCounterexample.LinearODE.phase line 258
24. def OAI.HarmonicCounterexample.LinearODE.value line 261
25. def OAI.HarmonicCounterexample.LinearODE.velocity line 264
26. lemma OAI.HarmonicCounterexample.LinearODE.value_initial line 267
27. lemma OAI.HarmonicCounterexample.LinearODE.velocity_initial line 270
28. lemma OAI.HarmonicCounterexample.LinearODE.value_deriv line 275
29. lemma OAI.HarmonicCounterexample.LinearODE.velocity_deriv line 284
30. lemma OAI.HarmonicCounterexample.LinearODE.value_smooth line 294
31. theorem OAI.HarmonicCounterexample.LinearODE.phase_euclidean_tail line 320

    Source documentation

    Exact matching to the regular Euclidean solution on the entire negative logarithmic half-line, obtained by uniqueness rather than an asymptotic ansatz.

    theorem phase_euclidean_tail {A : ℝ → E →L[ℝ] E} {b : ℝ → ℝ}
        (hA : Continuous A) (hb : Continuous b) {MA Mb : ℝ}
        (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hAn : ∀ t, ‖A t‖ ≤ MA) (hbn : ∀ t, |b t| ≤ Mb)
        {l B : ℝ} (hAi : ∀ t ≤ 0, ∀ v, A t v = (l*(l+B)) • v)
        (hbi : ∀ t ≤ 0, b t = B) (x : E) {t : ℝ} (ht : t ≤ 0) :
        phase A b l x t = Real.exp (l*t) • (x,l • x) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.phase

32. lemma OAI.HarmonicCounterexample.LinearODE.value_euclidean_tail line 355
33. def OAI.HarmonicCounterexample.LinearODE.integratingWeight line 378
34. lemma OAI.HarmonicCounterexample.LinearODE.integratingWeight_pos line 381
35. lemma OAI.HarmonicCounterexample.LinearODE.integratingWeight_initial line 384
36. lemma OAI.HarmonicCounterexample.LinearODE.integratingWeight_deriv line 387
37. lemma OAI.HarmonicCounterexample.LinearODE.weighted_energy_deriv line 396

    Source documentation

    Exact weighted energy identity; no invertibility of the value block is assumed.

    lemma weighted_energy_deriv {A : ℝ → E →L[ℝ] E} {b : ℝ → ℝ}
        (hb : Continuous b) {y z : ℝ → E} {t : ℝ}
        (hy : HasDerivAt y (z t) t)
        (hz : HasDerivAt z (A t (y t)-b t • z t) t) :
        HasDerivAt (fun t => integratingWeight b t * ⟪y t,z t⟫_ℝ)
          (integratingWeight b t*(⟪y t,A t (y t)⟫_ℝ+‖z t‖^2)) t := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.integratingWeight

38. lemma OAI.HarmonicCounterexample.LinearODE.weighted_energy_monotone line 406
39. lemma OAI.HarmonicCounterexample.LinearODE.regular_pairing_positive line 416

    Source documentation

    Center-regular initial data have a strictly positive pairing for all t≥0. This rules out conjugate zeros and produces the value-block injectivity.

    lemma regular_pairing_positive {A : ℝ → E →L[ℝ] E} {b : ℝ → ℝ}
        (hb : Continuous b) (hAp : ∀ t v, 0 ≤ ⟪v,A t v⟫_ℝ) {y z : ℝ → E}
        (hy : ∀ t, HasDerivAt y (z t) t)
        (hz : ∀ t, HasDerivAt z (A t (y t)-b t • z t) t)
        {l : ℝ} (hl : 0 < l) (hinit : z 0 = l • y 0) (hne : y 0 ≠ 0)
        {t : ℝ} (ht : 0 ≤ t) : 0 < ⟪y t,z t⟫_ℝ := by
    …

    Mentions: OAI.HarmonicCounterexample.b

40. lemma OAI.HarmonicCounterexample.LinearODE.value_nonzero_of_nonnegative line 431
41. lemma OAI.HarmonicCounterexample.LinearODE.value_linear line 446
42. lemma OAI.HarmonicCounterexample.LinearODE.value_injective_of_nonnegative line 465
43. lemma OAI.HarmonicCounterexample.LinearODE.weighted_wronskian_deriv line 495

    Source documentation

    Symplectic flux cancellation for two actual center-regular solutions.

    lemma weighted_wronskian_deriv {A : ℝ → E →L[ℝ] E} {b : ℝ → ℝ}
        (hb : Continuous b) {u v p q : ℝ → E} {t : ℝ}
        (hA : ∀ x y, ⟪A t x,y⟫_ℝ = ⟪x,A t y⟫_ℝ)
        (hu : HasDerivAt u (v t) t) (hv : HasDerivAt v (A t (u t)-b t • v t) t)
        (hp : HasDerivAt p (q t) t) (hq : HasDerivAt q (A t (p t)-b t • q t) t) :
        HasDerivAt (fun t => integratingWeight b t*(⟪u t,q t⟫_ℝ-⟪v t,p t⟫_ℝ)) 0 t := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.integratingWeight

44. lemma OAI.HarmonicCounterexample.LinearODE.weighted_wronskian_constant line 505
45. lemma OAI.HarmonicCounterexample.LinearODE.regular_wronskian_zero line 521
46. def OAI.HarmonicCounterexample.LinearODE.leftAction line 550

    Source documentation

    Left composition lifts a bounded coefficient to the Banach space of operators.

    def leftAction (A : ℝ → E →L[ℝ] E) (t : ℝ) : (E →L[ℝ] E) →L[ℝ] (E →L[ℝ] E) :=
    …

47. lemma OAI.HarmonicCounterexample.LinearODE.leftAction_continuous line 553
48. lemma OAI.HarmonicCounterexample.LinearODE.leftAction_smooth line 556
49. lemma OAI.HarmonicCounterexample.LinearODE.leftAction_norm_le line 559
50. def OAI.HarmonicCounterexample.LinearODE.operatorValue line 565
51. def OAI.HarmonicCounterexample.LinearODE.operatorVelocity line 568
52. lemma OAI.HarmonicCounterexample.LinearODE.operatorValue_deriv line 571
53. lemma OAI.HarmonicCounterexample.LinearODE.operatorVelocity_deriv line 579
54. lemma OAI.HarmonicCounterexample.LinearODE.operatorValue_smooth line 588
55. lemma OAI.HarmonicCounterexample.LinearODE.operatorValue_apply_deriv line 596
56. lemma OAI.HarmonicCounterexample.LinearODE.operatorVelocity_apply_deriv line 604
57. lemma OAI.HarmonicCounterexample.LinearODE.operatorPhase_deriv line 613
58. lemma OAI.HarmonicCounterexample.LinearODE.operatorPhase_initial line 623
59. lemma OAI.HarmonicCounterexample.LinearODE.operatorPhase_apply line 628
60. lemma OAI.HarmonicCounterexample.LinearODE.operatorValue_apply line 644
61. lemma OAI.HarmonicCounterexample.LinearODE.operatorVelocity_apply line 651
62. def OAI.HarmonicCounterexample.LinearODE.slope line 675

    Source documentation

    The logarithmic derivative of the actual center-regular value operator.

    def slope (A : ℝ → E →L[ℝ] E) (b : ℝ → ℝ) (l t : ℝ) : E →L[ℝ] E :=
    …

    Mentions: OAI.HarmonicCounterexample.b

63. lemma OAI.HarmonicCounterexample.LinearODE.operatorValue_isUnit line 678
64. lemma OAI.HarmonicCounterexample.LinearODE.slope_value line 693
65. lemma OAI.HarmonicCounterexample.LinearODE.slope_initial line 701
66. lemma OAI.HarmonicCounterexample.LinearODE.slope_symmetric line 707
67. lemma OAI.HarmonicCounterexample.LinearODE.slope_nonnegative line 723
68. lemma OAI.HarmonicCounterexample.LinearODE.clm_inverse_deriv line 744
69. lemma OAI.HarmonicCounterexample.LinearODE.slope_deriv line 756
70. lemma OAI.HarmonicCounterexample.LinearODE.integrating_factor_nonnegative line 790

    Source documentation

    A genuine integrating-factor comparison on the half-line.

    lemma integrating_factor_nonnegative (p f f' : ℝ → ℝ) (hp : Continuous p)
        (hf : ∀ t,HasDerivAt f (f' t) t) (h0 : 0 ≤ f 0)
        (hineq : ∀ t,0 ≤ t → 0 ≤ f' t+p t*f t) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ f t := by
    …

71. lemma OAI.HarmonicCounterexample.LinearODE.solution_energy_lower line 817

    Source documentation

    Energy comparison proves the lower Riccati barrier directly for actual second-order solutions, without presupposing a global Riccati solution.

    lemma solution_energy_lower (A : ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (y v : ℝ → E) (hb : Continuous b) (hy : ∀ t,HasDerivAt y (v t) t)
        (hv : ∀ t,HasDerivAt v (A t (y t)-b t • v t) t) (c : ℝ)
        (h0 : c*⟪y 0,y 0⟫ ≤ ⟪y 0,v 0⟫)
        (hA : ∀ t,0 ≤ t → ∀ z, (b t*c+c^2)*⟪z,z⟫ ≤ ⟪z,A t z⟫)
        {t : ℝ} (ht : 0 ≤ t) : c*⟪y t,y t⟫ ≤ ⟪y t,v t⟫ := by
    …

    Mentions: OAI.HarmonicCounterexample.b

72. lemma OAI.HarmonicCounterexample.LinearODE.solution_norm_lower line 840

    Source documentation

    Value vectors cannot vanish: the center-regular norm is nondecreasing.

    lemma solution_norm_lower (A : ℝ → E →L[ℝ] E) (b : ℝ → ℝ)
        (y v : ℝ → E) (hb : Continuous b) (hy : ∀ t,HasDerivAt y (v t) t)
        (hv : ∀ t,HasDerivAt v (A t (y t)-b t • v t) t)
        (h0 : 0 ≤ ⟪y 0,v 0⟫)
        (hA : ∀ t,0 ≤ t → ∀ z,0 ≤ ⟪z,A t z⟫)
        {t : ℝ} (ht : 0 ≤ t) : ‖y 0‖ ≤ ‖y t‖ := by
    …

    Mentions: OAI.HarmonicCounterexample.b

73. theorem OAI.HarmonicCounterexample.LinearODE.value_norm_lower line 864

    Source documentation

    Actual center-regular value flow is norm-expanding for all nonnegative times.

    theorem value_norm_lower {A : ℝ → E →L[ℝ] E} {b : ℝ → ℝ}
        (hA : Continuous A) (hb : Continuous b) {MA Mb : ℝ}
        (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hAn : ∀ t,‖A t‖ ≤ MA) (hbn : ∀ t,|b t| ≤ Mb)
        {l : ℝ} (hl : 0 ≤ l) (hpos : ∀ t,0 ≤ t → ∀ z,0 ≤ ⟪z,A t z⟫)
        (x : E) {t : ℝ} (ht : 0 ≤ t) : ‖x‖ ≤ ‖value A b l x t‖ := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.value

74. theorem OAI.HarmonicCounterexample.LinearODE.slope_quadratic_lower line 896

    Source documentation

    Uniform strictly positive lower barrier for the already constructed ACTUAL center-regular global Riccati slope. No Riccati existence is an assumption.

    theorem slope_quadratic_lower {A : ℝ → E →L[ℝ] E} {b : ℝ → ℝ}
        (hA : Continuous A) (hb : Continuous b) {MA Mb : ℝ}
        (hMA : 0 ≤ MA) (hMb : 0 ≤ Mb)
        (hAn : ∀ t,‖A t‖ ≤ MA) (hbn : ∀ t,|b t| ≤ Mb)
        {l c t : ℝ} (hc : c ≤ l) (ht : 0 ≤ t)
        (hpos : ∀ s,0 ≤ s → ∀ z,(b s*c+c^2)*(inner ℝ z z) ≤ (inner ℝ z (A s z)))
        (hV : IsUnit (operatorValue A b l t)) (x : E) :
        c*‖x‖^2 ≤ (inner ℝ x (slope A b l t x)) := by
    …

    Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.LinearODE.operatorValue, OAI.HarmonicCounterexample.LinearODE.slope