OAI/Computability/MaxCut/Estimates/Density.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OptimalMaxCut.GaussianBellman.density line 13
  2. def OAI.OptimalMaxCut.GaussianBellman.cdf line 15
  3. theorem OAI.OptimalMaxCut.GaussianBellman.density_pos line 17
  4. theorem OAI.OptimalMaxCut.GaussianBellman.density_nonneg line 18
  5. theorem OAI.OptimalMaxCut.GaussianBellman.density_continuous line 19
  6. theorem OAI.OptimalMaxCut.GaussianBellman.density_integrable line 23
  7. theorem OAI.OptimalMaxCut.GaussianBellman.density_neg line 25
  8. theorem OAI.OptimalMaxCut.GaussianBellman.density_deriv line 28
  9. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_deriv line 35
  10. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_continuous line 43
  11. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_strictMono line 46
  12. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_zero line 52
  13. theorem OAI.OptimalMaxCut.GaussianBellman.integral_density line 54
  14. theorem OAI.OptimalMaxCut.GaussianBellman.half_integral line 57
  15. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_eq_integral line 65
  16. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_mem_Ioo line 72
  17. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_neg line 86
  18. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_tendsto_atBot line 95
  19. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_tendsto_atTop line 100
  20. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_range line 105
  21. def OAI.OptimalMaxCut.GaussianBellman.quantile line 113
  22. theorem OAI.OptimalMaxCut.GaussianBellman.quantile_cdf line 115
  23. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_quantile line 118
  24. theorem OAI.OptimalMaxCut.GaussianBellman.quantile_strictMonoOn line 122
  25. theorem OAI.OptimalMaxCut.GaussianBellman.quantile_image line 127
  26. theorem OAI.OptimalMaxCut.GaussianBellman.quantile_continuousAt line 132
  27. theorem OAI.OptimalMaxCut.GaussianBellman.quantile_deriv line 138
  28. theorem OAI.OptimalMaxCut.GaussianBellman.quantile_half line 145
  29. theorem OAI.OptimalMaxCut.GaussianBellman.integral_hasDerivAt_compact line 150

    Source documentation

    Differentiation under a finite integral using the actual compact uniform bound, to be applied to the Plackett integrand below.

     theorem integral_hasDerivAt_compact {F F' : ℝ → ℝ → ℝ} {a b u v x : ℝ}
    (hx : x ∈ Ioo u v) (hab : a ≤ b)
    (hc : ContinuousOn (Function.uncurry F) (Icc u v ×ˢ Icc a b))
    (hc' : ContinuousOn (Function.uncurry F') (Icc u v ×ˢ Icc a b))
    (hd : ∀ z ∈ Icc u v, ∀ t ∈ Icc a b, HasDerivAt (F · t) (F' z t) z) :
    HasDerivAt (fun z => ∫ t in a..b, F z t) (∫ t in a..b, F' x t) x := by
…
  30. def OAI.OptimalMaxCut.GaussianBellman.sigma line 180
  31. def OAI.OptimalMaxCut.GaussianBellman.conditionalArg line 181
  32. def OAI.OptimalMaxCut.GaussianBellman.plackett line 182
  33. def OAI.OptimalMaxCut.GaussianBellman.kernel line 184
  34. theorem OAI.OptimalMaxCut.GaussianBellman.sigma_pos line 187
  35. theorem OAI.OptimalMaxCut.GaussianBellman.sigma_sq line 191
  36. theorem OAI.OptimalMaxCut.GaussianBellman.sigma_continuous line 195
  37. theorem OAI.OptimalMaxCut.GaussianBellman.sigma_deriv line 197
  38. theorem OAI.OptimalMaxCut.GaussianBellman.plackett_pos line 203
  39. theorem OAI.OptimalMaxCut.GaussianBellman.conditionalArg_continuousOn line 206
  40. theorem OAI.OptimalMaxCut.GaussianBellman.plackett_continuousOn line 213
  41. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_ge_product line 221
  42. theorem OAI.OptimalMaxCut.GaussianBellman.density_mul line 229
  43. theorem OAI.OptimalMaxCut.GaussianBellman.density_zero_sq line 235
  44. theorem OAI.OptimalMaxCut.GaussianBellman.plackett_symm line 240
  45. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_symm line 255
  46. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_half line 265
  47. theorem OAI.OptimalMaxCut.GaussianBellman.conditionalArg_deriv_u line 283
  48. theorem OAI.OptimalMaxCut.GaussianBellman.conditionalArg_deriv_v line 288
  49. theorem OAI.OptimalMaxCut.GaussianBellman.conditionalArg_deriv_t line 293
  50. theorem OAI.OptimalMaxCut.GaussianBellman.plackett_deriv_u line 304
  51. theorem OAI.OptimalMaxCut.GaussianBellman.plackett_quantile_deriv_x line 318
  52. theorem OAI.OptimalMaxCut.GaussianBellman.conditionalCDF_deriv_t line 326
  53. def OAI.OptimalMaxCut.GaussianBellman.flux line 332
  54. theorem OAI.OptimalMaxCut.GaussianBellman.flux_continuousOn line 335
  55. theorem OAI.OptimalMaxCut.GaussianBellman.quantile_continuousOn line 344
  56. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_deriv_x line 347
  57. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_deriv_y line 385
  58. def OAI.OptimalMaxCut.GaussianBellman.kernelX line 393
  59. def OAI.OptimalMaxCut.GaussianBellman.kernelXX line 394
  60. def OAI.OptimalMaxCut.GaussianBellman.kernelXY line 396
  61. theorem OAI.OptimalMaxCut.GaussianBellman.kernelX_deriv_x line 399
  62. theorem OAI.OptimalMaxCut.GaussianBellman.kernelX_deriv_y line 408
  63. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_weighted_hessian line 417
  64. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_weighted_hessian_nonpos line 427
  65. theorem OAI.OptimalMaxCut.GaussianBellman.density_contDiff line 435
  66. theorem OAI.OptimalMaxCut.GaussianBellman.cdf_contDiff line 439
  67. theorem OAI.OptimalMaxCut.GaussianBellman.quantile_contDiffOn line 449
  68. theorem OAI.OptimalMaxCut.GaussianBellman.kernelX_contDiffOn line 462
  69. def OAI.OptimalMaxCut.GaussianBellman.kernelD line 472
  70. theorem OAI.OptimalMaxCut.GaussianBellman.kernelD_contDiffOn line 476
  71. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_fderiv line 484
  72. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_contDiffOn line 510
  73. theorem OAI.OptimalMaxCut.GaussianBellman.affinePath_deriv line 527
  74. theorem OAI.OptimalMaxCut.GaussianBellman.affinePath_iterated_two line 531
  75. theorem OAI.OptimalMaxCut.GaussianBellman.affinePath_iterated_three line 537
  76. theorem OAI.OptimalMaxCut.GaussianBellman.iteratedDeriv_affinePath_two line 543
  77. theorem OAI.OptimalMaxCut.GaussianBellman.iteratedDeriv_affinePath_three line 552
  78. theorem OAI.OptimalMaxCut.GaussianBellman.compact_third_derivative_bound line 565
  79. theorem OAI.OptimalMaxCut.GaussianBellman.compact_cubic_taylor_bound line 576
  80. theorem OAI.OptimalMaxCut.GaussianBellman.kernelX_line_deriv line 631
  81. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_line_deriv line 646
  82. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_line_second line 656
  83. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_second_diagonal line 682
  84. theorem OAI.OptimalMaxCut.GaussianBellman.norm_pair_cube_le line 695
  85. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_uniform_cubic line 701
  86. def OAI.OptimalMaxCut.GaussianBellman.sign line 730
  87. def OAI.OptimalMaxCut.GaussianBellman.bitPairWeight line 732
  88. theorem OAI.OptimalMaxCut.GaussianBellman.bitPairWeight_nonneg line 734
  89. theorem OAI.OptimalMaxCut.GaussianBellman.bitPairWeight_mass line 738
  90. theorem OAI.OptimalMaxCut.GaussianBellman.bitPairWeight_marginal line 741
  91. theorem OAI.OptimalMaxCut.GaussianBellman.bitPairWeight_symm line 744
  92. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_one_bit line 747
  93. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_lipschitz_x line 798
  94. theorem OAI.OptimalMaxCut.GaussianBellman.kernel_lipschitz line 811