OAI/Geometry/HarmonicGrowth/Growth.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HarmonicCounterexample.LinearODE.actual_scalar_baseline_integrated line 14

   Source documentation

   Exact integrated scalar damping for the genuine positive diagonal-leg solution, allowing its incoming logarithmic derivative to differ from the limiting dwell root. This retains the finite initial-discrepancy cost.

   theorem actual_scalar_baseline_integrated {A p : ℝ → ℝ}
       (hA : Continuous A) (hp : Continuous p)
       {MA Mp : ℝ} (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
       (hAn : ∀ t,|A t| ≤ MA) (hpn : ∀ t,|p t| ≤ Mp)
       (hAp : ∀ t,0 ≤ t → 0 ≤ A t) {θ d γ M T : ℝ}
       (hθ : 0 ≤ θ) (hd : 0 ≤ d) (hγ : 0 < γ) (hT : 0 ≤ T)
       (hpl : ∀ t ∈ Icc 0 T,γ ≤ p t)
       (hF : ∀ t ∈ Icc 0 T,|A t-p t*d-d^2| ≤ M) :
       (∫ t in (0:ℝ)..T,|scalarBaseline A p θ t-d|) ≤ (|θ-d|+M*T)/γ := by
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.scalarBaseline

2. lemma OAI.HarmonicCounterexample.LinearODE.actual_scalar_log_value line 54

   Source documentation

   The logarithm of the ACTUAL positive scalar value is the integral of its actual baseline. This is the bridge from Riccati estimates to diagonal growth.

   lemma actual_scalar_log_value {A p : ℝ → ℝ}
       (hA : Continuous A) (hp : Continuous p)
       {MA Mp : ℝ} (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
       (hAn : ∀ t,|A t| ≤ MA) (hpn : ∀ t,|p t| ≤ Mp)
       (hAp : ∀ t,0 ≤ t → 0 ≤ A t) {θ T : ℝ}
       (hθ : 0 ≤ θ) (hT : 0 ≤ T) :
       Real.log (scalarPhase A p 1 θ T).1=∫ t in (0:ℝ)..T,scalarBaseline A p θ t := by
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.scalarPhase, OAI.HarmonicCounterexample.LinearODE.scalarBaseline

3. theorem OAI.HarmonicCounterexample.LinearODE.actual_scalar_diagonal_growth line 75

   Source documentation

   Genuine logarithmic growth of the diagonal multiplier. Unlike an unproved asymptotic symbol this bound holds for every finite dwell length.

   theorem actual_scalar_diagonal_growth {A p : ℝ → ℝ}
       (hA : Continuous A) (hp : Continuous p)
       {MA Mp : ℝ} (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
       (hAn : ∀ t,|A t| ≤ MA) (hpn : ∀ t,|p t| ≤ Mp)
       (hAp : ∀ t,0 ≤ t → 0 ≤ A t) {θ d γ M T : ℝ}
       (hθ : 0 ≤ θ) (hd : 0 ≤ d) (hγ : 0 < γ) (hT : 0 ≤ T)
       (hpl : ∀ t ∈ Icc 0 T,γ ≤ p t)
       (hF : ∀ t ∈ Icc 0 T,|A t-p t*d-d^2| ≤ M) :
       |Real.log (scalarU A p T+θ*scalarV A p T)-d*T| ≤ (|θ-d|+M*T)/γ := by
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.scalarU, OAI.HarmonicCounterexample.LinearODE.scalarV

4. theorem OAI.HarmonicCounterexample.LinearODE.actual_scalar_variable_integrated line 110

   Source documentation

   Integrated damping with the actual time-dependent forcing. Rise/fall costs need not be artificially small; only their relative duration matters.

   theorem actual_scalar_variable_integrated {A p : ℝ → ℝ}
       (hA : Continuous A) (hp : Continuous p)
       {MA Mp : ℝ} (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
       (hAn : ∀ t,|A t| ≤ MA) (hpn : ∀ t,|p t| ≤ Mp)
       (hAp : ∀ t,0 ≤ t → 0 ≤ A t) {θ d γ T : ℝ}
       (hθ : 0 ≤ θ) (hd : 0 ≤ d) (hγ : 0 < γ) (hT : 0 ≤ T)
       (hpl : ∀ t ∈ Icc 0 T,γ ≤ p t) :
       (∫ t in (0:ℝ)..T,|scalarBaseline A p θ t-d|) ≤
         (|θ-d|+∫ t in (0:ℝ)..T,|A t-p t*d-d^2|)/γ := by
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.scalarBaseline

5. theorem OAI.HarmonicCounterexample.LinearODE.actual_scalar_variable_growth line 148

   Source documentation

   Finite complete-leg logarithmic error, with its exact forcing integral.

   theorem actual_scalar_variable_growth {A p : ℝ → ℝ}
       (hA : Continuous A) (hp : Continuous p)
       {MA Mp : ℝ} (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
       (hAn : ∀ t,|A t| ≤ MA) (hpn : ∀ t,|p t| ≤ Mp)
       (hAp : ∀ t,0 ≤ t → 0 ≤ A t) {θ d γ T : ℝ}
       (hθ : 0 ≤ θ) (hd : 0 ≤ d) (hγ : 0 < γ) (hT : 0 ≤ T)
       (hpl : ∀ t ∈ Icc 0 T,γ ≤ p t) :
       |Real.log (scalarU A p T+θ*scalarV A p T)-d*T| ≤
         (|θ-d|+∫ t in (0:ℝ)..T,|A t-p t*d-d^2|)/γ := by
   …

   Mentions: OAI.HarmonicCounterexample.LinearODE.scalarU, OAI.HarmonicCounterexample.LinearODE.scalarV

6. lemma OAI.HarmonicCounterexample.LinearODE.integral_three_piece_bound line 181

   Source documentation

   Complete-leg forcing estimate. The two short transition/rest pieces cost only their true total duration; the long dwell uses its separate small bound.

   lemma integral_three_piece_bound {f : ℝ → ℝ} (hf : Continuous f)
       {T L C ε : ℝ} (hT : 0 ≤ T) (hL : 0 ≤ L)
       (hbound : ∀ t ∈ Icc 0 (3*T+L),f t ≤ C)
       (hsmall : ∀ t ∈ Icc T (T+L),f t ≤ ε) :
       (∫ t in (0:ℝ)..3*T+L,f t) ≤ 3*C*T+ε*L := by
   …

7. theorem OAI.HarmonicCounterexample.LinearODE.scalar_complete_leg_limit line 203

   Source documentation

   True scalar U+theta V has the dwell-normalized root exponent whenever only the DWELL forcing tends to zero and the actual transition fraction does. No uniform smallness on the short rise/fall/rest portions is asserted.

   theorem scalar_complete_leg_limit (A p : ℕ → ℝ → ℝ) (T L : ℕ → ℝ)
       {θ d γ MA Mp C : ℝ}
       (hA : ∀ j,Continuous (A j)) (hp : ∀ j,Continuous (p j))
       (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
       (hAn : ∀ j t,|A j t| ≤ MA) (hpn : ∀ j t,|p j t| ≤ Mp)
       (hAp : ∀ j t,0 ≤ t → 0 ≤ A j t)
       (hθ : 0 ≤ θ) (hd : 0 ≤ d) (hγ : 0 < γ)
       (hT : ∀ j,0 ≤ T j) (hL : ∀ j,0 < L j)
       (hLtop : Tendsto L atTop atTop)
       (hratio : Tendsto (fun j => T j/L j) atTop (𝓝 0))
       (hpl : ∀ᶠ j in atTop,∀ t ∈ Icc 0 (3*T j+L j),γ ≤ p j t)
       (hbound : ∀ j,∀ t ∈ Icc 0 (3*T j+L j),|A j t-p j t*d-d^2| ≤ C)
   …

8. lemma OAI.HarmonicCounterexample.Schedule.dwell_atTop_limit line 266
9. lemma OAI.HarmonicCounterexample.Schedule.pulse_dwell_limit line 270
10. lemma OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.legLambda_dwell line 297
11. theorem OAI.HarmonicCounterexample.LinearODE.HistoryGeometry.leg_root_limit line 309

    Source documentation

    Exact root exponent of every true complete-leg diagonal entry. The pulse, ramp, fall and final round rest are not discarded in the solution definition.

    theorem HistoryGeometry.leg_root_limit (slot : Fin n → κ) (d₀ : ∀ b,ι b → ℝ)
        (hd₀ : ∀ b,orthogonalMatrix (S.basis b) (G.D₀ b)=Matrix.diagonal (d₀ b))
        (j0 : ℕ) (b : ξ) (i : ι b) {d : ℝ} (hd : 0 ≤ d)
        (hroot : d^2+S.p₀*d=S.β b*(G.qstar^S.r*S.B b+
            (G.qstar^S.r-G.qstar^(S.r-1))*d₀ b i)) :
        Tendsto (fun j => Real.log ((G.legU d₀ j0 j b+S.θ b • G.legV d₀ j0 j b) i i)/dwell j)
          atTop (𝓝 d) := by
    …

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

12. def OAI.HarmonicCounterexample.Construction.Stream.legMatrix line 375
13. def OAI.HarmonicCounterexample.Construction.Stream.legDiagonal line 379
14. lemma OAI.HarmonicCounterexample.Construction.Stream.leg_diagonal line 381
15. lemma OAI.HarmonicCounterexample.Construction.Stream.leg_positive line 389
16. lemma OAI.HarmonicCounterexample.Construction.Stream.leg_limit line 395
17. def OAI.HarmonicCounterexample.Construction.Stream.slip line 403
18. lemma OAI.HarmonicCounterexample.Construction.Stream.slip_bounds line 406
19. def OAI.HarmonicCounterexample.Construction.Stream.factor line 412
20. lemma OAI.HarmonicCounterexample.Construction.Stream.factor_positive line 415
21. lemma OAI.HarmonicCounterexample.Construction.Stream.period_factor line 418
22. lemma OAI.HarmonicCounterexample.Construction.Stream.baseline_cost line 425
23. lemma OAI.HarmonicCounterexample.Construction.Stream.factor_log_bound line 460
24. abbrev OAI.HarmonicCounterexample.Construction.SelectedIndex line 480
25. def OAI.HarmonicCounterexample.Construction.selectionEquiv line 482
26. def OAI.HarmonicCounterexample.Construction.selectedIndex line 485
27. lemma OAI.HarmonicCounterexample.Construction.selectedIndex_injective line 487
28. def OAI.HarmonicCounterexample.Construction.cyclePermutation line 490
29. lemma OAI.HarmonicCounterexample.Construction.cyclePermutation_apply line 494
30. def OAI.HarmonicCounterexample.Construction.cycleTarget line 499
31. def OAI.HarmonicCounterexample.Construction.constructedStream line 502
32. def OAI.HarmonicCounterexample.Construction.selectedBasis line 504
33. lemma OAI.HarmonicCounterexample.Construction.selectedBasis_norm line 505
34. lemma OAI.HarmonicCounterexample.Construction.selectedBasis_independent line 507
35. def OAI.HarmonicCounterexample.Construction.meanRoot line 510
36. lemma OAI.HarmonicCounterexample.Construction.selectedRoot_sum line 512
37. lemma OAI.HarmonicCounterexample.Construction.meanRoot_pos line 520
38. lemma OAI.HarmonicCounterexample.Construction.meanRoot_lt line 525
39. def OAI.HarmonicCounterexample.Construction.Stream.virtualTransfer line 533
40. lemma OAI.HarmonicCounterexample.Construction.Stream.virtualTransfer_action line 536
41. lemma OAI.HarmonicCounterexample.Construction.Stream.virtualTransfer_injective line 544
42. lemma OAI.HarmonicCounterexample.Construction.Stream.virtualTransfer_matrix line 547
43. lemma OAI.HarmonicCounterexample.Construction.Stream.virtualOrbit_rate line 553
44. lemma OAI.HarmonicCounterexample.GlobalGrowth.ode_local_log_bound line 592
45. theorem OAI.HarmonicCounterexample.GlobalGrowth.ode_all_time_log_growth line 617

    Source documentation

    Actual bounded Riccati ODEs have the source's all-real-time logarithmic bound. No local log-growth estimate is supplied as an extra assumption.

    theorem ode_all_time_log_growth {Y : ℝ → E} {P : ℝ → E →L[ℝ] E}
        {τ : ℕ → ℝ} {d α C : ℝ}
        (hτ : Tendsto τ atTop atTop) (hτpos : ∀ j,0 < τ j)
        (hend : Tendsto (fun j => Real.log ‖Y (τ j)‖/τ j) atTop (𝓝 d))
        (hduration : Tendsto (fun j => (τ (j+1)-τ j)/τ j) atTop (𝓝 0))
        (hC : 0 ≤ C) (hY : ∀ t,HasDerivAt Y (P t (Y t)) t)
        (hP : ∀ᶠ t in atTop,‖P t‖ ≤ C) (hnz : ∀ t,Y t ≠ 0)
        (hd : 0 ≤ d) (hα : d < α) :
        ∀ᶠ t in atTop,Real.log ‖Y t‖ ≤ α*t := by
    …

46. theorem OAI.HarmonicCounterexample.GlobalGrowth.ode_radial_growth line 635

    Source documentation

    A polynomial bound at EVERY sufficiently large radius, derived from the actual ODE and the endpoint limit.

    theorem ode_radial_growth {Y : ℝ → E} {P : ℝ → E →L[ℝ] E}
        {τ : ℕ → ℝ} {d α C : ℝ}
        (hτ : Tendsto τ atTop atTop) (hτpos : ∀ j,0 < τ j)
        (hend : Tendsto (fun j => Real.log ‖Y (τ j)‖/τ j) atTop (𝓝 d))
        (hduration : Tendsto (fun j => (τ (j+1)-τ j)/τ j) atTop (𝓝 0))
        (hC : 0 ≤ C) (hY : ∀ t,HasDerivAt Y (P t (Y t)) t)
        (hP : ∀ᶠ t in atTop,‖P t‖ ≤ C) (hnz : ∀ t,Y t ≠ 0)
        (hd : 0 ≤ d) (hα : d < α) :
        ∀ᶠ r in atTop,‖Y (Real.log r)‖ ≤ r^α :=
    …

47. def OAI.HarmonicCounterexample.LinearODE.regularAt line 663

    Source documentation

    Select the actual center-regular solution by its value at a positive late sphere. No arbitrary two-sided ODE solution is introduced.

    def regularAt (A : ℝ → E →L[ℝ] E) (p : ℝ → ℝ) (l a : ℝ) (x : E) (t : ℝ) : E :=
    …

    Mentions: OAI.HarmonicCounterexample.a

48. lemma OAI.HarmonicCounterexample.LinearODE.regularAt_initial line 667
49. theorem OAI.HarmonicCounterexample.LinearODE.actual_regular_radial_growth line 675

    Source documentation

    True smooth coefficient solutions with an endpoint rate satisfy power bounds at ALL sufficiently large radii. The uniform Riccati bound and all-time nonvanishing are produced from the angular coefficients and Euclidean core.

    theorem actual_regular_radial_growth {A : ℝ → E →L[ℝ] E} {p : ℝ → ℝ}
        (hA : Continuous A) (hp : Continuous p) {MA Mp : ℝ}
        (hMA : 0 ≤ MA) (hMp : 0 ≤ Mp)
        (hAn : ∀ t,‖A t‖ ≤ MA) (hpn : ∀ t,|p t| ≤ Mp)
        (hAs : ∀ t x y,inner ℝ (A t x) y=inner ℝ x (A t y))
        (hAp : ∀ t x,0 ≤ inner ℝ x (A t x))
        {l B a : ℝ} (hl : 0 < l) (hAc : ∀ t ≤ 0,∀ x,A t x=(l*(l+B)) • x)
        (hpc : ∀ t ≤ 0,p t=B) {x : E} (hx : x ≠ 0)
        {τ : ℕ → ℝ} {d α : ℝ} (hτ : Tendsto τ atTop atTop) (hτp : ∀ j,0 < τ j)
        (hend : Tendsto (fun j => Real.log ‖regularAt A p l a x (τ j)‖/τ j) atTop (𝓝 d))
        (hdur : Tendsto (fun j => (τ (j+1)-τ j)/τ j) atTop (𝓝 0))
        (hd : 0 ≤ d) (hα : d < α) :
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.LinearODE.regularAt

50. def OAI.HarmonicCounterexample.Construction.Stream.A line 728
51. def OAI.HarmonicCounterexample.Construction.Stream.bound line 729
52. lemma OAI.HarmonicCounterexample.Construction.Stream.bound_nonneg line 731
53. lemma OAI.HarmonicCounterexample.Construction.Stream.A_smooth line 732
54. lemma OAI.HarmonicCounterexample.Construction.Stream.A_bound line 734
55. lemma OAI.HarmonicCounterexample.Construction.Stream.A_nonnegative line 736
56. lemma OAI.HarmonicCounterexample.Construction.Stream.A_symmetric line 738
57. lemma OAI.HarmonicCounterexample.Construction.Stream.A_center line 741
58. lemma OAI.HarmonicCounterexample.Construction.Stream.A_eq line 744
59. lemma OAI.HarmonicCounterexample.Construction.Stream.value_unit line 747
60. lemma OAI.HarmonicCounterexample.Construction.Stream.degree_cast line 752
61. lemma OAI.HarmonicCounterexample.Construction.Stream.angular_smooth line 754
62. lemma OAI.HarmonicCounterexample.Construction.Stream.angular_bound line 757
63. def OAI.HarmonicCounterexample.Construction.Stream.orbitOperator line 776
64. lemma OAI.HarmonicCounterexample.Construction.Stream.orbitOperator_apply line 778
65. lemma OAI.HarmonicCounterexample.Construction.Stream.orbitOperator_injective line 781
66. def OAI.HarmonicCounterexample.Construction.Stream.initialOperator line 786
67. lemma OAI.HarmonicCounterexample.Construction.Stream.initialOperator_injective line 788
68. def OAI.HarmonicCounterexample.Construction.Stream.initialPolynomial line 792
69. lemma OAI.HarmonicCounterexample.Construction.Stream.initialPolynomial_independent line 793
70. lemma OAI.HarmonicCounterexample.Construction.Stream.initialPolynomial_eq line 796
71. def OAI.HarmonicCounterexample.Construction.Stream.trajectory line 802
72. lemma OAI.HarmonicCounterexample.Construction.Stream.virtualTransfer_actual line 805
73. lemma OAI.HarmonicCounterexample.Construction.Stream.trajectory_initial line 812
74. lemma OAI.HarmonicCounterexample.Construction.Stream.trajectory_step line 819
75. lemma OAI.HarmonicCounterexample.Construction.Stream.trajectory_samples line 828
76. lemma OAI.HarmonicCounterexample.Construction.Stream.trajectory_rate line 836
77. lemma OAI.HarmonicCounterexample.Construction.Stream.orbit_nonzero line 842
78. lemma OAI.HarmonicCounterexample.Construction.Stream.trajectory_regularAt line 852
79. lemma OAI.HarmonicCounterexample.Construction.Stream.trajectory_radial_growth line 859
80. lemma OAI.HarmonicCounterexample.Construction.Stream.trajectory_exp_growth line 872