OAI/Analysis/BernoulliCone/LowerSupport.lean

GitHub source file

169 declarations, 0 contain sorry, 0 declared as axioms

The concrete seven-dimensional cone belonging to the De Silva–Jerison profile. These are actual function/Sobolev constructions, not an assumption of minimality.

  1. def OAI.Bernoulli.DeSilvaJerison.A line 18

    Source documentation

    Half the logarithmic ratio; it is artanh on (-1,1).

    def A (t : ℝ) : ℝ := (Real.log (1+t) - Real.log (1-t))/2
  2. def OAI.Bernoulli.DeSilvaJerison.f line 21

    Source documentation

    The even solution of (1-t²)f''-6tf'+6f=0 with f(0)=1.

    def f (t : ℝ) : ℝ :=
…
  3. def OAI.Bernoulli.DeSilvaJerison.fp line 25

    Source documentation

    A convenient rational-logarithmic expression for f'.

    def fp (t : ℝ) : ℝ :=
…
  4. lemma OAI.Bernoulli.DeSilvaJerison.A_neg line 28
  5. lemma OAI.Bernoulli.DeSilvaJerison.A_zero line 32
  6. lemma OAI.Bernoulli.DeSilvaJerison.f_zero line 33
  7. lemma OAI.Bernoulli.DeSilvaJerison.fp_zero line 34
  8. lemma OAI.Bernoulli.DeSilvaJerison.f_neg line 36
  9. lemma OAI.Bernoulli.DeSilvaJerison.A_eq_half_log line 40
  10. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_A line 46
  11. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_f line 57
  12. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_fp line 70
  13. lemma OAI.Bernoulli.DeSilvaJerison.f_relation line 82
  14. theorem OAI.Bernoulli.DeSilvaJerison.profile_equation line 90

    Source documentation

    The profile satisfies the differential equation (1-t²)f''-6tf'+6f=0.

    theorem profile_equation {t : ℝ} (ht : t ∈ Ioo (-1 : ℝ) 1) :
    (1-t^2) * deriv (deriv f) t - 6*t*deriv f t + 6*f t = 0 := by
…

    Mentions: OAI.Bernoulli.DeSilvaJerison.f

  15. lemma OAI.Bernoulli.DeSilvaJerison.A_nonneg line 101
  16. lemma OAI.Bernoulli.DeSilvaJerison.fp_neg line 105
  17. lemma OAI.Bernoulli.DeSilvaJerison.f_strictAnti line 115
  18. lemma OAI.Bernoulli.DeSilvaJerison.f_lower_pos line 125

    Source documentation

    A certified enclosure, replacing the decimal root in the preprint.

    lemma f_lower_pos : 0 < f (517330/1000000) := by
…

    Mentions: OAI.Bernoulli.DeSilvaJerison.f

  19. lemma OAI.Bernoulli.DeSilvaJerison.f_upper_neg line 134
  20. lemma OAI.Bernoulli.DeSilvaJerison.exists_profile_root line 143
  21. def OAI.Bernoulli.DeSilvaJerison.t7 line 152

    Source documentation

    The first positive root t₇ of the normalized profile.

    def t7 : ℝ := exists_profile_root.choose
  22. lemma OAI.Bernoulli.DeSilvaJerison.t7_bounds line 154
  23. lemma OAI.Bernoulli.DeSilvaJerison.f_t7 line 157
  24. lemma OAI.Bernoulli.DeSilvaJerison.t7_pos line 159
  25. lemma OAI.Bernoulli.DeSilvaJerison.t7_lt_one line 160
  26. lemma OAI.Bernoulli.DeSilvaJerison.f_pos_of_abs_lt line 162
  27. lemma OAI.Bernoulli.DeSilvaJerison.root_unique line 171
  28. lemma OAI.Bernoulli.DeSilvaJerison.fp_t7 line 174
  29. def OAI.Bernoulli.DeSilvaJerison.c7 line 183

    Source documentation

    The square of the normal derivative of the unscaled conical function.

    def c7 : ℝ := (1-t7^2) * (fp t7)^2

    Mentions: OAI.Bernoulli.DeSilvaJerison.t7, OAI.Bernoulli.DeSilvaJerison.fp

  30. lemma OAI.Bernoulli.DeSilvaJerison.c7_pos line 185
  31. lemma OAI.Bernoulli.DeSilvaJerison.c7_eq line 189
  32. lemma OAI.Bernoulli.DeSilvaJerison.contDiffAt_f line 195
  33. def OAI.Bernoulli.DeSilvaJerison.p line 206

    Source documentation

    Extend the positive spherical profile by zero outside its first two roots.

    def p (t : ℝ) : ℝ := f (min |t| t7)

    Mentions: OAI.Bernoulli.DeSilvaJerison.f, OAI.Bernoulli.DeSilvaJerison.t7

  34. lemma OAI.Bernoulli.DeSilvaJerison.f_abs line 208
  35. lemma OAI.Bernoulli.DeSilvaJerison.p_eq_f line 213
  36. lemma OAI.Bernoulli.DeSilvaJerison.p_eq_zero line 216
  37. lemma OAI.Bernoulli.DeSilvaJerison.p_neg line 219
  38. lemma OAI.Bernoulli.DeSilvaJerison.p_zero line 220
  39. lemma OAI.Bernoulli.DeSilvaJerison.p_pos_iff line 222
  40. lemma OAI.Bernoulli.DeSilvaJerison.p_nonneg line 232
  41. lemma OAI.Bernoulli.DeSilvaJerison.p_le_one line 237
  42. lemma OAI.Bernoulli.DeSilvaJerison.exists_lipschitz_p line 243
  43. def OAI.Bernoulli.DeSilvaJerison.κ line 259

    Source documentation

    The normalization imposed by the Bernoulli condition.

    def κ : ℝ := (Real.sqrt c7)⁻¹

    Mentions: OAI.Bernoulli.DeSilvaJerison.c7

  44. lemma OAI.Bernoulli.DeSilvaJerison.κ_pos line 261
  45. lemma OAI.Bernoulli.DeSilvaJerison.κ_sq line 262
  46. def OAI.Bernoulli.DeSilvaJerison.Z line 273

    Source documentation

    The homogeneous, nonnegative profile, prior to normalizing its boundary slope.

    def Z (x : Space 7) : ℝ := ‖x‖ * p (x 6 / ‖x‖)

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.p

  47. def OAI.Bernoulli.DeSilvaJerison.U line 275
  48. lemma OAI.Bernoulli.DeSilvaJerison.Z_zero line 277
  49. lemma OAI.Bernoulli.DeSilvaJerison.U_zero line 278
  50. lemma OAI.Bernoulli.DeSilvaJerison.Z_nonneg line 279
  51. lemma OAI.Bernoulli.DeSilvaJerison.U_nonneg line 280
  52. lemma OAI.Bernoulli.DeSilvaJerison.Z_le_norm line 281
  53. lemma OAI.Bernoulli.DeSilvaJerison.U_even line 284
  54. lemma OAI.Bernoulli.DeSilvaJerison.coordinate_le_norm line 287
  55. lemma OAI.Bernoulli.DeSilvaJerison.angular_estimate line 290
  56. lemma OAI.Bernoulli.DeSilvaJerison.exists_lipschitz_Z line 316
  57. lemma OAI.Bernoulli.DeSilvaJerison.exists_lipschitz_U line 349
  58. lemma OAI.Bernoulli.DeSilvaJerison.U_continuous line 353
  59. theorem OAI.Bernoulli.DeSilvaJerison.U_h1loc line 355
  60. lemma OAI.Bernoulli.DeSilvaJerison.U_smul line 360
  61. theorem OAI.Bernoulli.DeSilvaJerison.U_homogeneous line 365
  62. lemma OAI.Bernoulli.DeSilvaJerison.U_of_coordinate_zero line 370

    Source documentation

    Values in every direction perpendicular to the symmetry axis are positive.

    lemma U_of_coordinate_zero {x : Space 7} (hx : x 6=0) : U x = κ*‖x‖ := by
…

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.DeSilvaJerison.κ

  63. theorem OAI.Bernoulli.DeSilvaJerison.U_nonzero line 373
  64. theorem OAI.Bernoulli.DeSilvaJerison.U_not_flat line 383
  65. lemma OAI.Bernoulli.Axisymmetric.hasDerivAt_radius line 405
  66. lemma OAI.Bernoulli.Axisymmetric.hasDerivAt_axis line 415
  67. def OAI.Bernoulli.Axisymmetric.lift line 422

    Source documentation

    Lift of a polar profile; values at the origin use the usual total operations.

    def lift (e : E) (α : ℝ) (φ : ℝ → ℝ) (x : E) : ℝ :=
…
  68. lemma OAI.Bernoulli.Axisymmetric.hasDerivAt_angular line 425
  69. lemma OAI.Bernoulli.Axisymmetric.hasDerivAt_lift_line line 433
  70. def OAI.Bernoulli.Axisymmetric.lineFirst line 451

    Source documentation

    The explicit first derivative along a line, used to avoid assuming an ODE or a second derivative in the Euclidean Laplacian computation.

    def lineFirst (e x v : E) (α : ℝ) (φ φ₁ : ℝ → ℝ) (t : ℝ) : ℝ :=
…
  71. lemma OAI.Bernoulli.Axisymmetric.hasDerivAt_lineFirst line 458
  72. def OAI.Bernoulli.Axisymmetric.secondCoeff line 496

    Source documentation

    Scalar diagonal Hessian coefficient in a unit radial/angular frame.

    def secondCoeff (α F F₁ F₂ s p b n : ℝ) : ℝ :=
…
  73. lemma OAI.Bernoulli.Axisymmetric.secondCoeff_sum line 500
  74. lemma OAI.Bernoulli.Axisymmetric.contDiffAt_lift line 516
  75. lemma OAI.Bernoulli.Axisymmetric.lift_line_second line 524
  76. lemma OAI.Bernoulli.Axisymmetric.line_second_derivative line 548
  77. lemma OAI.Bernoulli.Axisymmetric.laplacian_lift line 567
  78. def OAI.Bernoulli.Axisymmetric.radial line 604

    Source documentation

    The radial unit vector (at nonzero points) and the tangential polar direction.

    def radial (x : E) : E := ‖x‖⁻¹ • x
  79. def OAI.Bernoulli.Axisymmetric.polarGradient line 606
  80. lemma OAI.Bernoulli.Axisymmetric.radial_norm line 609
  81. lemma OAI.Bernoulli.Axisymmetric.radial_inner line 612
  82. lemma OAI.Bernoulli.Axisymmetric.norm_sq_polarGradient line 615
  83. lemma OAI.Bernoulli.Axisymmetric.hasGradientAt_lift line 627
  84. lemma OAI.Bernoulli.Axisymmetric.gradient_lift_norm_sq line 655
  85. def OAI.Bernoulli.DeSilvaJerison.axis line 670
  86. def OAI.Bernoulli.DeSilvaJerison.angle line 672
  87. lemma OAI.Bernoulli.DeSilvaJerison.axis_norm line 674
  88. lemma OAI.Bernoulli.DeSilvaJerison.inner_axis line 675
  89. lemma OAI.Bernoulli.DeSilvaJerison.angle_contDiffAt line 678
  90. lemma OAI.Bernoulli.DeSilvaJerison.U_pos_iff line 686
  91. def OAI.Bernoulli.DeSilvaJerison.Zsigned line 696

    Source documentation

    Smooth signed extension near the free boundary away from the singular axis.

    def Zsigned : Space 7 → ℝ := lift axis 1 f

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.DeSilvaJerison.f

  92. def OAI.Bernoulli.DeSilvaJerison.Usigned line 698
  93. lemma OAI.Bernoulli.DeSilvaJerison.Zsigned_eq line 700
  94. lemma OAI.Bernoulli.DeSilvaJerison.Z_eq_Zsigned line 703
  95. lemma OAI.Bernoulli.DeSilvaJerison.U_eq_Usigned line 707
  96. lemma OAI.Bernoulli.DeSilvaJerison.signed_contDiffAt line 711
  97. lemma OAI.Bernoulli.DeSilvaJerison.signed_laplacian line 716
  98. lemma OAI.Bernoulli.DeSilvaJerison.signed_harmonicAt line 736
  99. lemma OAI.Bernoulli.DeSilvaJerison.U_eventuallyEq_Usigned line 745
  100. theorem OAI.Bernoulli.DeSilvaJerison.U_harmonic line 752

    Source documentation

    Positive-phase harmonicity is proved for the actual Sobolev candidate.

    theorem U_harmonic : HarmonicOnNhd U {x|0<U x} := by
…

    Mentions: OAI.Bernoulli.DeSilvaJerison.U

  101. lemma OAI.Bernoulli.DeSilvaJerison.fp_neg_arg line 758
  102. lemma OAI.Bernoulli.DeSilvaJerison.f_zero_at_boundary line 762
  103. lemma OAI.Bernoulli.DeSilvaJerison.fp_sq_at_boundary line 765
  104. lemma OAI.Bernoulli.DeSilvaJerison.signed_gradient_norm_sq line 773
  105. lemma OAI.Bernoulli.DeSilvaJerison.Zsigned_boundary_slope line 780

    Source documentation

    Exact slope-squared c7 on the boundary of the unnormalized cone.

    lemma Zsigned_boundary_slope {x : Space 7} (hx : x≠0) (ha : |angle x|=t7) :
    ‖gradient Zsigned x‖^2=c7 := by
…

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.angle, OAI.Bernoulli.DeSilvaJerison.t7, OAI.Bernoulli.DeSilvaJerison.Zsigned, OAI.Bernoulli.DeSilvaJerison.c7

  106. lemma OAI.Bernoulli.DeSilvaJerison.gradient_const_mul line 787
  107. theorem OAI.Bernoulli.DeSilvaJerison.Usigned_boundary_slope line 795

    Source documentation

    The actual signed extension has exactly unit normal slope at every nonvertex free-boundary point. This does not claim its energy comparison.

    theorem Usigned_boundary_slope {x : Space 7} (hx : x≠0) (ha : |angle x|=t7) :
    ‖gradient Usigned x‖=1 := by
…

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.angle, OAI.Bernoulli.DeSilvaJerison.t7, OAI.Bernoulli.DeSilvaJerison.Usigned

  108. def OAI.Bernoulli.DeSilvaJerison.B line 809
  109. lemma OAI.Bernoulli.DeSilvaJerison.B_nonneg line 811
  110. lemma OAI.Bernoulli.DeSilvaJerison.odd_sum_eq line 816
  111. lemma OAI.Bernoulli.DeSilvaJerison.A_series_bounds line 824
  112. lemma OAI.Bernoulli.DeSilvaJerison.f_series_lower line 836
  113. lemma OAI.Bernoulli.DeSilvaJerison.fp_series_upper line 845
  114. def OAI.Bernoulli.DeSilvaJerison.Algebra.g line 858
  115. def OAI.Bernoulli.DeSilvaJerison.Algebra.g1 line 860
  116. def OAI.Bernoulli.DeSilvaJerison.Algebra.g2 line 862
  117. def OAI.Bernoulli.DeSilvaJerison.Algebra.FlowNum line 864
  118. def OAI.Bernoulli.DeSilvaJerison.Algebra.JlowNum line 866
  119. def OAI.Bernoulli.DeSilvaJerison.Algebra.H line 868
  120. def OAI.Bernoulli.DeSilvaJerison.Algebra.bern line 873
  121. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.identity line 910
  122. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.bern_nonneg line 914
  123. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.H_nonneg line 919
  124. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.hasDerivAt_g line 927
  125. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.hasDerivAt_g1 line 933
  126. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.g_ge_one line 939
  127. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.g1_nonneg line 944
  128. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.g_residual_nonpos line 946
  129. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.lower_logder line 955
  130. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.upper_logder line 967
  131. lemma OAI.Bernoulli.DeSilvaJerison.Algebra.FlowNum_nonneg line 979
  132. def OAI.Bernoulli.DeSilvaJerison.gSub line 995
  133. def OAI.Bernoulli.DeSilvaJerison.gSub1 line 996
  134. def OAI.Bernoulli.DeSilvaJerison.gSub2 line 997
  135. def OAI.Bernoulli.DeSilvaJerison.qSub line 998
  136. lemma OAI.Bernoulli.DeSilvaJerison.gSub_pos line 1000
  137. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_gSub line 1005
  138. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_gSub1 line 1012
  139. lemma OAI.Bernoulli.DeSilvaJerison.gSub_residual line 1020
  140. lemma OAI.Bernoulli.DeSilvaJerison.qSub_nonneg line 1026
  141. lemma OAI.Bernoulli.DeSilvaJerison.qSub_bounds line 1030
  142. lemma OAI.Bernoulli.DeSilvaJerison.c7_upper line 1048
  143. lemma OAI.Bernoulli.DeSilvaJerison.fp_strictAnti line 1060
  144. lemma OAI.Bernoulli.DeSilvaJerison.sub_endpoint_bounds line 1070
  145. def OAI.Bernoulli.DeSilvaJerison.GSub line 1082

    Source documentation

    The free-boundary gradient numerator for the explicit lower barrier.

    def GSub (t:ℝ) : ℝ := (1-(-643/200:ℝ))^2*(f t)^2+
…

    Mentions: OAI.Bernoulli.DeSilvaJerison.f

  146. def OAI.Bernoulli.DeSilvaJerison.FLo line 1085
  147. def OAI.Bernoulli.DeSilvaJerison.JLo line 1086
  148. lemma OAI.Bernoulli.DeSilvaJerison.FLo_le line 1088
  149. lemma OAI.Bernoulli.DeSilvaJerison.fp_le_JLo line 1096
  150. lemma OAI.Bernoulli.DeSilvaJerison.JLo_nonneg line 1105
  151. lemma OAI.Bernoulli.DeSilvaJerison.GSub_low line 1116
  152. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_qSub line 1147
  153. lemma OAI.Bernoulli.DeSilvaJerison.qSub_deriv_bound line 1154
  154. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_GSub line 1168
  155. lemma OAI.Bernoulli.DeSilvaJerison.GSub_nonpos_deriv line 1179
  156. lemma OAI.Bernoulli.DeSilvaJerison.GSub_high line 1214
  157. theorem OAI.Bernoulli.DeSilvaJerison.GSub_ge_c7 line 1231

    Source documentation

    Exact substitute for DSJ's numerical lower-barrier plot in dimension seven.

    theorem GSub_ge_c7 {t:ℝ} (ht:0≤t) (ht7:t≤t7) : c7≤GSub t := by
…

    Mentions: OAI.Bernoulli.DeSilvaJerison.t7, OAI.Bernoulli.DeSilvaJerison.c7, OAI.Bernoulli.DeSilvaJerison.GSub

  158. lemma OAI.Bernoulli.DeSilvaJerison.qSub_neg line 1242
  159. lemma OAI.Bernoulli.DeSilvaJerison.GSub_neg line 1246
  160. lemma OAI.Bernoulli.DeSilvaJerison.GSub_ge_c7_abs line 1250
  161. lemma OAI.Bernoulli.DeSilvaJerison.gSub_contDiff line 1256
  162. def OAI.Bernoulli.DeSilvaJerison.YSub line 1261

    Source documentation

    Positive superharmonic ground state used by the lower comparison.

    def YSub : Space 7 → ℝ := lift axis (-643/200) gSub

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.DeSilvaJerison.gSub

  163. lemma OAI.Bernoulli.DeSilvaJerison.YSub_pos line 1263
  164. lemma OAI.Bernoulli.DeSilvaJerison.YSub_contDiffAt line 1267
  165. theorem OAI.Bernoulli.DeSilvaJerison.YSub_superharmonic line 1271

    Source documentation

    An actual sign of the Euclidean Laplacian, not a barrier hypothesis.

    theorem YSub_superharmonic {x:Space 7} (hx:x≠0) : Δ YSub x≤0 := by
…

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.YSub

  166. lemma OAI.Bernoulli.DeSilvaJerison.Usigned_gradient line 1286
  167. lemma OAI.Bernoulli.DeSilvaJerison.YSub_gradient line 1295
  168. lemma OAI.Bernoulli.DeSilvaJerison.U_gradient line 1301
  169. theorem OAI.Bernoulli.DeSilvaJerison.lower_groundstate_slope line 1311

    Source documentation

    The square-completion vector of the lower comparison has norm at least one throughout the entire positive phase of the concrete seven-dimensional cone.

    theorem lower_groundstate_slope {x:Space 7} (hu:0<U x) :
    1≤‖gradient U x-(U x/YSub x) • gradient YSub x‖^2 := by
…

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.DeSilvaJerison.YSub