OAI/MathematicalPhysics/Transonic/Core.lean

GitHub source file

340 declarations, 0 contain sorry, 0 declared as axioms

The normalized sonic equation is regular singular. After removing its nonresonant finite jet, the remaining problem has the form z g' + c g = z H(z, g) with c > 0. The analytic disk space below supports a contraction argument for this equation.

  1. abbrev OAI.SepticProfile.Fuchsian.Disk line 43
  2. abbrev OAI.SepticProfile.Fuchsian.DiskMap line 44
  3. def OAI.SepticProfile.Fuchsian.extend line 46
  4. theorem OAI.SepticProfile.Fuchsian.extend_coe line 50
  5. theorem OAI.SepticProfile.Fuchsian.extend_zero line 53
  6. theorem OAI.SepticProfile.Fuchsian.extend_add line 57
  7. theorem OAI.SepticProfile.Fuchsian.extend_smul line 62
  8. def OAI.SepticProfile.Fuchsian.analyticDisk line 68
  9. theorem OAI.SepticProfile.Fuchsian.analyticDisk_closed line 78
  10. instance OAI.SepticProfile.Fuchsian.(instance at line 95) line 95
  11. abbrev OAI.SepticProfile.Fuchsian.UnitInterval line 97
  12. def OAI.SepticProfile.Fuchsian.diskScale line 99
  13. theorem OAI.SepticProfile.Fuchsian.continuous_diskScale line 106
  14. theorem OAI.SepticProfile.Fuchsian.scale_mem_ball line 111
  15. def OAI.SepticProfile.Fuchsian.dilateMap line 117
  16. theorem OAI.SepticProfile.Fuchsian.extend_dilate_on line 121
  17. theorem OAI.SepticProfile.Fuchsian.dilate_analytic line 130
  18. def OAI.SepticProfile.Fuchsian.dilate line 139
  19. theorem OAI.SepticProfile.Fuchsian.norm_dilate_le line 142
  20. theorem OAI.SepticProfile.Fuchsian.continuous_dilate line 148
  21. def OAI.SepticProfile.Fuchsian.clip line 153
  22. def OAI.SepticProfile.Fuchsian.radialIntegrand line 155
  23. def OAI.SepticProfile.Fuchsian.radialIntegral line 158
  24. theorem OAI.SepticProfile.Fuchsian.continuous_radialIntegrand line 161
  25. theorem OAI.SepticProfile.Fuchsian.norm_radialIntegrand_le line 166
  26. theorem OAI.SepticProfile.Fuchsian.norm_radialIntegral_le line 176
  27. theorem OAI.SepticProfile.Fuchsian.differentiableAt_extend line 189
  28. theorem OAI.SepticProfile.Fuchsian.deriv_bound line 193
  29. def OAI.SepticProfile.Fuchsian.derivLinear line 213
  30. def OAI.SepticProfile.Fuchsian.derivEval line 222
  31. def OAI.SepticProfile.Fuchsian.eval line 228
  32. theorem OAI.SepticProfile.Fuchsian.eval_apply line 231
  33. theorem OAI.SepticProfile.Fuchsian.deriv_dilate line 233
  34. theorem OAI.SepticProfile.Fuchsian.clip_coe line 248
  35. theorem OAI.SepticProfile.Fuchsian.radialIntegrand_eval line 251
  36. theorem OAI.SepticProfile.Fuchsian.radialIntegrand_deriv line 261
  37. def OAI.SepticProfile.Fuchsian.radialOperator line 281
  38. theorem OAI.SepticProfile.Fuchsian.radialOperator_apply line 285
  39. theorem OAI.SepticProfile.Fuchsian.radial_primitive_deriv line 293
  40. theorem OAI.SepticProfile.Fuchsian.radial_primitive_continuous line 318
  41. theorem OAI.SepticProfile.Fuchsian.radialIntegral_ode line 338
  42. def OAI.SepticProfile.Fuchsian.coordinateMulMap line 355
  43. theorem OAI.SepticProfile.Fuchsian.extend_coordinateMulMap line 358
  44. def OAI.SepticProfile.Fuchsian.coordinateMul line 367
  45. theorem OAI.SepticProfile.Fuchsian.norm_coordinateMul_le line 373
  46. theorem OAI.SepticProfile.Fuchsian.coordinateMul_sub line 385
  47. theorem OAI.SepticProfile.Fuchsian.radialIntegrand_sub line 392
  48. theorem OAI.SepticProfile.Fuchsian.radialIntegral_sub line 400
  49. def OAI.SepticProfile.Fuchsian.inverse line 407
  50. theorem OAI.SepticProfile.Fuchsian.norm_inverse_le line 410
  51. theorem OAI.SepticProfile.Fuchsian.inverse_sub line 413
  52. theorem OAI.SepticProfile.Fuchsian.inverse_ode line 418
  53. theorem OAI.SepticProfile.Fuchsian.inverse_zero line 435
  54. theorem OAI.SepticProfile.Fuchsian.exists_fuchsian_disk_invariant line 442

    Source documentation

    Bounds on an analytic right-hand side give an invariant fixed point of the regular-singular integral operator.

     theorem exists_fuchsian_disk_invariant {c r R M L : ℝ} (hc : 0 ≤ c) (hr : 0 ≤ r)
    (hR : 0 ≤ R) (hrM : r * M ≤ R) (hrL : r * L ≤ 1/2)
    (H : analyticDisk → analyticDisk)
    (hbound : ∀ f, ‖f‖ ≤ R → ‖H f‖ ≤ M)
    (hlip : ∀ f g, ‖f‖ ≤ R → ‖g‖ ≤ R → ‖H f - H g‖ ≤ L * ‖f-g‖)
    (P : Set analyticDisk) (hPc : IsClosed P) (hP0 : 0 ∈ P)
    (hP : ∀ f ∈ P, ‖f‖ ≤ R → (r : ℂ) • inverse c (H f) ∈ P) :
    ∃ f : analyticDisk, f ∈ P ∧ ‖f‖ ≤ R ∧ extend (f : DiskMap) 0 = 0 ∧
      ∀ z ∈ ball (0 : ℂ) 1,
        z * deriv (extend (f : DiskMap)) z + (c : ℂ) * extend (f : DiskMap) z =
          (r : ℂ) * z * extend (H f : DiskMap) z := by
…

    Mentions: OAI.SepticProfile.Fuchsian.analyticDisk, OAI.SepticProfile.Fuchsian.inverse, OAI.SepticProfile.Fuchsian.extend, OAI.SepticProfile.Fuchsian.DiskMap

  55. theorem OAI.SepticProfile.Fuchsian.exists_fuchsian_disk line 508
  56. theorem OAI.SepticProfile.Fuchsian.inputBound line 521
  57. def OAI.SepticProfile.Fuchsian.composeMap line 530
  58. theorem OAI.SepticProfile.Fuchsian.extend_composeMap line 537
  59. def OAI.SepticProfile.Fuchsian.composeDisk line 545
  60. def OAI.SepticProfile.Fuchsian.nonlinearDisk line 561
  61. theorem OAI.SepticProfile.Fuchsian.nonlinearDisk_apply line 567
  62. theorem OAI.SepticProfile.Fuchsian.norm_nonlinearDisk_le line 575
  63. theorem OAI.SepticProfile.Fuchsian.nonlinearDisk_lip line 596
  64. theorem OAI.SepticProfile.Fuchsian.exists_scaled_fuchsian line 614
  65. def OAI.SepticProfile.Fuchsian.realDisk line 659
  66. theorem OAI.SepticProfile.Fuchsian.realDisk_closed line 661
  67. theorem OAI.SepticProfile.Fuchsian.realDisk_zero line 666
  68. theorem OAI.SepticProfile.Fuchsian.realDisk_real_smul line 670
  69. theorem OAI.SepticProfile.Fuchsian.realDisk_radialIntegral line 677
  70. theorem OAI.SepticProfile.Fuchsian.realDisk_inverse line 695
  71. theorem OAI.SepticProfile.Fuchsian.exists_scaled_real_fuchsian line 702
  72. theorem OAI.SepticProfile.Fuchsian.exists_real_fuchsian_germ line 758

    Source documentation

    Real analytic local solvability of the post-jet regular-singular equation. The radius is constructed and positive; existence is not an input hypothesis.

     theorem exists_real_fuchsian_germ {c : ℝ} (hc : 0 ≤ c) (h : ℂ × ℂ → ℂ)
    (ha : AnalyticAt ℂ h 0)
    (hreal : ∀ p : ℂ × ℂ, p.1.im = 0 → p.2.im = 0 → (h p).im = 0) :
    ∃ F : ℂ → ℂ, AnalyticAt ℂ F 0 ∧ F 0 = 0 ∧
      (∀ x : ℝ, (F x).im = 0) ∧
      ∀ᶠ z in 𝓝 (0 : ℂ), z * deriv F z + (c : ℂ)*F z = z*h (z,F z) := by
…
  73. abbrev OAI.SepticProfile.Formal.Series line 806
  74. def OAI.SepticProfile.Formal.z line 808
  75. def OAI.SepticProfile.Formal.prefactor line 810
  76. def OAI.SepticProfile.Formal.den line 811
  77. def OAI.SepticProfile.Formal.r line 812
  78. def OAI.SepticProfile.Formal.t line 813
  79. def OAI.SepticProfile.Formal.residual line 814
  80. def OAI.SepticProfile.Formal.lin line 817
  81. lemma OAI.SepticProfile.Formal.coefficient_shift_zero line 821
  82. lemma OAI.SepticProfile.Formal.coefficient_shift_same line 826
  83. lemma OAI.SepticProfile.Formal.coefficient_monomial_second_order line 830
  84. lemma OAI.SepticProfile.Formal.derivative_monomial line 838
  85. lemma OAI.SepticProfile.Formal.coefficient_monomial_derivative line 847
  86. lemma OAI.SepticProfile.Formal.residual_linearization line 857
  87. lemma OAI.SepticProfile.Formal.residual_monomial_perturbation line 869
  88. lemma OAI.SepticProfile.Formal.coeff_den_one line 880
  89. lemma OAI.SepticProfile.Formal.coeff_lin_zero line 888
  90. lemma OAI.SepticProfile.Formal.coeff_den_derivative_monomial line 899
  91. lemma OAI.SepticProfile.Formal.coeff_lin_monomial line 912
  92. lemma OAI.SepticProfile.Formal.coefficient_step line 923

    Source documentation

    The exact nth-jet coefficient includes all nonlinear terms in the normalization. Its multiplier vanishes at an integral slope ratio.

    lemma coefficient_step (sigma kappa c : K) (u : Series K) (s : K)
    (hu0 : constantCoeff u = 1) (hu1 : coeff 1 u = s) (n : ℕ) (a : K) :
    coeff (n+2) (residual sigma kappa c (u+C a*X^(n+2))) =
      coeff (n+2) (residual sigma kappa c u) +
        ((1-c)*(2*kappa+3)-2*(1-sigma)*s*(n+3))*a := by
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.Formal.Series, OAI.SepticProfile.Formal.residual

  93. def OAI.SepticProfile.Formal.Agree line 936

    Source comment

    Coefficient locality at the singular point. Although differentiating costs one coefficient, its multiplier has zero constant term, so the nth residual coefficient only depends on coefficients through n.
    def Agree (n : ℕ) (u v : Series K) : Prop :=
…

    Mentions: OAI.SepticProfile.Formal.Series

  94. lemma OAI.SepticProfile.Formal.Agree.refl line 939
  95. lemma OAI.SepticProfile.Formal.Agree.add line 941
  96. lemma OAI.SepticProfile.Formal.Agree.sub line 946
  97. lemma OAI.SepticProfile.Formal.Agree.mul line 951
  98. lemma OAI.SepticProfile.Formal.Agree.pow line 960
  99. lemma OAI.SepticProfile.Formal.Agree.mul_derivative line 966
  100. lemma OAI.SepticProfile.Formal.residual_agree line 980
  101. def OAI.SepticProfile.Formal.before line 995
  102. lemma OAI.SepticProfile.Formal.coeff_before line 998
  103. lemma OAI.SepticProfile.Formal.before_zero line 1001
  104. lemma OAI.SepticProfile.Formal.before_one line 1006
  105. lemma OAI.SepticProfile.Formal.agree_before_next line 1009
  106. lemma OAI.SepticProfile.Formal.step_at line 1017
  107. def OAI.SepticProfile.SourceJets.residualP line 1040

    Source documentation

    The literal normalized source polynomial residual, expanded about z=1.

    def residualP (sigma kappa c : K) (u : Polynomial K) : Polynomial K :=
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa

  108. theorem OAI.SepticProfile.SourceJets.coe_residualP line 1044
  109. theorem OAI.SepticProfile.SourceJets.coeff_residual_one line 1054
  110. theorem OAI.SepticProfile.SourceJets.constantCoeff_residual line 1067
  111. theorem OAI.SepticProfile.SourceJets.exists_finite_jet line 1077

    Source documentation

    Construct all required finite sonic jets at a nonresonant weak slope. There is no assumed formal series. The zero multiplier at a resonance is explicitly excluded; this is why the resonant parameter cannot be used as a selected analytic profile parameter.

     theorem exists_finite_jet (sigma kappa c s : K)
    (hs : 2*(1-sigma)*s^2-(1-c)*(2*kappa+3)*s+3*(1-c)=0)
    (N : ℕ)
    (hne : ∀ n < N, (1-c)*(2*kappa+3)-2*(1-sigma)*s*(n+3) ≠ 0) :
    ∃ p : Polynomial K, p.coeff 0=1 ∧ p.coeff 1=s ∧
      ∀ i ≤ N+1, (residualP sigma kappa c p).coeff i=0 := by
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.SourceJets.residualP

  112. theorem OAI.SepticProfile.SourceJets.exists_finite_jet_divisible line 1132
  113. def OAI.SepticProfile.Remainder.pref line 1149
  114. def OAI.SepticProfile.Remainder.den line 1150
  115. def OAI.SepticProfile.Remainder.amp line 1151
  116. def OAI.SepticProfile.Remainder.trans line 1152
  117. def OAI.SepticProfile.Remainder.res line 1153
  118. def OAI.SepticProfile.Remainder.lin line 1155
  119. def OAI.SepticProfile.Remainder.quad line 1157
  120. def OAI.SepticProfile.Remainder.denDiff line 1161
  121. theorem OAI.SepticProfile.Remainder.den_expansion line 1163
  122. theorem OAI.SepticProfile.Remainder.res_expansion line 1168
  123. def OAI.SepticProfile.Remainder.denQuot line 1175
  124. theorem OAI.SepticProfile.Remainder.den_factor line 1177
  125. def OAI.SepticProfile.Remainder.jetA line 1182
  126. def OAI.SepticProfile.Remainder.jetE line 1185
  127. theorem OAI.SepticProfile.Remainder.jet_identity line 1190

    Source documentation

    Exact cleared algebraic identity; no small-denominator approximation.

    theorem jet_identity (sigma kappa c rho x p p1 dp s e g dg : K) (m : ℕ)
    (hp : p=1+x*p1)
    (hr : res sigma kappa c x p dp=x^(m+3)*s)
    (hl : rho*denQuot sigma x p1+lin sigma kappa c x p dp=x*e) :
    res sigma kappa c x (p+x^(m+2)*g)
      (dp+(m+2)*x^(m+1)*g+x^(m+2)*dg) =
      x^(m+2)*(jetA sigma x p p1 g m * (x*dg+((m+2)-rho)*g)+
        x*jetE sigma kappa c rho x p dp s e g m) := by
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.Remainder.res, OAI.SepticProfile.Remainder.denQuot, OAI.SepticProfile.Remainder.lin, OAI.SepticProfile.Remainder.jetA, OAI.SepticProfile.Remainder.jetE

  128. theorem OAI.SepticProfile.Remainder.jetA_zero line 1207
  129. def OAI.SepticProfile.SourceSonic.prefP line 1217
  130. def OAI.SepticProfile.SourceSonic.denQuotP line 1218
  131. def OAI.SepticProfile.SourceSonic.transP line 1219
  132. def OAI.SepticProfile.SourceSonic.linP line 1221
  133. theorem OAI.SepticProfile.SourceSonic.split_polynomial line 1225
  134. theorem OAI.SepticProfile.SourceSonic.coeff_denQuotP line 1235
  135. theorem OAI.SepticProfile.SourceSonic.coeff_linP line 1242
  136. theorem OAI.SepticProfile.SourceSonic.split_linearization line 1252
  137. theorem OAI.SepticProfile.SourceSonic.aeval_prefP line 1261
  138. theorem OAI.SepticProfile.SourceSonic.aeval_denQuotP line 1263
  139. theorem OAI.SepticProfile.SourceSonic.aeval_transP line 1266
  140. theorem OAI.SepticProfile.SourceSonic.aeval_linP line 1269
  141. theorem OAI.SepticProfile.SourceSonic.aeval_residualP line 1273
  142. theorem OAI.SepticProfile.SourceSonic.aeval_real line 1279
  143. def OAI.SepticProfile.SourceSonic.sourceH line 1293
  144. theorem OAI.SepticProfile.SourceSonic.sourceH_analytic line 1298
  145. theorem OAI.SepticProfile.SourceSonic.sourceH_real line 1321
  146. theorem OAI.SepticProfile.SourceSonic.derivative_jet_add line 1340
  147. theorem OAI.SepticProfile.SourceSonic.exists_sonic_germ line 1348

    Source documentation

    A nonresonant analytic transonic germ for the normalized residual.

     theorem exists_sonic_germ (sigma kappa c s rho : ℝ)
    (hs : 2*(1-sigma)*s^2-(1-c)*(2*kappa+3)*s+3*(1-c)=0)
    (hd : 2*(1-sigma)*s ≠ 0)
    (hrho : rho*(2*(1-sigma)*s)=(1-c)*(2*kappa+3)-2*(1-sigma)*s)
    (hnr : ∀ n : ℕ, rho ≠ (n : ℝ)+2) :
    ∃ U : ℂ → ℂ, AnalyticAt ℂ U 0 ∧ U 0=1 ∧ deriv U 0=(s : ℂ) ∧
      (∀ x : ℝ, (U x).im=0) ∧
      ∀ᶠ z in 𝓝 (0 : ℂ),
        (1+z)*(1-(sigma : ℂ)*(1+z)^2)*(1-(U z)^2)*deriv U z =
          (1-(c : ℂ)*(U z)^2)*((kappa : ℂ)*(1+z)*(1-(U z)^2)+3*((1+z)-U z)) := by
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa

  148. theorem OAI.SepticProfile.SourceSonic.exists_real_sonic_germ line 1441
  149. def OAI.SepticProfile.SourceEuler.changeOfVariable line 1479
  150. def OAI.SepticProfile.SourceEuler.A line 1480
  151. def OAI.SepticProfile.SourceEuler.B line 1481
  152. def OAI.SepticProfile.SourceEuler.residual line 1483
  153. lemma OAI.SepticProfile.SourceEuler.derivative_changeOfVariable line 1487
  154. lemma OAI.SepticProfile.SourceEuler.transform_equation line 1494
  155. theorem OAI.SepticProfile.SourceEuler.exists_real_euler_germ line 1503
  156. def OAI.SepticProfile.ShootingParameters.leftEnd line 1550
  157. def OAI.SepticProfile.ShootingParameters.rightEnd line 1551
  158. def OAI.SepticProfile.ShootingParameters.a line 1553
  159. def OAI.SepticProfile.ShootingParameters.d line 1554
  160. def OAI.SepticProfile.ShootingParameters.e line 1555
  161. def OAI.SepticProfile.ShootingParameters.k line 1556
  162. def OAI.SepticProfile.ShootingParameters.beta line 1558
  163. def OAI.SepticProfile.ShootingParameters.q line 1559
  164. def OAI.SepticProfile.ShootingParameters.sigma line 1560
  165. def OAI.SepticProfile.ShootingParameters.kappa line 1561
  166. def OAI.SepticProfile.ShootingParameters.slope line 1562
  167. def OAI.SepticProfile.ShootingParameters.ratio line 1563
  168. theorem OAI.SepticProfile.ShootingParameters.rough_bounds line 1565
  169. theorem OAI.SepticProfile.ShootingParameters.a_pos line 1570
  170. theorem OAI.SepticProfile.ShootingParameters.d_pos line 1575
  171. theorem OAI.SepticProfile.ShootingParameters.e_pos line 1580
  172. theorem OAI.SepticProfile.ShootingParameters.k_pos line 1585
  173. theorem OAI.SepticProfile.ShootingParameters.parameter_identities line 1590
  174. theorem OAI.SepticProfile.ShootingParameters.sonic_quadratic line 1606
  175. theorem OAI.SepticProfile.ShootingParameters.ratio_bounds line 1615
  176. theorem OAI.SepticProfile.ShootingParameters.nonresonance line 1631
  177. theorem OAI.SepticProfile.ShootingParameters.beta_bounds line 1640
  178. theorem OAI.SepticProfile.ShootingParameters.sigma_bounds line 1656
  179. theorem OAI.SepticProfile.ShootingParameters.slope_pos line 1669
  180. theorem OAI.SepticProfile.ShootingParameters.sonic_divisor_ne line 1672
  181. theorem OAI.SepticProfile.ShootingParameters.ratio_identity line 1676
  182. theorem OAI.SepticProfile.ShootingParameters.standing_beta_bound line 1687
  183. theorem OAI.SepticProfile.ShootingParameters.shooting_coefficient_bounds line 1699
  184. abbrev OAI.SepticProfile.SonicJet.Series line 1735
  185. def OAI.SepticProfile.SonicJet.jet line 1737
  186. lemma OAI.SepticProfile.SonicJet.coeff_jet line 1739
  187. lemma OAI.SepticProfile.SonicJet.jet_congr line 1743
  188. lemma OAI.SepticProfile.SonicJet.jet_const line 1747
  189. lemma OAI.SepticProfile.SonicJet.jet_add line 1751
  190. lemma OAI.SepticProfile.SonicJet.jet_sub line 1757
  191. lemma OAI.SepticProfile.SonicJet.jet_mul line 1763
  192. lemma OAI.SepticProfile.SonicJet.jet_pow line 1773
  193. lemma OAI.SepticProfile.SonicJet.jet_deriv line 1781
  194. lemma OAI.SepticProfile.SonicJet.jet_id line 1787
  195. lemma OAI.SepticProfile.SonicJet.jet_z line 1797
  196. lemma OAI.SepticProfile.SonicJet.jet_zero line 1800
  197. def OAI.SepticProfile.SonicJet.z line 1803
  198. def OAI.SepticProfile.SonicJet.prefactor line 1804
  199. def OAI.SepticProfile.SonicJet.den line 1805
  200. def OAI.SepticProfile.SonicJet.r line 1806
  201. def OAI.SepticProfile.SonicJet.t line 1807
  202. def OAI.SepticProfile.SonicJet.residual line 1808
  203. def OAI.SepticProfile.SonicJet.profileResidual line 1811
  204. lemma OAI.SepticProfile.SonicJet.jet_residual line 1815
  205. lemma OAI.SepticProfile.SonicJet.residual_of_smooth_solution line 1825

    Source documentation

    Every smooth local solution supplies an exact formal jet solution, without assuming convergence of its Taylor expansion.

    lemma residual_of_smooth_solution (sigma kappa : ℝ) {f : ℝ → ℝ}
    (hf : ContDiffAt ℝ ∞ f 0)
    (heq : profileResidual sigma kappa f =ᶠ[𝓝 0] fun _ => 0) :
    residual sigma kappa (jet f) = 0 := by
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.SonicJet.profileResidual, OAI.SepticProfile.SonicJet.residual, OAI.SepticProfile.SonicJet.jet

  206. abbrev OAI.SepticProfile.EulerFormal.Series line 1837
  207. def OAI.SepticProfile.EulerFormal.A line 1839
  208. def OAI.SepticProfile.EulerFormal.B line 1840
  209. def OAI.SepticProfile.EulerFormal.pref line 1841
  210. def OAI.SepticProfile.EulerFormal.residual line 1842
  211. def OAI.SepticProfile.EulerFormal.profileResidual line 1846
  212. lemma OAI.SepticProfile.EulerFormal.jet_A line 1850
  213. lemma OAI.SepticProfile.EulerFormal.jet_B line 1855
  214. lemma OAI.SepticProfile.EulerFormal.jet_linear line 1860
  215. lemma OAI.SepticProfile.EulerFormal.jet_residual line 1863
  216. lemma OAI.SepticProfile.EulerFormal.residual_of_solution line 1872
  217. def OAI.SepticProfile.EulerFormal.p0 line 1879
  218. def OAI.SepticProfile.EulerFormal.p1 line 1880
  219. def OAI.SepticProfile.EulerFormal.p2 line 1881
  220. def OAI.SepticProfile.EulerFormal.p3 line 1882
  221. def OAI.SepticProfile.EulerFormal.i10 line 1884
  222. def OAI.SepticProfile.EulerFormal.i11 line 1885
  223. def OAI.SepticProfile.EulerFormal.i20 line 1886
  224. def OAI.SepticProfile.EulerFormal.i21 line 1887
  225. def OAI.SepticProfile.EulerFormal.i30 line 1888
  226. def OAI.SepticProfile.EulerFormal.i31 line 1889
  227. def OAI.SepticProfile.EulerFormal.i40 line 1890
  228. def OAI.SepticProfile.EulerFormal.i41 line 1891
  229. lemma OAI.SepticProfile.EulerFormal.pref_expansion line 1893
  230. lemma OAI.SepticProfile.EulerFormal.residual_expansion line 1901

    Source documentation

    This expansion is what the rational interval recurrence computes, including all cubic/quartic terms and the Euler factors.

    lemma residual_expansion (sigma kappa c h : ℝ) (w : Series) :
    residual sigma kappa c h (1+w) =
      -pref sigma h*(derivative (w^2)+C (1/3)*derivative (w^3))+
      C h*(-C (3*(1-c)*h)*X+
        (C (i10 kappa c h)+C (i11 kappa c h)*X)*w+
        (C (i20 kappa c h)+C (i21 kappa c h)*X)*w^2+
        (C (i30 kappa c h)+C (i31 kappa c h)*X)*w^3+
        (C (i40 kappa c h)+C (i41 kappa c h)*X)*w^4) := by
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.EulerFormal.Series, OAI.SepticProfile.EulerFormal.residual, OAI.SepticProfile.EulerFormal.pref, OAI.SepticProfile.EulerFormal.i10, OAI.SepticProfile.EulerFormal.i11, OAI.SepticProfile.EulerFormal.i20, OAI.SepticProfile.EulerFormal.i21, OAI.SepticProfile.EulerFormal.i30, OAI.SepticProfile.EulerFormal.i31, OAI.SepticProfile.EulerFormal.i40, OAI.SepticProfile.EulerFormal.i41

  231. lemma OAI.SepticProfile.EulerFormal.coeff_X_mul_derivative line 1923
  232. lemma OAI.SepticProfile.EulerFormal.coeff_pref_derivative line 1929
  233. lemma OAI.SepticProfile.EulerFormal.coeff_affine_mul line 1956
  234. lemma OAI.SepticProfile.EulerFormal.coefficient_equation line 1960
  235. lemma OAI.SepticProfile.EulerFormal.coeff_mul_Ico line 1988
  236. lemma OAI.SepticProfile.EulerFormal.coeff_square_low line 2007
  237. lemma OAI.SepticProfile.EulerFormal.coeff_square line 2017
  238. lemma OAI.SepticProfile.EulerFormal.coeff_cube line 2025
  239. lemma OAI.SepticProfile.EulerFormal.coeff_fourth line 2035
  240. lemma OAI.SepticProfile.EulerFormal.coeff_square_remainder line 2041
  241. structure OAI.SepticProfile.FixedInterval.Box line 2054
  242. def OAI.SepticProfile.FixedInterval.Holds line 2059
  243. def OAI.SepticProfile.FixedInterval.zero line 2062
  244. def OAI.SepticProfile.FixedInterval.neg line 2063
  245. def OAI.SepticProfile.FixedInterval.add line 2064
  246. def OAI.SepticProfile.FixedInterval.sub line 2065
  247. def OAI.SepticProfile.FixedInterval.grow line 2066
  248. def OAI.SepticProfile.FixedInterval.scale line 2067
  249. def OAI.SepticProfile.FixedInterval.mul line 2069
  250. def OAI.SepticProfile.FixedInterval.ofRat line 2073
  251. lemma OAI.SepticProfile.FixedInterval.radius_nonneg line 2075
  252. lemma OAI.SepticProfile.FixedInterval.quotient_bounds line 2078
  253. lemma OAI.SepticProfile.FixedInterval.rounding_bound line 2085
  254. lemma OAI.SepticProfile.FixedInterval.holds_zero line 2093
  255. lemma OAI.SepticProfile.FixedInterval.holds_neg line 2094
  256. lemma OAI.SepticProfile.FixedInterval.holds_add line 2103
  257. lemma OAI.SepticProfile.FixedInterval.holds_sub line 2112
  258. lemma OAI.SepticProfile.FixedInterval.holds_scale line 2116
  259. lemma OAI.SepticProfile.FixedInterval.holds_mul line 2146
  260. lemma OAI.SepticProfile.FixedInterval.holds_ofRat line 2195
  261. def OAI.SepticProfile.FixedInterval.treeSumBox line 2216
  262. lemma OAI.SepticProfile.FixedInterval.holds_treeSumBox line 2220
  263. def OAI.SepticProfile.FixedInterval.sumBox line 2237
  264. lemma OAI.SepticProfile.FixedInterval.holds_sumBox line 2240
  265. def OAI.SepticProfile.FixedInterval.convBox line 2260
  266. lemma OAI.SepticProfile.FixedInterval.holds_convBox line 2263
  267. lemma OAI.SepticProfile.FixedInterval.holds_exact line 2272
  268. lemma OAI.SepticProfile.FixedInterval.holds_enlarge line 2275
  269. def OAI.SepticProfile.FixedInterval.rscale line 2288
  270. def OAI.SepticProfile.FixedInterval.ratBox line 2290
  271. lemma OAI.SepticProfile.FixedInterval.holds_rscale line 2292
  272. lemma OAI.SepticProfile.FixedInterval.holds_ratBox line 2297
  273. structure OAI.SepticProfile.JetTrace.Parameters line 2307
  274. structure OAI.SepticProfile.JetTrace.Trace line 2310
  275. def OAI.SepticProfile.JetTrace.linear line 2313
  276. def OAI.SepticProfile.JetTrace.stepBox line 2315
  277. def OAI.SepticProfile.JetTrace.stepValue line 2327
  278. lemma OAI.SepticProfile.JetTrace.holds_stepBox line 2336
  279. structure OAI.SepticProfile.JetTrace.Valid line 2371
  280. theorem OAI.SepticProfile.JetTrace.coefficients_enclosed line 2390

    Source documentation

    Soundness of the finite integer trace. Its hypotheses are arithmetic identities checked from the data and the exact coefficient recurrence; no profile or endpoint inequality is assumed.

    theorem coefficients_enclosed {Q : ℤ} (hQ : 0<Q) (D N : ℕ) (hN : N+1≤2^D)
    (p : Parameters) (t : Trace) (ht : Valid Q D N p t)
    (w b c d br : ℕ → ℝ) (hw0 : w 0=0) (hw1 : w 1=(p.a : ℝ))
    (hb : ∀ j, b j=∑ i ∈ Ico 1 j, w i*w (j-i))
    (hc : ∀ j, c j=∑ i ∈ Ico 1 (j-1), w i*b (j-i))
    (hd : ∀ j, d j=∑ i ∈ Ico 2 (j-1), b i*b (j-i))
    (hbr : ∀ j, br j=∑ i ∈ Ico 2 j, w i*w (j+1-i))
    (he : ∀ j, 2≤j → j≤N → (linear p j : ℝ)*w j+stepValue p w b c d br j=0) :
    ∀ j≤N, Holds Q (t.w j) (w j) := by
…

    Mentions: OAI.SepticProfile.JetTrace.Parameters, OAI.SepticProfile.JetTrace.Trace, OAI.SepticProfile.JetTrace.Valid, OAI.SepticProfile.JetTrace.linear, OAI.SepticProfile.JetTrace.stepValue

  281. def OAI.SepticProfile.JetTrace.sourceParams line 2459
  282. lemma OAI.SepticProfile.JetTrace.source_recurrence line 2475
  283. theorem OAI.SepticProfile.JetTrace.source_coefficients_enclosed line 2496
  284. lemma OAI.SepticProfile.EulerFormal.residual_direct line 2519
  285. lemma OAI.SepticProfile.EulerFormal.coeff_B_mul line 2534
  286. lemma OAI.SepticProfile.EulerFormal.coeff_A_mul line 2538
  287. lemma OAI.SepticProfile.EulerFormal.coeff_B_high line 2542
  288. lemma OAI.SepticProfile.EulerFormal.residual_coeff_direct line 2545
  289. lemma OAI.SepticProfile.EulerFormal.residual_congr_X_pow line 2568

    Source documentation

    Tangency of the sonic vector-field divisor prevents loss of one order in its residual. This is the reason finite jets suffice for the barrier.

    lemma residual_congr_X_pow (sigma kappa c h : ℝ) (u v : Series) (m : ℕ)
    (hm : 1  ≤  m) (hu0 : coeff 0 u=1) (hdiv : X^m  ∣  u-v) :
    X^m  ∣  residual sigma kappa c h u-residual sigma kappa c h v := by
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.EulerFormal.Series, OAI.SepticProfile.EulerFormal.residual

  290. lemma OAI.SepticProfile.FixedInterval.coeff_mul_support line 2619
  291. lemma OAI.SepticProfile.FixedInterval.coeff_mul_support_zero line 2637
  292. lemma OAI.SepticProfile.FixedInterval.holds_poly_conv line 2644
  293. structure OAI.SepticProfile.BarrierTrace.Parameters line 2660
  294. def OAI.SepticProfile.BarrierTrace.sourceParams line 2663
  295. structure OAI.SepticProfile.BarrierTrace.Trace line 2676
  296. def OAI.SepticProfile.BarrierTrace.residualBox line 2679
  297. lemma OAI.SepticProfile.BarrierTrace.residual_enclosed line 2691
  298. lemma OAI.SepticProfile.FixedInterval.holds_change_scale line 2728
  299. lemma OAI.SepticProfile.FixedInterval.bounds line 2737
  300. lemma OAI.SepticProfile.FixedInterval.abs_bound line 2743
  301. structure OAI.SepticProfile.BarrierTrace.ValidPowers line 2755
  302. lemma OAI.SepticProfile.BarrierTrace.powers_enclosed line 2763
  303. def OAI.SepticProfile.EulerPolynomial.residual line 2805
  304. lemma OAI.SepticProfile.EulerPolynomial.coe_residual line 2809
  305. lemma OAI.SepticProfile.EulerPolynomial.eval_residual line 2817
  306. lemma OAI.SepticProfile.EulerPolynomial.degree_residual line 2822
  307. def OAI.SepticProfile.EulerPolynomial.barrier line 2829
  308. lemma OAI.SepticProfile.EulerPolynomial.coeff_barrier line 2832
  309. lemma OAI.SepticProfile.EulerPolynomial.degree_barrier line 2839
  310. lemma OAI.SepticProfile.EulerPolynomial.barrier_congr line 2846
  311. lemma OAI.SepticProfile.EulerPolynomial.residual_lowzero line 2853
  312. lemma OAI.SepticProfile.EulerPolynomial.eval_factor line 2862
  313. def OAI.SepticProfile.FixedInterval.treeInt line 2883
  314. lemma OAI.SepticProfile.FixedInterval.treeInt_eq line 2887
  315. def OAI.SepticProfile.FixedInterval.sumInt line 2899
  316. lemma OAI.SepticProfile.FixedInterval.sumInt_eq line 2902
  317. def OAI.SepticProfile.FixedInterval.absTail line 2913
  318. lemma OAI.SepticProfile.FixedInterval.scaled_tail_bound line 2916
  319. lemma OAI.SepticProfile.FixedInterval.quad_lower line 2948
  320. lemma OAI.SepticProfile.FixedInterval.finite_positive line 2956

    Source documentation

    Finite, exact positivity criterion used by the sonic residual certificate. The tail is bounded absolutely, not numerically sampled.

    lemma finite_positive {Q : ℤ} (hQ : 0<Q) (D M : ℕ) (hM : 10 ≤ M) (hD : M ≤ 2^D)
    (b : ℕ → Box) (a : ℕ → ℝ)
    (ha : ∀ i<M, Holds Q (b i) (a i))
    (L0 L1 L2 : ℝ) (h0 : L0 ≤ a 0) (h1 : L1 ≤ a 1) (h2 : L2 ≤ a 2)
    (hmid : ∀ i, 3 ≤ i → i<10 → (b i).radius ≤ (b i).center)
    (hL2 : 0 ≤ L2) (hder : L1+2*(5/6)*L2 ≤ 0)
    (hh : 4/100000000 ≤ L0+L1*(5/6)+L2*(5/6)^2)
    (htail : 100000000*absTail D 10 M b<Q*6^(M-1))
    {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 5/6) : 0<∑ i ∈ range M, a i*x^i := by
…

    Mentions: OAI.SepticProfile.FixedInterval.Box, OAI.SepticProfile.FixedInterval.Holds, OAI.SepticProfile.radius, OAI.SepticProfile.FixedInterval.absTail

  321. lemma OAI.SepticProfile.EulerPolynomial.eval_add_monomial line 3002
  322. lemma OAI.SepticProfile.EulerPolynomial.eval_barrier line 3008
  323. lemma OAI.SepticProfile.EulerPolynomial.taylor_jet_littleO line 3013
  324. lemma OAI.SepticProfile.EulerPolynomial.exists_barrier_entry line 3038

    Source documentation

    The barriers enter on the correct sides of the actual analytic sonic solution. No numerical assumption about the omitted Taylor tail is needed.

    lemma exists_barrier_entry (f : ℝ → ℝ) (hf : ContDiffAt ℝ 220 f 0)
    (δ : ℝ) (hδ : 0<δ) :
    ∀ᶠ x in 𝓝 (0 : ℝ), 0<x →
      (barrier (SonicJet.jet f) (-δ)).eval x<f x ∧
        f x<(barrier (SonicJet.jet f) δ).eval x := by
…

    Mentions: OAI.SepticProfile.EulerPolynomial.barrier, OAI.SepticProfile.SonicJet.jet

  325. lemma OAI.SepticProfile.FixedInterval.tail_unscaled_bound line 3066
  326. lemma OAI.SepticProfile.FixedInterval.finite_velocity_range line 3085
  327. lemma OAI.SepticProfile.EulerPolynomial.eval_shift_one line 3124
  328. lemma OAI.SepticProfile.EulerPolynomial.polynomial_velocity_range line 3135
  329. def OAI.SepticProfile.RegularContinuation.clamp line 3160

    Source documentation

    Projection to a closed scalar interval. It is used only away from the source singularities, and is proved inactive by exact comparison barriers.

    def clamp (c d x : ℝ) : ℝ := max (min x d) c
  330. lemma OAI.SepticProfile.RegularContinuation.clamp_mem line 3162
  331. lemma OAI.SepticProfile.RegularContinuation.clamp_eq line 3165
  332. lemma OAI.SepticProfile.RegularContinuation.clamp_lipschitz line 3168
  333. theorem OAI.SepticProfile.RegularContinuation.exists_clamped_solution line 3173

    Source documentation

    An ordinary (nonsingular) ODE on a compact rectangle has a clamped solution on the entire time interval. No singular-point continuation is imported here.

    theorem exists_clamped_solution {a b c d : ℝ} (hab : a≤b) (hcd : c≤d)
    {f : ℝ×ℝ → ℝ} (hf : ContDiffOn ℝ 1 f (Icc a b ×ˢ Icc c d)) (u0 : ℝ) :
    ∃ u : ℝ → ℝ, u a=u0 ∧ ContinuousOn u (Icc a b) ∧
      ∀ t ∈ Icc a b, HasDerivWithinAt u (f (t,clamp c d (u t))) (Icc a b) t := by
…

    Mentions: OAI.SepticProfile.RegularContinuation.clamp

  334. theorem OAI.SepticProfile.RegularContinuation.exists_between_strict_barriers line 3216

    Source documentation

    A compact nonsingular scalar ODE is continued between verified strict barriers. The integrator is constructed, rather than assumed.

    theorem exists_between_strict_barriers {a b c d u0 : ℝ} (hab : a≤b) (hcd : c≤d)
    {f : ℝ×ℝ → ℝ} (hf : ContDiffOn ℝ 1 f (Icc a b ×ˢ Icc c d))
    (lo hi dlo dhi : ℝ → ℝ)
    (hloder : ∀ t ∈ Icc a b, HasDerivAt lo (dlo t) t)
    (hhider : ∀ t ∈ Icc a b, HasDerivAt hi (dhi t) t)
    (hlorange : ∀ t ∈ Icc a b, lo t ∈ Icc c d)
    (hhirange : ∀ t ∈ Icc a b, hi t ∈ Icc c d)
    (hlostrict : ∀ t ∈ Icc a b, dlo t<f (t,lo t))
    (hhistrict : ∀ t ∈ Icc a b, f (t,hi t)<dhi t)
    (hu0 : u0 ∈ Icc (lo a) (hi a)) :
    ∃ u : ℝ → ℝ, u a=u0 ∧ ContinuousOn u (Icc a b) ∧
      (∀ t ∈ Icc a b, u t ∈ Icc (lo t) (hi t)) ∧
…
  335. def OAI.SepticProfile.EulerContinuation.D line 3268
  336. def OAI.SepticProfile.EulerContinuation.N line 3270
  337. lemma OAI.SepticProfile.EulerContinuation.D_pos line 3274
  338. lemma OAI.SepticProfile.EulerContinuation.field_contDiffOn line 3283
  339. lemma OAI.SepticProfile.EulerContinuation.residual_eq line 3292
  340. theorem OAI.SepticProfile.EulerContinuation.exists_between_polynomials line 3300

    Source documentation

    Genuine regular continuation of the sonic Euler equation from a>0 to 5/6, provided the two polynomial residual certificates are supplied.

    theorem exists_between_polynomials {sigma kappa a u0 : ℝ} (hs : sigma<1)
    (ha : 0<a) (ha' : a≤5/6) (p q : ℝ[X])
    (hrangep : ∀ t ∈ Icc 0 (5/6), 1-t/50≤p.eval t ∧ p.eval t≤1-t/500)
    (hrangeq : ∀ t ∈ Icc 0 (5/6), 1-t/50≤q.eval t ∧ q.eval t≤1-t/500)
    (hresp : ∀ t ∈ Ioc 0 (5/6),
      EulerFormal.profileResidual sigma kappa (3/5) (1/500) (fun x => p.eval x) t<0)
    (hresq : ∀ t ∈ Ioc 0 (5/6),
      0<EulerFormal.profileResidual sigma kappa (3/5) (1/500) (fun x => q.eval x) t)
    (hu0 : u0 ∈ Icc (p.eval a) (q.eval a)) :
    ∃ u : ℝ → ℝ, u a=u0 ∧ ContinuousOn u (Icc a (5/6)) ∧
      (∀ t ∈ Icc a (5/6), p.eval t≤u t ∧ u t≤q.eval t) ∧
      ∀ t ∈ Icc a (5/6), HasDerivWithinAt u
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.q, OAI.SepticProfile.EulerFormal.profileResidual