OAI/Combinatorics/KServer/Simplex.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Exact analytic kernels of §04, necessary for the simplex minimization. Only the point values of integrands at zero are irrelevant to the integrals.

  1. def OAI.KServer.SimplexAnalytic.regularF line 15
  2. def OAI.KServer.SimplexAnalytic.markedF line 17
  3. def OAI.KServer.SimplexAnalytic.kernel line 19
  4. def OAI.KServer.SimplexAnalytic.singularKernel line 21
  5. def OAI.KServer.SimplexAnalytic.primitive line 23
  6. def OAI.KServer.SimplexAnalytic.regularTail line 27

    Source documentation

    Continuous primitive of the regular B/s term, including the improper endpoint.

    def regularTail (h : ℝ) : ℝ → ℝ := Function.update (fun s => h / (h - Real.log s)) 0 0
  7. lemma OAI.KServer.SimplexAnalytic.regularTail_zero line 29
  8. lemma OAI.KServer.SimplexAnalytic.regularTail_of_ne line 31
  9. lemma OAI.KServer.SimplexAnalytic.regularTail_continuousAt_zero line 34
  10. lemma OAI.KServer.SimplexAnalytic.regularTail_derivative line 42
  11. lemma OAI.KServer.SimplexAnalytic.regularTail_continuousOn line 58
  12. lemma OAI.KServer.SimplexAnalytic.regular_singular_formula line 66
  13. lemma OAI.KServer.SimplexAnalytic.regular_singular_intervalIntegrable line 74
  14. lemma OAI.KServer.SimplexAnalytic.regular_singular_integral line 90
  15. lemma OAI.KServer.SimplexAnalytic.kernel_measurable line 100
  16. lemma OAI.KServer.SimplexAnalytic.singularKernel_measurable line 104
  17. lemma OAI.KServer.SimplexAnalytic.log_inverse_nonneg line 108
  18. lemma OAI.KServer.SimplexAnalytic.marked_quadratic_lower line 112
  19. lemma OAI.KServer.SimplexAnalytic.singular_dominated line 118
  20. lemma OAI.KServer.SimplexAnalytic.singular_intervalIntegrable_of_quadratic line 136
  21. lemma OAI.KServer.SimplexAnalytic.kernel_intervalIntegrable line 148
  22. lemma OAI.KServer.SimplexAnalytic.integrand_affine line 162
  23. lemma OAI.KServer.SimplexAnalytic.integrand_intervalIntegrable line 168
  24. lemma OAI.KServer.SimplexAnalytic.primitive_continuousOn line 176
  25. lemma OAI.KServer.SimplexAnalytic.primitive_derivative line 187
  26. lemma OAI.KServer.SimplexAnalytic.log_inverse_tendsto line 209
  27. lemma OAI.KServer.SimplexAnalytic.polynomial_log_decay line 213
  28. lemma OAI.KServer.SimplexAnalytic.quadratic_lower_tendsto line 224
  29. lemma OAI.KServer.SimplexAnalytic.singular_tendsto line 232
  30. lemma OAI.KServer.SimplexAnalytic.integrand_tendsto_atBot line 248
  31. lemma OAI.KServer.SimplexAnalytic.primitive_inward_atBot line 265
  32. lemma OAI.KServer.SimplexAnalytic.regular_quadratic_lower line 291
  33. lemma OAI.KServer.SimplexAnalytic.regular_decay line 298
  34. lemma OAI.KServer.SimplexAnalytic.marked_decay line 303
  35. lemma OAI.KServer.SimplexAnalytic.marked_lower_constant line 308
  36. lemma OAI.KServer.SimplexAnalytic.regular_inward_atBot line 315
  37. lemma OAI.KServer.SimplexAnalytic.marked_singular_intervalIntegrable line 324
  38. lemma OAI.KServer.SimplexAnalytic.marked_inward_atBot line 329
  39. lemma OAI.KServer.SimplexAnalytic.exp_marked_bound line 339

    Source documentation

    Elementary exponential estimate giving the marked contribution's side cancellation.

    lemma exp_marked_bound {y : ℝ} (hy : 0 ≤ y) :
    Real.exp (-y) * y * (1 + y) ≤ 2 * (1 - Real.exp (-y)) := by
…
  40. lemma OAI.KServer.SimplexAnalytic.exp_square_bound line 347
  41. lemma OAI.KServer.SimplexAnalytic.regular_exp_tail line 356
  42. lemma OAI.KServer.SimplexAnalytic.regular_coordinate_bound line 369
  43. lemma OAI.KServer.SimplexAnalytic.marked_coordinate_bound line 389
  44. def OAI.KServer.SimplexAnalytic.affineLogTail line 403

    Source documentation

    Logarithmic comparison primitive on the upper half of the marked integral.

    def affineLogTail (u H s : ℝ) : ℝ := -Real.log (u - H * Real.log s) / H
  45. lemma OAI.KServer.SimplexAnalytic.affineLogTail_derivative line 405
  46. lemma OAI.KServer.SimplexAnalytic.marked_lower_half_bound line 416
  47. lemma OAI.KServer.SimplexAnalytic.marked_singular_integral_bound line 442
  48. lemma OAI.KServer.SimplexAnalytic.regular_denominator_sum line 530
  49. lemma OAI.KServer.SimplexAnalytic.marked_denominator_sum line 547
  50. lemma OAI.KServer.SimplexAnalytic.log_inverse_nonneg_closed line 607
  51. lemma OAI.KServer.SimplexAnalytic.primitive_affine line 613
  52. lemma OAI.KServer.SimplexAnalytic.regularF_lower line 629
  53. lemma OAI.KServer.SimplexAnalytic.regular_kernel_bounds line 634
  54. lemma OAI.KServer.SimplexAnalytic.regular_coefficients line 643
  55. lemma OAI.KServer.SimplexAnalytic.regular_component_bound line 669
  56. lemma OAI.KServer.SimplexAnalytic.marked_positive line 687
  57. lemma OAI.KServer.SimplexAnalytic.marked_coefficients line 693
  58. lemma OAI.KServer.SimplexAnalytic.marked_component_bound line 726
  59. lemma OAI.KServer.SimplexAnalytic.affine_sum_input_bound line 792

    Source documentation

    Dimension-free input bound for an affine sum of the exact primitives. The scalar assumptions are the integral coefficient bounds established above.

    lemma affine_sum_input_bound {ι : Type*} [Fintype ι]
    {K J η B B' : ι → ℝ} {L ηmax CK CJ : ℝ}
    (hL : 0 ≤ L) (hη : ∀ i, 0 ≤ η i) (hηmax : ∀ i, η i ≤ ηmax)
    (hK : ∑ i, |K i| ≤ CK) (hJ : ∀ i, |J i| ≤ CJ) :
    |(∑ i, L * ((∑ j, B j) * K i - (1 + η i) * B i * J i)) -
      (∑ i, L * ((∑ j, B' j) * K i - (1 + η i) * B' i * J i))| ≤
      L * (CK + (1 + ηmax) * CJ) * ∑ i, |B i - B' i| := by
…
  60. lemma OAI.KServer.SimplexAnalytic.regular_input_slopes line 834

    Source documentation

    The exact regular-domain version of (alpha-input-slopes), with constant 3.

    lemma regular_input_slopes {ι : Type*} [Fintype ι]
    {h η B B' a : ι → ℝ} {Cα ell : ℝ}
    (ha0 : ∀ i, 0 ≤ a i) (ha1 : ∑ i, a i = 1)
    (hh : ∀ i, 1 ≤ h i) (hη0 : ∀ i, 0 ≤ η i) (hη1 : ∀ i, η i ≤ 1)
    (hC : 0 ≤ Cα) (hl : 0 ≤ ell) :
    |(∑ i, primitive (regularF (h i)) Cα ell (η i) (∑ j, B j) (B i) 0 (a i)) -
      (∑ i, primitive (regularF (h i)) Cα ell (η i) (∑ j, B' j) (B' i) 0 (a i))| ≤
      3 * Cα * ell * ∑ i, |B i - B' i| := by
…

    Mentions: OAI.KServer.SimplexAnalytic.primitive, OAI.KServer.SimplexAnalytic.regularF

  61. lemma OAI.KServer.SimplexAnalytic.marked_input_slopes line 877

    Source documentation

    The source marked-domain affine input bound, also uniform as u tends to 0.

    lemma marked_input_slopes {ι : Type*} [Fintype ι] [DecidableEq ι] (o : ι)
    {h η B B' a : ι → ℝ} {Cα ell u H : ℝ}
    (ha0 : ∀ i, 0 ≤ a i) (ha1 : ∑ i, a i = 1)
    (hh : ∀ i, i ≠ o → 1 ≤ h i) (hu : 0 < u) (hu1 : u ≤ 1)
    (hH : H = 1 + Real.log (1 / u))
    (hη0 : ∀ i, 0 ≤ η i) (hη1 : ∀ i, η i ≤ 1)
    (hC : 0 ≤ Cα) (hl : 0 ≤ ell) :
    let F := fun i => if i = o then markedF u H else regularF (h i)
…

    Mentions: OAI.KServer.SimplexAnalytic.markedF, OAI.KServer.SimplexAnalytic.regularF