OAI/Geometry/HarmonicGrowth/Profiles.lean

GitHub source file

153 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicCounterexample.Scale.cutoff line 21

   Source documentation

   The fixed cutoff is independent of all pulse data. It is zero already on (-infty,5/2] and one on [7/2,infty), as allowed by geometry.tex.

   def cutoff (t : ℝ) : ℝ := Real.smoothTransition (t - 5/2)

2. def OAI.HarmonicCounterexample.Scale.weight line 23
3. def OAI.HarmonicCounterexample.Scale.primitive line 25
4. def OAI.HarmonicCounterexample.Scale.total line 27
5. def OAI.HarmonicCounterexample.Scale.profile line 29
6. def OAI.HarmonicCounterexample.Scale.slope line 31
7. lemma OAI.HarmonicCounterexample.Scale.cutoff_smooth line 33
8. lemma OAI.HarmonicCounterexample.Scale.cutoff_zero line 36
9. lemma OAI.HarmonicCounterexample.Scale.cutoff_one line 39
10. lemma OAI.HarmonicCounterexample.Scale.cutoff_nonneg line 42
11. lemma OAI.HarmonicCounterexample.Scale.cutoff_le_one line 43
12. lemma OAI.HarmonicCounterexample.Scale.cutoff_mono line 44
13. lemma OAI.HarmonicCounterexample.Scale.weight_zero line 47
14. lemma OAI.HarmonicCounterexample.Scale.weight_tail line 50
15. lemma OAI.HarmonicCounterexample.Scale.weight_smooth line 53
16. lemma OAI.HarmonicCounterexample.Scale.weight_nonneg line 65
17. lemma OAI.HarmonicCounterexample.Scale.weight_le_one line 70
18. lemma OAI.HarmonicCounterexample.Scale.primitive_hasDerivAt line 77
19. lemma OAI.HarmonicCounterexample.Scale.primitive_smooth line 82
20. lemma OAI.HarmonicCounterexample.Scale.primitive_zero line 89
21. lemma OAI.HarmonicCounterexample.Scale.primitive_nonneg line 97
22. lemma OAI.HarmonicCounterexample.Scale.primitive_tail line 102
23. lemma OAI.HarmonicCounterexample.Scale.total_pos line 126
24. lemma OAI.HarmonicCounterexample.Scale.primitive_le_total line 132
25. lemma OAI.HarmonicCounterexample.Scale.primitive_limit line 144
26. lemma OAI.HarmonicCounterexample.Scale.profile_smooth line 156
27. lemma OAI.HarmonicCounterexample.Scale.profile_pos line 159
28. lemma OAI.HarmonicCounterexample.Scale.profile_le_one line 161
29. lemma OAI.HarmonicCounterexample.Scale.profile_lower line 165
30. lemma OAI.HarmonicCounterexample.Scale.profile_initial line 170
31. lemma OAI.HarmonicCounterexample.Scale.profile_limit line 173
32. lemma OAI.HarmonicCounterexample.Scale.profile_hasDerivAt line 178
33. lemma OAI.HarmonicCounterexample.Scale.profile_logSlope line 182
34. lemma OAI.HarmonicCounterexample.Scale.slope_nonpos line 185
35. lemma OAI.HarmonicCounterexample.Scale.slope_lower line 188
36. lemma OAI.HarmonicCounterexample.Scale.weight_deriv line 212
37. lemma OAI.HarmonicCounterexample.Scale.slope_deriv line 226
38. lemma OAI.HarmonicCounterexample.Scale.slope_deriv_bound line 229
39. lemma OAI.HarmonicCounterexample.Scale.slope_initial_deriv line 245
40. theorem OAI.HarmonicCounterexample.Scale.radial_concavity line 253

    Source documentation

    The exact concavity estimate used on the whole initial round region, not merely the limiting tail.

    theorem radial_concavity {μ : ℝ} (hμ : 0 ≤ μ) (hμ1 : μ ≤ 1/4) (t : ℝ) :
        slope μ t + deriv (slope μ) t + slope μ t ^ 2 ≤ 0 := by
    …

    Mentions: OAI.HarmonicCounterexample.Scale.slope

41. lemma OAI.HarmonicCounterexample.Scale.log_profile_tail line 271
42. lemma OAI.HarmonicCounterexample.Scale.slope_tail line 278
43. lemma OAI.HarmonicCounterexample.Scale.profile_antitone line 281
44. theorem OAI.HarmonicCounterexample.Scale.choose_scale line 289

    Source documentation

    Every requested subunit endpoint sufficiently close to one is attained by the same fixed cutoff, before any control family is specified.

    theorem choose_scale {a : ℝ} (ha : 0 < a) (ha1 : a < 1)
        (hclose : Real.exp (-total/4) ≤ a) :
        ∃ μ : ℝ, 0 < μ ∧ μ ≤ 1/4 ∧
          Tendsto (profile μ) atTop (𝓝 a) ∧ Real.exp (-μ*total) = a := by
    …

    Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.Scale.total, OAI.HarmonicCounterexample.Scale.profile

45. lemma OAI.HarmonicCounterexample.Scale.radial_tail_margin line 324
46. lemma OAI.HarmonicCounterexample.Scale.slope_limit line 340
47. lemma OAI.HarmonicCounterexample.Scale.slope_deriv_tail line 350
48. lemma OAI.HarmonicCounterexample.Scale.slope_deriv_limit line 365
49. def OAI.HarmonicCounterexample.Schedule.pulse line 398

    Source documentation

    Source period j is indexed here by j-1; no period lengths are changed.

    def pulse (j : ℕ) : ℝ := (j + 1 : ℝ) ^ 6

50. def OAI.HarmonicCounterexample.Schedule.dwell line 399
51. def OAI.HarmonicCounterexample.Schedule.time line 400
52. def OAI.HarmonicCounterexample.Schedule.dwellSum line 401
53. theorem OAI.HarmonicCounterexample.Schedule.time_zero line 403
54. theorem OAI.HarmonicCounterexample.Schedule.time_succ line 404
55. theorem OAI.HarmonicCounterexample.Schedule.sum_pow_seven line 408
56. theorem OAI.HarmonicCounterexample.Schedule.sum_pow_six line 419
57. theorem OAI.HarmonicCounterexample.Schedule.dwellSum_formula line 430
58. theorem OAI.HarmonicCounterexample.Schedule.time_formula line 435
59. theorem OAI.HarmonicCounterexample.Schedule.time_pos line 443
60. theorem OAI.HarmonicCounterexample.Schedule.dwellSum_nonneg line 447
61. theorem OAI.HarmonicCounterexample.Schedule.tendsto_inv_nat line 450
62. theorem OAI.HarmonicCounterexample.Schedule.dwellSum_scaled line 453
63. theorem OAI.HarmonicCounterexample.Schedule.time_scaled line 466
64. theorem OAI.HarmonicCounterexample.Schedule.dwell_scaled line 483
65. theorem OAI.HarmonicCounterexample.Schedule.pulse_scaled line 493
66. lemma OAI.HarmonicCounterexample.Schedule.cancel_scale_limit line 503
67. theorem OAI.HarmonicCounterexample.Schedule.dwellSum_time line 516
68. theorem OAI.HarmonicCounterexample.Schedule.dwell_time line 520
69. theorem OAI.HarmonicCounterexample.Schedule.pulse_time line 524
70. theorem OAI.HarmonicCounterexample.Schedule.duration_time line 528
71. theorem OAI.HarmonicCounterexample.Schedule.time_strictMono line 537
72. theorem OAI.HarmonicCounterexample.Schedule.time_atTop line 545
73. theorem OAI.HarmonicCounterexample.Schedule.dwellSum_atTop line 554
74. def OAI.HarmonicCounterexample.Pulses.ramp line 586

    Source documentation

    A globally smooth, fixed ramp, constant on neighborhoods of both endpoints.

    def ramp (t : ℝ) : ℝ := Real.smoothTransition (2*t-1/2)

75. lemma OAI.HarmonicCounterexample.Pulses.ramp_smooth line 588
76. lemma OAI.HarmonicCounterexample.Pulses.ramp_zero line 590
77. lemma OAI.HarmonicCounterexample.Pulses.ramp_one line 592
78. lemma OAI.HarmonicCounterexample.Pulses.ramp_range line 594
79. lemma OAI.HarmonicCounterexample.Pulses.ramp_mono line 596
80. lemma OAI.HarmonicCounterexample.Pulses.pulse_pos line 599
81. lemma OAI.HarmonicCounterexample.Pulses.dwell_pos line 600
82. theorem OAI.HarmonicCounterexample.Pulses.smooth_escaping_sum line 604

    Source documentation

    Smoothness of this series is LOCAL FINITENESS, not an unproved convergence claim or an exchange of derivatives and a general infinite sum.

    theorem smooth_escaping_sum {f : ℕ → ℝ → ℝ} (hf : ∀ j, ContDiff ℝ ∞ (f j))
        (hz : ∀ j t, t ≤ time j → f j t = 0) :
        ContDiff ℝ ∞ (fun t => ∑' j, f j t) := by
    …

83. def OAI.HarmonicCounterexample.Pulses.window line 618

    Source documentation

    The upward and downward ramps, with the exact dwell and rest schedule.

    def window (j : ℕ) (t : ℝ) : ℝ :=
    …

84. lemma OAI.HarmonicCounterexample.Pulses.window_smooth line 622
85. lemma OAI.HarmonicCounterexample.Pulses.window_zero_before line 626
86. lemma OAI.HarmonicCounterexample.Pulses.window_zero_after line 636
87. lemma OAI.HarmonicCounterexample.Pulses.window_one line 646
88. lemma OAI.HarmonicCounterexample.Pulses.window_range line 656
89. def OAI.HarmonicCounterexample.Pulses.increment line 667

    Source documentation

    Controls are arbitrary across periods; only each individual scalar bump is smooth.

    def increment (z : ℕ → ℝ → ℝ) (qstar : ℝ) (j : ℕ) (t : ℝ) : ℝ :=
    …

90. def OAI.HarmonicCounterexample.Pulses.profile line 670
91. lemma OAI.HarmonicCounterexample.Pulses.increment_smooth line 673
92. lemma OAI.HarmonicCounterexample.Pulses.increment_zero_before line 679
93. lemma OAI.HarmonicCounterexample.Pulses.increment_zero_after line 687
94. lemma OAI.HarmonicCounterexample.Pulses.profile_smooth line 697
95. lemma OAI.HarmonicCounterexample.Pulses.profile_initial line 711
96. lemma OAI.HarmonicCounterexample.Pulses.profile_period line 722
97. lemma OAI.HarmonicCounterexample.GlobalGrowth.grid_bracket line 760

    Source documentation

    Every late real time lies between consecutive entries of an unbounded grid. No interpolation or endpoint-only growth convention is used.

    lemma grid_bracket {τ : ℕ → ℝ} (hτ : Tendsto τ atTop atTop)
        (N : ℕ) {t : ℝ} (ht : τ N ≤ t) :
        ∃ j ≥ N, τ j ≤ t ∧ t ≤ τ (j+1) := by
    …

98. theorem OAI.HarmonicCounterexample.GlobalGrowth.all_time_log_bound line 782

    Source documentation

    The full real-time bridge in the proof of the main theorem. A bounded Riccati matrix controls each period, and sublinear period lengths prevent hidden growth between endpoints.

    theorem all_time_log_bound {τ : ℕ → ℝ} {w : ℝ → ℝ} {d α C : ℝ}
        (hτ : Tendsto τ atTop atTop) (hpos : ∀ j, 0 < τ j)
        (hend : Tendsto (fun j => w (τ j) / τ j) atTop (𝓝 d))
        (hduration : Tendsto (fun j => (τ (j+1) - τ j) / τ j) atTop (𝓝 0))
        (hlocal : ∀ᶠ j in atTop, ∀ t ∈ Set.Icc (τ j) (τ (j+1)),
          w t ≤ w (τ j) + C * (τ (j+1) - τ j))
        (hd : 0 ≤ d) (hα : d < α) :
        ∀ᶠ t in atTop, w t ≤ α * t := by
    …

99. theorem OAI.HarmonicCounterexample.GlobalGrowth.radial_power_bound line 806

    Source documentation

    Passing from logarithmic time to radius is an actual bound on every sufficiently large radius, not just on the discrete schedule.

    theorem radial_power_bound {y : ℝ → ℝ} {α : ℝ}
        (hy : ∀ t, 0 ≤ y t)
        (hlog : ∀ᶠ t in atTop, Real.log (y t) ≤ α * t) :
        ∀ᶠ r in atTop, y (Real.log r) ≤ r ^ α := by
    …

100. lemma OAI.HarmonicCounterexample.Pulses.profile_bounds_on_period line 845
101. theorem OAI.HarmonicCounterexample.Pulses.choose_positive_start line 865

     Source documentation

     Uniform positivity is obtained by delaying the pulses, with NO dependence on the subsequently chosen sequence of parameters.

     theorem choose_positive_start {z : ℕ → ℝ → ℝ} {M qstar : ℝ}
         (hz0 : ∀ j u, u ≤ 0 → z j u = 0) (hz1 : ∀ j u, 1 ≤ u → z j u = 0)
         (hbound : ∀ j u, |z j u| ≤ M) (hq : 1 ≤ qstar) :
         ∃ j0 : ℕ, ∀ t, 1/2 ≤ profile z qstar j0 t ∧
           profile z qstar j0 t ≤ qstar + 1/2 := by
     …

     Mentions: OAI.HarmonicCounterexample.Pulses.profile

102. lemma OAI.HarmonicCounterexample.Pulses.profile_pulse line 884
103. lemma OAI.HarmonicCounterexample.Pulses.profile_dwell line 894
104. lemma OAI.HarmonicCounterexample.Pulses.profile_rest line 906
105. lemma OAI.HarmonicCounterexample.Pulses.deriv_eqOn_Icc line 941
106. lemma OAI.HarmonicCounterexample.Pulses.deriv_two_eqOn_Icc line 950
107. lemma OAI.HarmonicCounterexample.Pulses.affine_composition_deriv line 959
108. lemma OAI.HarmonicCounterexample.Pulses.affine_composition_hasDerivAt line 964
109. lemma OAI.HarmonicCounterexample.Pulses.window_deriv line 969
110. lemma OAI.HarmonicCounterexample.Pulses.window_deriv_two line 986
111. lemma OAI.HarmonicCounterexample.Pulses.increment_deriv line 1008
112. lemma OAI.HarmonicCounterexample.Pulses.increment_deriv_two line 1021
113. lemma OAI.HarmonicCounterexample.Pulses.profile_deriv_period line 1040
114. lemma OAI.HarmonicCounterexample.Pulses.profile_deriv_two_period line 1051
115. lemma OAI.HarmonicCounterexample.Pulses.bounded_of_zero_outside line 1085
116. lemma OAI.HarmonicCounterexample.Pulses.ramp_locally_constant line 1095
117. lemma OAI.HarmonicCounterexample.Pulses.ramp_derivatives_bounded line 1106
118. lemma OAI.HarmonicCounterexample.Pulses.pulse_one_le line 1116
119. lemma OAI.HarmonicCounterexample.Pulses.window_deriv_bound line 1122
120. lemma OAI.HarmonicCounterexample.Pulses.window_deriv_two_bound line 1131
121. lemma OAI.HarmonicCounterexample.Pulses.increment_deriv_bound line 1140
122. lemma OAI.HarmonicCounterexample.Pulses.increment_deriv_two_bound line 1160
123. theorem OAI.HarmonicCounterexample.Pulses.profile_derivative_bounds line 1182

     Source documentation

     The time derivatives are controlled uniformly on each CLOSED period, including both joining points. Constants depend on the fixed pulse family, never its history.

     theorem profile_derivative_bounds {z : ℕ → ℝ → ℝ} (hs : ∀ j, ContDiff ℝ ∞ (z j))
         (hz0 : ∀ j u, u ≤ 0 → z j u = 0) (hz1 : ∀ j u, 1 ≤ u → z j u = 0)
         {M1 M2 : ℝ} (hM1 : ∀ j t, |deriv (z j) t| ≤ M1)
         (hM2 : ∀ j t, |deriv (deriv (z j)) t| ≤ M2) (qstar : ℝ) :
         ∃ C1 C2 : ℝ, 0 ≤ C1 ∧ 0 ≤ C2 ∧ ∀ j0 j, j0 ≤ j →
           ∀ t ∈ Set.Icc (time j) (time (j+1)),
             |deriv (profile z qstar j0) t| ≤ C1/pulse j ∧
             |deriv (deriv (profile z qstar j0)) t| ≤ C2/pulse j^2 := by
     …

     Mentions: OAI.HarmonicCounterexample.Pulses.profile

124. def OAI.HarmonicCounterexample.Pulses.logSlope line 1224

     Source documentation

     Half the logarithmic derivative of the volume-normalized Berger anisotropy.

     def logSlope (q : ℝ → ℝ) (t : ℝ) : ℝ := deriv q t / (2*q t)

125. lemma OAI.HarmonicCounterexample.Pulses.logSlope_smooth line 1226
126. lemma OAI.HarmonicCounterexample.Pulses.logSlope_deriv line 1231
127. lemma OAI.HarmonicCounterexample.Pulses.logSlope_bound line 1240
128. lemma OAI.HarmonicCounterexample.Pulses.logSlope_deriv_bound line 1246
129. lemma OAI.HarmonicCounterexample.Schedule.time_succ_upper line 1291
130. lemma OAI.HarmonicCounterexample.Schedule.period_weight_bound line 1312
131. lemma OAI.HarmonicCounterexample.Berger.scale_margin_on_period line 1352
132. theorem OAI.HarmonicCounterexample.Berger.radial_budget_index line 1374

     Source documentation

     A single late index absorbs the entire radial curvature cost uniformly in all subsequent controls satisfying the fixed derivative bound.

     theorem radial_budget_index {m μ C : ℝ} (hm : 1 ≤ m) (hμ : 0 < μ) :
         ∃ J : ℕ, ∀ j ≥ J, 64*C^2 ≤ m*μ*(j+1:ℝ)^2 := by
     …

133. theorem OAI.HarmonicCounterexample.Berger.radialRicci_of_pulse_budget line 1389
134. def OAI.HarmonicCounterexample.Berger.tangentH line 1428

     Source documentation

     The two tangent Ricci eigenvalues as continuous functions of the six scalar profile jets. The harmless positive clamp is inactive wherever q≥1/2.

     def tangentH (m : ℝ) (X : Fin 6 → ℝ) : ℝ :=
     …

135. def OAI.HarmonicCounterexample.Berger.tangentV line 1431
136. lemma OAI.HarmonicCounterexample.Berger.tangentH_continuous line 1435
137. lemma OAI.HarmonicCounterexample.Berger.tangentV_continuous line 1442
138. def OAI.HarmonicCounterexample.Berger.staticJet line 1449
139. lemma OAI.HarmonicCounterexample.Berger.staticJet_continuous line 1451
140. lemma OAI.HarmonicCounterexample.Berger.staticH line 1456
141. lemma OAI.HarmonicCounterexample.Berger.staticV line 1462
142. theorem OAI.HarmonicCounterexample.Berger.tangent_budget_tube line 1470

     Source documentation

     The strict link margin yields a uniform open neighborhood of positive horizontal and vertical Ricci jets along the ENTIRE compact Berger segment.

     theorem tangent_budget_tube {m a qstar : ℝ}
         (hH : ∀ q ∈ Set.Icc 1 qstar, 0 < m+1-2*q-(m-1)*a^2*q^(-1/m))
         (hV : ∀ q ∈ Set.Icc 1 qstar, 0 < (m-1)*q*(q-a^2*q^(-1/m))) :
         ∃ δ > 0, ∀ (X : Fin 6 → ℝ) (q : ℝ), q ∈ Set.Icc 1 qstar →
           dist X (staticJet a q) < δ → 0 < tangentH m X ∧ 0 < tangentV m X := by
     …

     Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.Berger.staticJet, OAI.HarmonicCounterexample.Berger.tangentH, OAI.HarmonicCounterexample.Berger.tangentV

143. lemma OAI.HarmonicCounterexample.Berger.static_vertical_margin line 1490

     Source documentation

     Positivity of the vertical static margin follows directly from a<1.

     lemma static_vertical_margin {m a q : ℝ} (hm : 1 < m) (ha : a^2 < 1) (hq : 1 ≤ q) :
         0 < (m-1)*q*(q-a^2*q^(-1/m)) := by
     …

     Mentions: OAI.HarmonicCounterexample.a

144. theorem OAI.HarmonicCounterexample.Berger.tangent_budget_coordinates line 1521
145. lemma OAI.HarmonicCounterexample.Berger.clamp_segment line 1548

     Source documentation

     Any anisotropy in an epsilon enlargement of the closed dwell segment is within epsilon of an actual point of that segment.

     lemma clamp_segment {qstar q ε : ℝ} (hqstar : 1 ≤ qstar)
         (hlo : 1-ε ≤ q) (hhi : q ≤ qstar+ε) (he : 0 ≤ ε) :
         ∃ q0 ∈ Set.Icc 1 qstar, |q-q0| ≤ ε := by
     …

146. lemma OAI.HarmonicCounterexample.Schedule.pulse_atTop_limit line 1579
147. lemma OAI.HarmonicCounterexample.Schedule.pulse_reciprocal_limit line 1584
148. lemma OAI.HarmonicCounterexample.Schedule.pulse_reciprocal_square_limit line 1589
149. theorem OAI.HarmonicCounterexample.Berger.tangentRicci_of_pulse_budget line 1620

     Source documentation

     Uniform tangent curvature budget, independent of the later control sequence. All hypotheses concerning q are the bounds already proved for the actual pulse profile; the smallness index is produced from the fixed scale and fixed family.

     theorem tangentRicci_of_pulse_budget {m a μ qstar M C1 C2 : ℝ}
         (hM : 0 ≤ M) (hqstar : 1 ≤ qstar)
         (ha : Tendsto (Scale.profile μ) atTop (𝓝 a))
         (hH : ∀ q ∈ Set.Icc 1 qstar, 0 < m+1-2*q-(m-1)*a^2*q^(-1/m))
         (hV : ∀ q ∈ Set.Icc 1 qstar, 0 < (m-1)*q*(q-a^2*q^(-1/m))) :
         ∃ J : ℕ, ∀ j ≥ J, ∀ (q : ℝ → ℝ) (t : ℝ),
           ContDiff ℝ ∞ q → 1/2 ≤ q t →
           1-M/pulse j ≤ q t → q t ≤ qstar+M/pulse j →
           |deriv q t| ≤ C1/pulse j → |deriv (deriv q) t| ≤ C2/(pulse j)^2 →
           time j ≤ t →
           0 < horizontalRicciNumerator (m+1)
             ((Scale.profile μ t)^2*(q t)^(-1/m)) (q t)
     …

     Mentions: OAI.HarmonicCounterexample.a, OAI.HarmonicCounterexample.Scale.profile, OAI.HarmonicCounterexample.Berger.horizontalRicciNumerator

150. lemma OAI.HarmonicCounterexample.christoffel_eq_zero_of_locallyConstant line 1688
151. lemma OAI.HarmonicCounterexample.ricci_eq_zero_of_locallyConstant line 1696
152. lemma OAI.HarmonicCounterexample.Cartesian.rawCoefficient_locally_fixed line 1729
153. theorem OAI.HarmonicCounterexample.Cartesian.bergerMetric_ricciNonnegative line 1746

     Source documentation

     Genuine global Ricci positivity of the constructed smooth metric from the three exact scalar eigenvalue inequalities. The origin and all switching gaps are included; no differentiability of the label function is required.

     theorem bergerMetric_ricciNonnegative (c q u v : ℝ → ℝ)
         (J : ℝ → ComplexStructure (Fin n))
         (hc : ContDiff ℝ ∞ c) (hq : ContDiff ℝ ∞ q)
         (hcp : ∀ t, 0 < c t) (hqp : ∀ t, 0 < q t)
         (hJ : ∀ t, (∀ᶠ s in 𝓝 t, J s = J t) ∨ (∀ᶠ s in 𝓝 t, q s = 1))
         {T : ℝ} (hc0 : ∀ t ≤ T, c t = 1) (hq0 : ∀ t ≤ T, q t = 1)
         (hdc : ∀ t, HasDerivAt c (2*c t*u t) t)
         (hdq : ∀ t, HasDerivAt q (2*q t*v t) t)
         (hu : Differentiable ℝ u) (hv : Differentiable ℝ v)
         (hR : ∀ t, 0 ≤ radialRicciNumerator n (u t) (v t) (deriv u t) (deriv v t))
         (hH : ∀ t, 0 ≤ horizontalRicciNumerator n (c t) (q t) (u t) (v t) (deriv u t))
         (hV : ∀ t, 0 ≤ verticalRicciNumerator n (c t) (q t) (u t) (v t) (deriv u t) (deriv v t)) :
     …