OAI/Analysis/BernoulliCone/UpperSupport.lean

GitHub source file

169 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Bernoulli.DeSilvaJerison.UpperAlgebra.flo line 10
  2. def OAI.Bernoulli.DeSilvaJerison.UpperAlgebra.fhi line 12
  3. def OAI.Bernoulli.DeSilvaJerison.UpperAlgebra.numerator line 14
  4. def OAI.Bernoulli.DeSilvaJerison.UpperAlgebra.denominator line 16
  5. def OAI.Bernoulli.DeSilvaJerison.UpperAlgebra.bern_lo line 17
  6. lemma OAI.Bernoulli.DeSilvaJerison.UpperAlgebra.identity_lo line 39
  7. lemma OAI.Bernoulli.DeSilvaJerison.UpperAlgebra.bound_lo line 44
  8. def OAI.Bernoulli.DeSilvaJerison.UpperAlgebra.bern_hi line 57
  9. lemma OAI.Bernoulli.DeSilvaJerison.UpperAlgebra.identity_hi line 79
  10. lemma OAI.Bernoulli.DeSilvaJerison.UpperAlgebra.bound_hi line 84
  11. def OAI.Bernoulli.DeSilvaJerison.gSup line 102

    Source documentation

    For τ=-2 the auxiliary Legendre solution is elementary and rational.

    def gSup (t:ℝ) :ℝ := (1+t^2)/(1-t^2)^2
  12. def OAI.Bernoulli.DeSilvaJerison.gSup1 line 103
  13. def OAI.Bernoulli.DeSilvaJerison.qSup line 104
  14. def OAI.Bernoulli.DeSilvaJerison.qSup1 line 105
  15. def OAI.Bernoulli.DeSilvaJerison.GSup line 106
  16. lemma OAI.Bernoulli.DeSilvaJerison.gSup_pos line 108
  17. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_gSup line 113
  18. lemma OAI.Bernoulli.DeSilvaJerison.qSup_eq line 122
  19. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_qSup line 128
  20. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_GSup line 139
  21. lemma OAI.Bernoulli.DeSilvaJerison.upper_endpoint_bounds line 160
  22. lemma OAI.Bernoulli.DeSilvaJerison.qSup_small line 169
  23. lemma OAI.Bernoulli.DeSilvaJerison.GSup_nonpos_deriv line 190
  24. lemma OAI.Bernoulli.DeSilvaJerison.GSup_near line 210
  25. lemma OAI.Bernoulli.DeSilvaJerison.c7_lower line 229
  26. lemma OAI.Bernoulli.DeSilvaJerison.numerator_scaled_bounds line 239
  27. lemma OAI.Bernoulli.DeSilvaJerison.quadratic_bound line 268
  28. lemma OAI.Bernoulli.DeSilvaJerison.GSup_numerator line 284
  29. lemma OAI.Bernoulli.DeSilvaJerison.GSup_far line 298
  30. theorem OAI.Bernoulli.DeSilvaJerison.GSup_le_c7 line 321

    Source documentation

    Exact replacement for the numerical supersolution slope plot, using the rational τ=-2 Legendre solution and the rational angle 3/5.

    theorem GSup_le_c7 {t:ℝ} (hl:t7≤t) (hr:t≤3/5) : GSup t≤c7 := by
…

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

  31. def OAI.Bernoulli.DeSilvaJerison.capAmplitude line 330

    Source documentation

    The transverse unit-cylinder profile of the concrete upper barrier.

    def capAmplitude : ℝ := -(10/17)*f (3/5)

    Mentions: OAI.Bernoulli.DeSilvaJerison.f

  32. def OAI.Bernoulli.DeSilvaJerison.capRadius line 331
  33. def OAI.Bernoulli.DeSilvaJerison.capAngle line 332
  34. def OAI.Bernoulli.DeSilvaJerison.capH line 333
  35. def OAI.Bernoulli.DeSilvaJerison.capHP line 334
  36. def OAI.Bernoulli.DeSilvaJerison.capP line 336
  37. def OAI.Bernoulli.DeSilvaJerison.capB line 337
  38. def OAI.Bernoulli.DeSilvaJerison.capV line 339
  39. def OAI.Bernoulli.DeSilvaJerison.capVP line 341
  40. def OAI.Bernoulli.DeSilvaJerison.capVPP line 343
  41. def OAI.Bernoulli.DeSilvaJerison.capY line 345
  42. lemma OAI.Bernoulli.DeSilvaJerison.capRadius_pos line 347
  43. lemma OAI.Bernoulli.DeSilvaJerison.capRadius_sq line 348
  44. lemma OAI.Bernoulli.DeSilvaJerison.capAngle_mem line 349
  45. lemma OAI.Bernoulli.DeSilvaJerison.capAngle_d line 355
  46. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_capRadius line 360
  47. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_capAngle line 367
  48. lemma OAI.Bernoulli.DeSilvaJerison.cap_f_relation line 373
  49. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_capH line 380
  50. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_capHP line 389
  51. lemma OAI.Bernoulli.DeSilvaJerison.capH_even line 401
  52. lemma OAI.Bernoulli.DeSilvaJerison.capHP_odd line 403
  53. lemma OAI.Bernoulli.DeSilvaJerison.capH_zero line 407
  54. lemma OAI.Bernoulli.DeSilvaJerison.capHP_zero line 408
  55. lemma OAI.Bernoulli.DeSilvaJerison.capRadius_end line 409
  56. lemma OAI.Bernoulli.DeSilvaJerison.capAngle_end line 413
  57. lemma OAI.Bernoulli.DeSilvaJerison.capH_end line 414
  58. lemma OAI.Bernoulli.DeSilvaJerison.capHP_end line 417
  59. lemma OAI.Bernoulli.DeSilvaJerison.capAmplitude_bounds line 423
  60. lemma OAI.Bernoulli.DeSilvaJerison.capAmplitude_pos line 430
  61. lemma OAI.Bernoulli.DeSilvaJerison.capAmplitude_le line 431
  62. lemma OAI.Bernoulli.DeSilvaJerison.capB_bounds line 433
  63. def OAI.Bernoulli.DeSilvaJerison.CapSign.flo line 450
  64. def OAI.Bernoulli.DeSilvaJerison.CapSign.polyK line 451
  65. def OAI.Bernoulli.DeSilvaJerison.CapSign.bern line 453
  66. lemma OAI.Bernoulli.DeSilvaJerison.CapSign.identity line 463
  67. lemma OAI.Bernoulli.DeSilvaJerison.CapSign.polyK_nonpos line 466
  68. lemma OAI.Bernoulli.DeSilvaJerison.capRadius_one_le line 482
  69. lemma OAI.Bernoulli.DeSilvaJerison.capHP_antitone line 486
  70. lemma OAI.Bernoulli.DeSilvaJerison.capHP_nonpos line 493
  71. lemma OAI.Bernoulli.DeSilvaJerison.capHP_le_linear line 497
  72. lemma OAI.Bernoulli.DeSilvaJerison.capH_antitone line 513
  73. lemma OAI.Bernoulli.DeSilvaJerison.capH_nonneg line 521
  74. lemma OAI.Bernoulli.DeSilvaJerison.capHPP_nonpos line 528
  75. lemma OAI.Bernoulli.DeSilvaJerison.capAngle_bounds line 532
  76. lemma OAI.Bernoulli.DeSilvaJerison.cap_flo_bound line 540
  77. lemma OAI.Bernoulli.DeSilvaJerison.cap_K_identity line 552
  78. theorem OAI.Bernoulli.DeSilvaJerison.cap_K_nonpos line 565
  79. def OAI.Bernoulli.DeSilvaJerison.capEta line 600
  80. def OAI.Bernoulli.DeSilvaJerison.capW line 601
  81. def OAI.Bernoulli.DeSilvaJerison.capWP line 602
  82. def OAI.Bernoulli.DeSilvaJerison.capWPP line 603
  83. lemma OAI.Bernoulli.DeSilvaJerison.capP_bounds line 605
  84. lemma OAI.Bernoulli.DeSilvaJerison.capEta_bounds line 609
  85. lemma OAI.Bernoulli.DeSilvaJerison.capW_even line 628
  86. lemma OAI.Bernoulli.DeSilvaJerison.capW_zero_nonpos line 630
  87. lemma OAI.Bernoulli.DeSilvaJerison.capW_end line 635
  88. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_capW line 643
  89. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_capWP line 650
  90. lemma OAI.Bernoulli.DeSilvaJerison.capRadius_cube_bound line 663
  91. lemma OAI.Bernoulli.DeSilvaJerison.capW_radial_convex line 668
  92. def OAI.Bernoulli.DeSilvaJerison.capZ line 680
  93. def OAI.Bernoulli.DeSilvaJerison.capZP line 681
  94. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_capZ line 682
  95. lemma OAI.Bernoulli.DeSilvaJerison.hasDerivAt_capZP line 686
  96. lemma OAI.Bernoulli.DeSilvaJerison.capZ_convex line 694
  97. theorem OAI.Bernoulli.DeSilvaJerison.cap_interface_nonpos line 713

    Source documentation

    The exact jump sign at the cylindrical gluing interface of the outer harmonic perturbation and the interior smooth cap.

    theorem cap_interface_nonpos {s : ℝ} (hs : |s|≤3/4) : capW s≤0 := by
…

    Mentions: OAI.Bernoulli.DeSilvaJerison.capW

  98. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.V line 731
  99. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.D line 732
  100. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.E line 733
  101. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.H line 734
  102. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.MN line 735
  103. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.NN line 736
  104. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_0 line 739
  105. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_0_nonneg line 744
  106. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_1 line 748
  107. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_1_nonneg line 753
  108. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_2 line 757
  109. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_2_nonneg line 762
  110. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_3 line 766
  111. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_3_nonneg line 771
  112. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_4 line 775
  113. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_4_nonneg line 780
  114. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.bern_Mlo line 784
  115. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.identity_Mlo line 790
  116. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mlo_nonneg line 795
  117. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_0 line 813
  118. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_0_nonneg line 818
  119. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_1 line 822
  120. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_1_nonneg line 827
  121. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_2 line 831
  122. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_2_nonneg line 836
  123. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_3 line 840
  124. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_3_nonneg line 845
  125. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_4 line 849
  126. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_4_nonneg line 854
  127. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.bern_Mhi line 858
  128. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.identity_Mhi line 864
  129. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Mhi_nonneg line 869
  130. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_0 line 887
  131. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_0_nonneg line 894
  132. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_1 line 898
  133. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_1_nonneg line 905
  134. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_2 line 909
  135. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_2_nonneg line 916
  136. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_3 line 920
  137. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_3_nonneg line 927
  138. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_4 line 931
  139. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_4_nonneg line 938
  140. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_5 line 942
  141. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_5_nonneg line 949
  142. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_6 line 953
  143. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_6_nonneg line 960
  144. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_7 line 964
  145. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_7_nonneg line 971
  146. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.bern_Nlo line 975
  147. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.identity_Nlo line 984
  148. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nlo_nonneg line 989
  149. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_0 line 1010
  150. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_0_nonneg line 1017
  151. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_1 line 1021
  152. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_1_nonneg line 1028
  153. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_2 line 1032
  154. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_2_nonneg line 1039
  155. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_3 line 1043
  156. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_3_nonneg line 1050
  157. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_4 line 1054
  158. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_4_nonneg line 1061
  159. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_5 line 1065
  160. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_5_nonneg line 1072
  161. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_6 line 1076
  162. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_6_nonneg line 1083
  163. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_7 line 1087
  164. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_7_nonneg line 1094
  165. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.bern_Nhi line 1098
  166. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.identity_Nhi line 1107
  167. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Nhi_nonneg line 1112
  168. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.H_pos line 1134
  169. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.coeff_bounds line 1135